Study On Optimization Of Branching Strategy In CDCL Algorithm Based On Variable Features

Satisfiability problem(Satisfiability Problem,SAT problem)is a classical problem in mathematical logic and an important research direction of automatic reasoning.In terms of theoretical application,many NPC problems(Non-deterministic Polynomial Complete),such as coloring problems,Euler's loop problems,traveling salesman problems and so on,can be converted into SAT problems to be solved.In practical applications,some practical problems can be solved by logically transforming into SAT problems,such as computer-aided design and manufacturing,and artificial intelligence.In addition,an indispensable link in formal verification is the determination of the satisfiability of logical formulas.Therefore,the study of SAT problems not only has important theoretical value but also has wide application prospects.At present,the algorithms for solving SAT problems mainly include complete algorithm and incomplete algorithm.The complete algorithm is mainly based on the idea of exhaustion and backtracking,and the incomplete algorithm is mainly based on the idea of stochastic local search.The CDCL(Conflict driven clause learning)algorithm developed based on the DPLL(Davis Putnam Logemann Loveland)algorithm is a representative and complete algorithm,and is also a mainstream algorithm for solving the SAT problem.Its solution structure mainly includes preprocessing,clause learning,branching decision and restart.In the CDCL algorithm solution framework,as the search proceeds,the solver will continuously record the causes of the conflict,which can effectively prevent the solving process from entering the same conflict space again.And the research experiments show that the key to the efficiency of the CDCL algorithm is its ability to learn conflicts.Under the framework of CDCL algorithm,this paper mainly does the following two aspects for the conflict-based branching heuristic:1.In order to reduce the phenomenon that the solver has too many random assignments in branching heuristic,this paper proposes a branching strategy based on variable characteristics.The new strategy combines the LBD of the learning clause and number of conflicts with the VSIDS branching heuristic,which is called BVA(Breaking the Balance of Variable Activity)branching strategy.The BVA branching heuristic strategy does not change the overall growth trend of variable activity values during the branching decision process,but only slightly increases the activity values of some variables.This not only retains the original advantages of the VSIDS branching strategy,but also helps reduce the randomness of the VSIDS branching strategy,making the selection of branching variables more accurate.2.Based on the above work,the BVA branching strategy is formed into an algorithm,and embedded into the famous solver Glocose4.1 and the 2018 international competition champion Maple?LCM?Dist?Chrono BT,respectively forming the Glocose4.1+BVA solver and Maple?LCM?Dist?Chrono BT+BVA solver.In the experimental part,the experiment selects2017-2019 competition instances for comparative testing.The test results show that the improved two solvers are superior to the original solvers in terms of solving efficiency and solving ability,especially it has obvious advantages in solving unsatisfiable problems.