【作者】 徐成刚；

【导师】 易军凯；

【作者基本信息】 北京化工大学 ， 计算机应用技术， 2007， 硕士

【摘要】 可满足性问题(简称SAT问题)是NP-hard问题，它是当前运筹学、人工智能和计算机科学的热点领域，解决SAT问题具有突出的理论价值和应用价值。解决SAT问题的传统算法往往要占用很长时间和大量的内存，而最后往往还不能得到满意的结果。为了提高SAT问题解决算法的性能，本文对于SAT问题做了对已有算法的分析研究、约束规划算法分析、约束规划算法的UML建模和约束规划算法来求解SAT问题的实验分析等方面的探讨，主要的内容有：对SAT问题已有的主要算法及存在的问题进行了研究，总结了提高算法性能和跳出局部陷井所用的策略或机制。对局部搜索算法的实验分析，针对局部搜索算法的灵活性、随机性和参数化等特点，深入探讨了相应的算法实验分析所涉及的算法性能度量、性能比较和参数调优等基本问题。提出了综合人工智能中一致性算法和启发式搜索算法，采用约束推理的方法的约束规划算法。本文通过对约束规划算法事件触发机制的分析和UML的建模，从而提高了搜索效率，提出了解决SAT问题。结合SAT问题特殊知识，提出了在启发式算法和一致性算法的基础上，采用整数有限域的优化和搜索策略，对非线性约束问题在其内部制作二叉树进行搜索的约束规划算法，描述了first_fail的分支策略设计和算法描述，提供了性能比较、参数优化等等多种目的的实验结果。实验结果表明约束规划算法能有效解决SAT问题和显著提高性能。更多还原

【Abstract】 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.更多还原