ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2021, Vol. 58 ›› Issue (11): 2515-2523.doi: 10.7544/issn1000-1239.2021.20200370

• 人工智能 • 上一篇    下一篇

基于MiniSAT的命题极小模型计算方法

张丽1,王以松1,2,谢仲涛1,冯仁艳1   

  1. 1(贵州大学计算机科学与技术学院 贵阳 550025);2(公共大数据国家重点实验室(贵州大学) 贵阳 550025) (gs.lizhang18@gzu.edu.cn)
  • 出版日期: 2021-11-01
  • 基金资助: 
    国家自然科学基金项目(61976065,U1836205)

Computing Propositional Minimal Models: MiniSAT-Based Approaches

Zhang Li1, Wang Yisong1,2, Xie Zhongtao1, Feng Renyan1   

  1. 1(College of Computer Science and Technology, Guizhou University, Guiyang 550025);2(State Key Laboratory of Public Big Data (Guizhou University), Guiyang 550025)
  • Online: 2021-11-01
  • Supported by: 
    This work was supported by the National Natural Science Foundation of China (61976065, U1836205).

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

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

Abstract: Computing minimal models is an essential task in many reasoning systems in artificial intelligence. However, even for a positive conjunctive normal form (CNF) formula, the tasks of computing and checking its minimal model are not tractable. To compute a minimal model of a clause theory, one of the current main methods is to convert the clause theory into a disjunction logic program and use an answer set programming (ASP) solver to compute its stable model. This paper proposes a method MMSAT for computing minimal models based on SAT(satisfiability problem) solvers. In terms of the recently proposed minimal reduct based minimal checking algorithm CheckMinMR, a minimal model decomposing based minimal model computing algorithm MRSAT is proposed. Finally, the two algorithms are evaluated by a large number of randomly generated 3CNF formulas and industrial benchmarks from the SAT international competition. Experimental results show that the two methods proposed in this paper compute minimal models at about three times faster than clingo for random 3CNF formulas and slightly faster than clingo for industrial SAT benchmarks. Thus, they are effective. In addition, it also reveals that clingo sometimes incorrectly computes a minimal model. Thus, the two proposed methods in this paper are more stable than clingo.

Key words: minimal model, SAT solver, CNF formula, minimal reduct, decomposing minimal model

中图分类号: