| The satisfiability problem(SAT)is one of the core issues in the field of computer and artificial intelligence.S.A.Cook first demonstrated in 1971 that the SAT problem is NP-complete,that is,any NP problem can be statistic to the SAT problem in polynomial time.The solution of SAT problem can help solve the NP problem;the SAT problem has been widely applied to many fields,such as mathematics,computer science,formal verification,etc.Therefore,the research of SAT problem has important theoretical value and application prospects.The algorithm for solving SAT problem can be divided into complete algorithms and incomplete algorithms according to completeness.Incomplete algorithms take less time to solve the satisfiability problem,but cannot judge the unsatisfiability of the problem;the complete algorithm appears earlier than the incomplete algorithm,and it takes a relatively long time to solve the satisfiability problem,but it can be proved when the problem is unsatisfiable.The CDCL algorithm is a popular complete algorithm,it is developed by the classic complete algorithm DPLL algorithm.Most of the efficient algorithm is based on the CDCL algorithm.This paper studies the branching strategy and the deletion strategy based on the CDCL algorithm.The work done is as follows:1.According to the influence of clause length on the initial stage branch variable,the initial stage variable score function is introduced to provide the basis for the initial stage branch strategy.According to the influence of the LBD value of the clause on the branch variable,the post-conflict variable score function is introduced to calculate the score of the post-conflict variable.Based on the introduction of initial stage variable score and post-conflict variable score function,a branch strategy is proposed,that is Clause LBD Based Heuristic(CLBH).2.According to the influence of learning clause LBD and length on deletion strategy,the concept of literal average LBD is introduced,as a criterion for evaluating learning clauses,a deletion strategy-based literal-based average LBD deletion strategy(LABCD)is proposed.3.The branching strategy formation algorithm based on the clause LBD is embedded in the famous solver Glucose4.1 to obtain the solver Glucose4.1+CLBH.The examples in SATLIB Benchmark were selected for comparison test.The number of successful solutions,the time spent on solving,the number of conflicts,the number of decisions,the number of propagations,to show the effectiveness and performance of the solver Glucose4.1 + CLBH.4.The deletion strategy and formation algorithm based on the average literal LBD is embedded in the famous solver Glucose4.1 to obtain the solver Glucose4.1+LABCD.Compare the examples in the Main Track in the 2017 and 2018 SAT competitions,and analyze the number of successful solutions,the time spent on the solution,the number of conflicts,the number of decisions,the number of propagations,to illustrate the effectiveness and performance excellence of the solver Glucose4.1+LABCD. |
