Study On Hybrid Branching Heuristic Strategy And Learnt Clause Integrated Management Strategy In SAT Solver

Knowledge Representation and Automatic Reasoning is at the heart of the great challenge of Artificial Intelligence.As a general method of knowledge representation,propositional logic provides theoretical support for theorem proving,and verification,compilation and reliability analysis for computer programs.The SAT solver has made an important contribution to improving the computational processability of propositional logic problems.It has achieved remarkable results in solving practical applications.Based on propositional logic the relevant strategies in the SAT solver are researched.This paper proposes a mixed branch heuristic strategy based on decision level and an integrated management strategy based on simplified activity.And they are embedded in the SAT solvers with CDCL(Conflict-Driven Clause Learning)framework.The specific results are as follows:First,during the branch decision process of variables,the variable assignment decision level and the current decision level are used for evaluation.On the one hand,the VSIDS?dl(Variable State Independent Decaying Sum?Decision Level)calculation rule based on the decision level is proposed when the variables took part in the conflict analysis.On the other hand,according to reinforcement learning,the difference between the backtracking level and current decision level is taken as a part of learning rate increment.The LRB?dl(Learning Rate-based Branching?Decision Level)calculation rule based on decision level is proposed when the variables are unassigned during the backtracking process.Then,the above two heuristic calculation rules are embedded in the three solvers with the mixed method of segmentation or alternating.The corresponding hybrid branching heuristic strategy is formed respectively.And a comparative experiment is carried out.The results show that the alternating hybrid heuristic strategy based on the decision layer shows the advantage under the Maple COMSPS solution system,when solving graph coloring and chromatic number of the plan problems.Second,the learnt clause evaluation criterion based on simplified activity is proposed to deal with the computational complexity and limitations of the learnt clauses activity.It is embedded in the Maple LCMDist Chrono BT solver by sorting and marking methods.This new strategy enables easy evaluation and data storage of global learnt clauses.The results show that the integrated management strategy based on simplified activity ranking can improve the solver's solution rate and solve some problems that the original solver cannot solve.