On Computing Minimal Model:A MiniSAT-based Approach

Computing the minimal model is an essential task in many reasoning systems in the field of Artificial Intelligence(AI).However,even for a positive conjunctive normal form(CNF)formula,the tasks of computing and checking its minimal model are intractable.Currently,one of the main methods to compute minimal models of a given CNF formula is to convert the CNF formula into a disjunctive logic program and then compute its stable model by an answer set program(ASP)solver.Therefore,we propose several new methods to calculate the minimal model of CNF and apply them to compute minimal diagnosis.The main work of this paper is as follows:1)Firstly,we propose an SAT solver-based method,called MMSAT1 to calculate the minimal model.Secondly,it is combined with the Check Min MR,a recent minimal model checking algorithm based on minimal reduct,called MRSAT.It is based on minimal model decomposition.Then according to the definition of the minimal reduct,by combining the algorithms MMSAT and MRSAT,we have obtained two algorithms MR_MMSAT and MR_MRSAT.Both of them are based on minimal reduct.Finally,testing a large number of randomly generated 3CNF formulas and some examples from the industry benchmark in the SAT international competition.Experimental results show that the four new methods for calculating minimal models proposed in this paper are effective on both random 3CNF formulas and SAT industrial test examples.And these approaches are significantly faster than the latest version of clingo,a state-of-the-art ASP solver.Moreover,it has been found that clingo5.4 has bugs on some of the SAT industrial competition examples,while the methods proposed in this paper are more stable.2)The methods of computing the minimal model are used for the model-based diagnosis(MBD)problems.Especially,a new method MMSAT_Diagnosis is proposed,which combines the algorithm MMSAT to calculate the combined circuit minimal diagnosis.And a new method SAT_Diagnosis based on the SAT solver is proposed.We have also presented the decision theorem of minimal diagnosis.Then,the MMSAT_Diagnosis and SAT_Diagnosis algorithm has been implemented based on the MMSAT algorithm.These approaches are tested on the international standard test circuit ISCAS-85.Experimental results show that the two new methods are very effective in computing a minimal diagnosis of these circuit benchmarks.The algorithm implementation and result address of this paper can be found on GitHub1.