Research On Branching Heuristic Strategy Based On CDCL For SAT Problem

The problem of satisfiability of the propositional logic formula?SAT problem?is to give a conjunctive normal form and judge whether there exists an assignment to make the conjunctive normal form satisfiable.SAT problem is a core issue in computer science and engineering,Artificial Intelligence,computer vision and computer aided design.It is also the first NP complete?Non-Deterministic Polynomial-Complete,NPC?problem that has been proved.Because of this,it is valuable to study the SAT problem and improve the efficiency of the solver.The algorithms for solving the SAT problem are divided into complete algorithm and incomplete algorithm.The characteristic of the complete algorithm is that it provides a model when the problem is satisfiable;when not satisfied,it gives proof.Based on the advantages of complete algorithm,this paper takes CDCL?Conflict Driven Clause Learning,CDCL?algorithm as a framework to study the relationship among the following main processes of CDCL algorithm:decision making,conflict analysis,learning clause and backtracking.The success of SAT solvers can be largely attributed to the ability to learn from wrong assignment,to quickly delete search space and to focus primarily on those"important"variables^[1].Therefore,this paper focuses on the decision making and conflict analysis in the CDCL algorithm.The main findings obtained are as follows:1.When a logical formula in a propositional logic is entered into a database in the form of CNF,the basis for selecting"important"variables is the number of variables appearing and the length of the clause containing the variable.Since shorter clauses are more difficult to satisfy,short clauses are given priority.Accordingly,the variables in the short clause are"important".In light of these information,the initial scoring and sorting methods of variables are given.2.When conflict occurs,that is,the current assignment makes some clauses unsatisfiable and the value of the corresponding variables in those clauses that participate in the conflict is higher than those that do not participate in the conflict,thus at this stage,the information carried by these clauses or variables are considered to depict the contribution value of the variables.On the basis of the experimental data in the bibliography,we can see that the exponential growth is pretty good.Therefore,according to the length of the learning clause,segmenting is performed.In each segment,we give a constant plus an exponential function to do the sorting.3.Based on the above research results,a new branching heuristic strategy is proposed and applied to the glucose4.0 algorithm.It is tested with the SAT competition examples in2016,2017and the SATLIB examples.the parameters are modified according to the effect.The results show that CLVDL is better to some extent than the original solver glucose4.0.