Study Of Satisfiability Solving Systems And Application Based On Contradiction Separation Based Multiple Dynamic Automated Deduction

Satisfiability(SAT)problem is a well-known problem in computer science theory and artificial intelligence.In the field of theoretical application,numerous NP complete problems,such as coverage problems,packing problems,routing problems scheduling problems,etc.,are converted to SAT problem in polynomial time.In the field of practical application,many practical problems can also be solved by transforming different coding techniques into SAT problems,such as combinatorial optimization problems,software formal verification,hardware formal verification,model verification and planning problems in the field of artificial intelligence.Therefore,it is of great theoretical value and application value to study efficient algorithms for solving SAT problems.Many research scholars have carried out related research on the algorithm of solving SAT problem.DPLL algorithm is a classical and complete algorithm for solving SAT problems.CDCL algorithm developed on the basis of DPLL algorithm has become the solving framework of current mainstream SAT solver.The main development of the CDCL algorithm is to use the resolution principle to generate learning clauses.The automated deduction with contradiction separation proposed by Prof.Yang Xu,breaks through the limitation of traditional resolution principle that only two clauses are involved in each resolution and only two literals are deleted.Based on this,a solver which integrates the automated deduction with contradiction separation rule and CDCL algorithm is developed.This paper presents a series of optimization algorithms for learning clause,heuristic branching,learnt clause evaluation,restart and path identification.First of all,the basic algorithm which combines the contradiction separation rule with CDCL algorithm is realized.The learning mechanism based on implication graph in CDCL algorithm is studied.The relationship between the unique implication points in implication graph is analyzed,and a learning clause algorithm based on the contradiction separation rule is proposed.By analyzing implication graphs,all clauses related to conflict are determined,and then a new learning clause is deduced by using the contradiction separation rule.So that the CDCL solver can get two non-conflict learning clauses each time conflict occurs,and can deduce more implied variables,reduce the decision-making level when conflicts occur,strengthen the pruning ability of the search space and accelerate the solving process.Experiments show that the learning clause generation algorithm based on the contradiction separation rule improves the number of conflicts,the number of decisions,and the number of Boolean constraints propagations,and improves the performance of solving problems in the application benchmark of 2015 SAT and 2016 SAT.Aiming at the problem that CDCL solving algorithm usually uses the score value of each variable in the heuristic algorithm to change the assignment sequence of decision variables.The chapter proposes an algorithm based on the deductive result-oriented to change variable assignment sequence,which finds the set of relevant clauses that meet the requirements in conflict analysis,and utilizes the contradiction separation rule to obtain thedeductive result.Through the deduction result,a decision variable can be directly determined.The decision level of the decision variable is smaller than the current decision level,and then the assignment sequence of variables is changed.And according to the LBD value and the decision level of the deductive result,a method for dynamically updating the reward value of variables is defined.The experimental results show that the algorithm changes the variable assignment sequence more frequently,increases the possibility of finding the solution,and makes each backtrack level smaller,and enhances the reduction of the search space.The improved algorithm also shows better performance for solving satisfiable and unsatisfiable instances.The chapter studies the learnt clause reduction algorithm,analyses the rationality of the reduction cycle,and illustrates the necessity of learnt clause reduction.A learnt clause evaluation criterion based on the length of deduction is proposed.Aiming at the singularity of the evaluation criterion in the existing strategies,a learnt clause evaluation criterion based on average is proposed,which combines the deductive length-based evaluation criterion with the LBD value-based evaluation criterion.This criterion can keep more learnt clauses which are beneficial to the subsequent solving process,delete more useless learning clauses and accelerate the solving process.The experiment verifies that when solving the SAT competition instance,the proposed learnt clause deletion strategy shows the advantage in the total number and solving time.The restart algorithm is studied.Based on the change of conflict decision level in the process of solving,a dynamic restart algorithm based on exponential smoothing is proposed,and the restart is dynamically triggered by comparing the predicted value and the actual value.In view of the existing restart strategy,which monitors one parameter of the solving process to decide whether to restart or not,so the chapter introduces the conflict decision level and LBD value to reflect the state of the current search branch comprehensively.The correlation coefficient between the conflict decision level and the LBD value is analyzed,and the dynamic restart strategy based on regression analysis is proposed.The dynamic restart strategy triggers or delays restart dynamically by comparing the predicted value with the actual value.The experimental results demonstrate that the performance of the proposed dynamic restart strategies is superior to both static restart strategy and dynamic restart strategy.After analyzing the problems of static restart strategy and dynamic restart strategy,an algorithm of dynamically changing variable assignment sequence is proposed.The algorithm dynamically adjusts the score of relevant variables according to the size of repeated assignment sequence before and after restart.Changing the variable score value can change the variable assignment sequence,and then change the search path in order to avoid wasting too much unnecessary solving time.The experimental results show that the proposed algorithm can efficiently identify duplicate assignments trails and deal with it by choosing appropriate decision variable adaptively.At the same time,the experimental results show that the performance of the proposed algorithm is better than that of the well-known solverin international SAT competition.