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