Study On Heuristics Of Solving SAT Problem Based On CDCL

In the logic problem,the Boolean satisfiability problem(i.e.,the SAT problem)has been widely concerned.The SAT problem is to determine whether a propositional logic formula given in the form of Conjunctive Normal Form(CNF)can be made to evaluate to true by assigning Boolean truth values to the variables in the formula,or proving that the formula is unsatisfiable.SAT problem is the first NP-complete problem that has been proven in algorithmic complexity.At present,the SAT problem is a research hotspot in many fields,such as Theorem Proving,Automated Reasoning,Model Checking,Electronic Design Automation,Computer Aided Design and so on.Therefore,the research on the SAT problem is not only significant in theory,but also has great value in practical applications.Incomplete and complete algorithms are the two main types of algorithms for solving SAT problems.The incomplete algorithms are mainly based on the stochastic local search,while the complete algorithms are mainly based on the backtracking search.The advantage of the complete algorithm is that it can certainly determine the satisfiability of the SAT problem.At present,the most popular complete algorithm is the CDCL algorithm.This paper is based on the framework of the CDCL algorithm,and has achieved the following research results:1.Inspired by EVSIDS and ACIDS algorithms,a DRB(Dynamic Reward Based Branching Heuristic)algorithm was proposed.The DRB algorithm updates the activity score of the variable which integrated with the variable decision level,conflict level,conflicts and the conflict frequency of variable whenever a conflict occurs.On this basis,the decision of a branching variable of the solver is thus guided.2.The level distance was introduced according to the LBD of the learnt clause,and it is used to evaluate the quality difference between the learnt clauses with the same LBD.On this basis,a LDCR(Level Distance Based Clause Reduction Heuristic)strategy was proposed to guide the clause database management of the solver.3.The DRB algorithm and the LDCR strategy were embedded into the SAT solvers Glucose 3.0 and MapleLCMDistChronoBT,and six new SAT solvers are obtained.Two experiments were mainly carried out.The first experiment was the comparison experimentbetween the improved solvers based on Glucose 3.0 and Glucose 3.0.The SAT competition instances in 2015,2016 and 2017 were selected for testing.The second experiment was the comparison experiment between the improved solvers based on MapleLCMDistChronoBT and MapleLCMDistChronoBT,and selected the 2018 SAT competition instances for testing.The results of the improved solvers were compared with the the original solvers.The experimental results show that the performance of the improved solvers are higher than the original solvers.Therefore,the two new heuristics proposed in this paper can effectively improve the CDCL algorithm and the performance of the SAT solver.