Research On Algorithms For Solving Satisfiability Problem

Satisfiability Problems(SAT)is the problem of determining if there exists an assignment of truth values to the variables of a given Boolean formula.The maximum satisfiability problem(MAX-SAT)is the optimization form of SAT problem which is the problem of determining the maximum number of clauses that can be made true by an assignment of truth values to the variables of the formula.Many problems in the real world can be modeled and solved by SAT problem or MAX-SAT problem.Conflict driven clause learning algorithm(CDCL)and local search(LS)are important algorithm for solving these problems.The performance of CDCL algorithm can be improved by invoking the appropriate branch strategy.The computational efficiency of LS algorithm can be improved by introducing appropriate transformation strategy.This paper mainly studies the improved algorithm of SAT problem and MAX-SAT problem,and the specific work is as follows:(1)In CDCL algorithm,an algorithm of dynamic scheduling branch strategy is proposed by evaluating the effectiveness of branch strategy.State of the art CDCL algorithm combines multiple branch strategies.Selecting the appropriate branch strategy can accelerate the solving efficiency.The solving process is divided into two stages.In the evaluation stage,each branch strategy is scored based on the quantity,quality and time cost of learning clauses in the stage.In the non-evaluation stage,the branch strategy with the highest score is selected for solving.(2)A new variable pick strategy-stopping time strategy is proposed.The variable pick strategy in LS algorithm is very important,and the efficient strategy should avoid local optimum as much as possible.The stopping time strategy realizes the approximation of the variable pick strategy by using stopping time,which makes the variable pick more diversified and reduces the local optimal.The experimental results show that the stopping time strategy improves the performance of the classical CCA solver.(3)Analyzed the variable pick strategy of LS algorithm solving the MAX-SAT problem,this study presents a variable pick strategy base on information of unsatisfied clause.In this strategy,the variable rollover is picked from the maximum score or the optimal set of unsatisfied clauses,rather than from a randomly picked unsatisfied clause.Experimental results show that this strategy is effective.