计算机研究与发展

作者：张丽,王以松,谢仲涛,冯仁艳,

关键词：极小模型, SAT求解器, CNF公式, 极小归约, 极小模型分解,

计算命题公式的极小模型在人工智能推理系统中是一项必不可少的任务.然而，即使是正CNF(conjunctivenormalform)公式，其极小模型的计算和验证都不是易处理的.当前，计算CNF公式极小模型的主要方法之一是将其转换为析取逻辑程序后用回答集程序(answersetprogramming,ASP)求解器计算其稳定模型/回答集.针对计算CNF公式的极小模型的问题，提出一种基于可满足性问题(satisfiabilityproblem,SAT)求解器的计算极小模型的方法MMSAT；然后结合最近基于极小归约的极小模型验证算法CheckMinMR，提出了基于极小模型分解的计算极小模型方法MRSAT；最后对随机生成的大量的3CNF公式和SAT国际竞赛上的部分工业基准测试用例进行测试.实验结果表明：MMSAT和MRSAT对随机3CNF公式和SAT工业测试用例都是有效的，且计算极小模型的速度都明显快于最新版的clingo，并且在SAT工业实例上发现了clingo有计算出错的情况，而MMSAT和MRSAT则更稳定.

来源：2021年第11期

《计算机研究与发展》期刊编辑部

查看计算机研究与发展杂志2021年第11期