The Research Of Branch Variable Heuristic Algorithm In CDCL SAT Solver

One of the core issue in the field of artificial intelligence and computer science is satisfiability.It is a NP-complete problem proved by Stephen Cook in terms of time complexity of algorithm in 1971.Above all,NP-complete problem is on the top of seven mathematical problems.All these show that it is hard to solve.However,it is widely used in the field of constraint satisfiability,mathematical logical,automated reasoning,software as well as hardware validation etc.Thus,the research to the decoding of SAT is of great importance in theoretical and application.So far,there are mainly two kinds of algorithm to solve SAT problem:one is complete algorithm;the other is incomplete algorithm.CDCL(Conflict Derive Clause Learning)is a popular complete algorithm based on DPLL and the solver corresponding to it is called CDCL SAT solver.There are mainly three stages for these solvers to solve SAT problem.They are respectively stage of branching variable selection,stage of boolean constraint propagation,and stage of conflict analysis as well as clause learning.Among them,branching variable heuristic algorithm of variable selection stage can be summed up in two categories:the first is the heuristic algorithm that does not combine with conflict analysis process,such as JW(Jeroslow-Wang)algorithm and DLIS(Dynamic Larger Independent Sum)algorithm etc;the second is the heuristic algorithm that combines with conflict analysis process,such as the classical VSIDS(Variable State Independent Decaying Sum)algorithm,CHB(Conflict History--based Branching Heuristic)and LRB(Learning Rate Branching)algorithm etc.It is widely acknowledged that the first algorithm need huge computational cost while the second fails to use the information in clause as well as does not reflect the difference between variable appeared learning clause.Therefore,in order to reduce the shortcomings of these algorithms and choose a better branch variable,this thesis proposes a new branch variable heuristic algorithm based on the frame work of classical VSIDS algorithm,and designs a sat solver based the new algorithm named Modified-MiniSat.In this thesis,the new algorithm is proposed by doing the following four works:1.In terms of general SAT problem,short clause is harder to be satisfied than long clause.So it is necessary to introduce a weight with respect to clause length clause,and defining the weight of variable in clause set.Then depicting variable activity in the initial clause set by the variable weight.Last make it accurately reflect the variable activity accurately at the beginning clause set as much as possible.2.It has designed a reward function related to decision level.When learning clause is added to the clause set along with the process of problem solving,the activity of variable appeared in learning clause can obtain a reward according to variable decision level.By this way it can increase variable activity in learning clause.3.Based on the two works above,branching variable heuristic algorithm based on reward is proposed,and this algorithm is used to replace original one in MiniSat solver.Then a new solver Modified-MiniSat is designed.4.Take a contrast test between Modified-MiniSat solver and MiniSat solver by instance in 2013 SAT competetion as well as 2016 SAT competetion.And then evaluate as well as analyze the effectiveness of new variable heuristic algorithm.