Constraint Planning Algorithm-Based SAT Problems

Satisfiability problems (SAT problems for short) is NP-hard problems, which are well-knowned in areas of Operations Research, Artificial Intelligence and Computer Science nowadays. Solving SAT problem is of great value in theory and application. Algorithms for solving SAT problems take up long run-times and lots of system resources and can't get satisfied results in the end before. To improve the performance of SAT solvers, in this thesis, the study of known algorithms, the analysis of constraint planning algorithm, UML modeling of constraint planning algorithm and the experimental analysis of solving SAT problem by the constraint planning algorithms are discussed. This thesis contains followings:SAT problem is researched in known main algorithms and the already existing problems, summed up the algorithm to improve performance and jumping out of the local strategy or mechanism used by the trap. With The experimental analysis of the local search algorithm, Local search algorithms are flexible, randomized and parameterized, and the corresponding experimental analysis must show how to measure and compare algorithm performance, and how to optimize algorithm parameters. Constraint planning algorithm is proposed to solve SAT problems by integrating consistency and heuristic search algorithm and adopts constraint reasoning. In this thesis, improving the searching efficiency with event analysis of variables narrowing and UML modeling, we propose to solve SAT problem.Combining the special knowledge of SAT problem, we propose the constraint planning algorithm, which is based on heuristic search algorithm and consistency algorithm and adopts finite fields integer optimization and search strategy to search by making binary tree search nonlinear constraint problems in its internal. Experimental results show that constraint planning algorithm can effectively solve SAT problem and improve performance significantly.