HI,欢迎来到好期刊网,发表咨询:400-888-9411 订阅咨询:400-888-1571证券代码(211862)

基于双模型的MUS求解方法

摘要:求解不可满足问题的极小不可满足子集(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方法效率较高,尤其在大规模问题或较大搜索空间时效率提高更为明显.

关键词:
  • 命题可满足问题  
  • 极小不可满足子集  
  • 极大可满足子集  
  • 幂集探索  
  • 双模型  
作者:
欧阳丹彤; 高菡; 田乃予; 刘梦; 张立明
单位:
吉林大学软件学院; 长春130012; 吉林大学计算机科学与技术学院; 长春130012; 符号计算与知识工程教育部重点实验室(吉林大学); 长春130012
刊名:
计算机研究与发展

注:因版权方要求,不能公开全文,如需全文,请咨询杂志社

期刊名称:计算机研究与发展

计算机研究与发展杂志紧跟学术前沿,紧贴读者,国内刊号为:11-1777/TP。坚持指导性与实用性相结合的原则,创办于1958年,杂志在全国同类期刊中发行数量名列前茅。