ISSN 1000-1239 CN 11-1777/TP

Journal of Computer Research and Development ›› 2021, Vol. 58 ›› Issue (11): 2515-2523.doi: 10.7544/issn1000-1239.2021.20200370

Previous Articles     Next Articles

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).

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

CLC Number: