摘要：求解不可滿足問題的極小不可滿足子集(minimal unsatisfiable subset,MUS)是人工智能領域的重要研究方向.MARCO-M方法是目前采用單一極大化模型求解MUS效率最高的方法,但此方法未對求解空間進行進一步有效剪枝.針對MARCO-M方法的不足,結合可滿足問題求解復雜度低于不可滿足問題的特征,提出基于雙模型即極大中間化模型的MARCO-MAM方法求解MUS.此方法對中間模型求解若得到極大可滿足子集(maximal satisfiable subset,MSS),則利用可滿足問題對應求解空間對不可滿足問題的求解空間進行剪枝,即利用MSS對應的空間來對MUS搜索空間進行剪枝,進而通過縮減未探索空間來提高MUS求解效率;如果中間模型進行求解得到MUS時,則減少了MARCO-M方法中MUS的不可滿足迭代求解次數.此方法避免了MARCO-M方法單一極大化模型求解MUS時未有效利用其他優化技術對求解空間進行剪枝的問題.實驗結果表明:與MARCO-M方法相比MARCO-MAM方法效率較高,尤其在大規模問題或較大搜索空間時效率提高更為明顯.
注：因版權方要求，不能公開全文，如需全文，請咨詢雜志社
