Advanced Search
    Zhang Li, Wang Yisong, Xie Zhongtao, Feng Renyan. Computing Propositional Minimal Models: MiniSAT-Based Approaches[J]. Journal of Computer Research and Development, 2021, 58(11): 2515-2523. DOI: 10.7544/issn1000-1239.2021.20200370
    Citation: Zhang Li, Wang Yisong, Xie Zhongtao, Feng Renyan. Computing Propositional Minimal Models: MiniSAT-Based Approaches[J]. Journal of Computer Research and Development, 2021, 58(11): 2515-2523. DOI: 10.7544/issn1000-1239.2021.20200370

    Computing Propositional Minimal Models: MiniSAT-Based Approaches

    • 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.
    • loading

    Catalog

      Turn off MathJax
      Article Contents

      /

      DownLoad:  Full-Size Img  PowerPoint
      Return
      Return