Research On Branching And Deletion Strategies Based On CDCL Algorithm

The CDCL(Conflict Derive Clause Learning)algorithm is a complete algorithm for solving the Satisfiability Problem(SAT).The basic stages of the CDCL algorithm are:preprocessing,,branching decision,Boolean Constraint Propagate(BCP),non-sequential backtracking and random restart.Branching decision is one of the important stages in CDCL algorithm.The branching strategy is one of the most important stages in CDCL algorithm,and the branching strategy in CDCL algorithm is the VSIDS(Variable State Independent Decaying Sum)strategy.Based on VSIDS strategy,a branching strategy based on added weight decision level is proposed in this paper.The new branching strategy can make short clauses and new learnt clauses get priority.The new branching strategy is composed of the initial variable decision strategy and the conflict variable decision strategy.The initial variable decision strategy is to assign the variables in the short clauses preferentially when initially selecting variables,so that the short clauses are preferentially satisfied,and the conflict variable decision strategies are to assign the variables in the new clauses preferentially when choosing variables after conflicts,so that the new clause is preferentially satisfied and the same search space is avoided.When the new branching strategy is embedded in the CDCL algorithm,the experimental results show that the algorithm was optimized.Not only a branching strategy based on added weight decision level is proposed in the paper,but also a deletion strategy based on weighting conflicts times is proposed.The clause deletion can optimize the storage space by deleting some less-valued clauses and retaining the learnt clauses that have a greater impact on the conflict.The number of conflicts is an important indicator to evaluate the quality of learnt clauses.The more times that the variables in the clauses participate in conflicts,the higher the quality of the clauses is.Deleting low quality learnt clauses can be used to optimize the storage space.When the newdeletion strategy is embedded in the CDCL algorithm,the experimental results show that the algorithm is optimized.The main research work is:1.For a group of clauses,there are more words in the long clause.Therefore,when assigning a variable,the long clause is easier to be satisfied than the short clause.Therefore,based on the idea of preferentially satisfying the short clause,and consideration of the length of the clause,the score function of variable weight is designed and a new initial variable decision strategy is given.2.In the CDCL algorithm,when the Boolean constraint propagation encounters a conflict,it is a non-sequential backtracking.For the conflict,the encouraged value of the conflict-related variable can be given according to the difference between the conflicting layer and the decision-making layer of the variable,and the priority can be given to short learnt clauses,therefore,combining the length of clauses with the difference between decision-making and conflicting layers,the calculation function of clause weights is constructed,and a new decision-making strategy of conflict variables is proposed.3.The contents of the previous two parts is combined to form a new branching strategy,and it is embbed in the CDCL algorithm to form a new algorithm.4.The clauses learned by the conflict analysis will be added to the clause library when a conflict occurs each time.As the number of clauses increases,the storage space becomes smaller.Therefore,in order to optimize the storage space,it is necessary to delete the less-valued clauses.The more the number of clauses participating in the conflict is,the greater the impact on the conflict is.Therefore,a new deletion strategy is proposed based on the average times of clauses conflicts,and it is embbed in the CDCL algorithm to form a new algorithm.5.The new branching strategy and the new deletion strategy are respectively embedded in the CDCL algorithm,then two new algorithms both are combined with Glucose4.1 or thesolver MapleLCMDistChronoBT,which can improve the new solver Glucose4.1+awdl or the solver ChronoBT+awdl,the solver Glucose4.1+ dwct or the solver ChronoBT+dwct.Two new strategies both are embedded in the CDCL algorithm,then the new algorithm is combined with Glucose4.1 or the solver MapleLCMDistChronoBT,which can improve the solver Glucose4.1+awdl+dwct or the solver ChronoBT+awdl+dwct.The SAT international competition examples are used to test and the effectiveness of the new solver is showed by experimental results.