基于双模型的MUS求解方法
【摘要】 求解不可满足问题的极小不可满足子集（minimalunsatisfiablesubset，MUS）是人工智能领域的重要研究方向.MARCO-M方法是目前采用单一极大化模型求解MUS效率最高的方法，但此方法未对求解空间进行进一步有效剪枝.针对MARCO-M方法的不足，结合可满足问题求解复杂度低于不可满足问题的特征，提出基于双模型即极大-中间化模型的MARCO-MAM方法求解MUS.此方法对中间模型求解若得到极大可满足子集（maximalsatisfiablesubset，MSS），则利用可满足问题对应求解空收稿日期:2018-12-24;修回日期:2019-05-09基金项目:国家自然科学基金项目（61872159，61672261，61502199）ThisworkwassupportedbytheNationalNaturalScienceFoundationofChina（61872159，61672261，61502199）通信作者:张立明（limingzhang@jlu.e
