Study On Optimization Strategy Of SAT Problem Based On CDCL

As the first NP-complete problem which has been proved,the satisfiability problem(SAT)is one of the important research directions of contemporary computational theory.The solution of SAT problem contributes to solving other NP problems.The quick solver to SAT problem is very important both in theory and in practice.SAT problem is widely used in the fields of artificial intelligence,automated reasoning,automatic software validation and so on.Thus,it is significant to look for efficient algorithms to solve SAT problem.At present,there are mainly two kinds of algorithm to solve SAT problem,including the complete algorithm and the incomplete algorithm.The incomplete algorithms is based on local searching,while the complete algorithm is based on branching and backtracking.Most state-of-the-art complete algorithms,including Conflict Driven Clause Learning(CDCL),are improved from the typical DPLL algorithm,which is proposed by Martin Davis,Hilary Putnam,George Logemann and Donald W.Loveland in 1962.There are many SAT solvers based on CDCL algorithm come into being in order to solve more complex SAT problem,such as z Chaff,MiniSAT,Glucose,Lingeling,PicoSAT and others.Based on the framework of CDCL algorithm,the main research work of this paper are the following:1.According to variable decision levels and conflict numbers,a variable score increment function is proposed to evaluate the variable scores during different searching stage dynamically.A branching heuristic based on variable decision levels(DLBH)is put forward in order to give guidance to the branching stage.2.According to the different variable decision levels appeared in the learnt clause,the definition of clause deepness is proposed to evaluate the quality of learnt clauses.A learnt clause deletion strategy based on the clause deepness(DBCD)is put forward in order to delete clauses of low quality and maintain high efficiency.3.Two new solvers glucose3.0+dlbh and glucose3.0+dbcd are obtained after DLBHand DBCD are embedded into the widely used solver Glucose3.0,respectively.Then,another new solver glucose3.0+dlbh+dbcd is obtained after DLBH and DBCD are embedded into Glucose3.0 at the same time.A comparison is made among glucose3.0+dlbh,glucose3.0+dbcd,glucose3.0+dlbh+dbcd and Glucose3.0 by testing 2015 and 2017 SAT competition instances.The validity and advantage of new solvers are analyzed from many aspects,such as the number of solved instance,the average decision number,the average conflict number,the solving time and so on.