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

Computing Propositional Minimal Models:MiniSAT-Based Approaches

计算命题公式的极小模型在人工智能推理系统中是一项必不可少的任务.然而,即使是正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则更稳定.

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.