基于CDCL的SAT问题求解算法研究

发布时间：2018-05-05 11:43

本文选题：命题逻辑 + 可满足性问题　；参考：《西南交通大学》2016年硕士论文

【摘要】：人工智能领域中,研究命题逻辑公式的可满足性(SAT)问题具有十分重要的作用。随着科学、技术、社会等领域的发展,需要解决的SAT问题的规模变得越来越大,而传统单一的算法无法适应这些大规模的SAT问题。因此一些针对大规模的SAT问题的求解器应运而生,如Chaff、zChaff、Minisa、Lingeling等诸多著名求解器。这些求解器都并非由单一的算法构建,而是在传统的DPLL等算法的基础上构建的一套系统,如CDCL求解器,其包含多个决策过程,在算法过程中不断的改进学习和调整,以更为高效的解大规模的SAT问题。这些求解器主要分为如下几个部分,分别是变量决策、冲突分析、子句学习和回溯机制。而其中的变量决策过程在整个算法构架中占有十分重要的地位,一个好的变量决策策略可以减少冲突的产生,大量节省求解时间,因此研究变量决策过程的策略具有较为重要的意义。本文主要结合CDCL求解器构架,做了如下几个方面的研究工作：1、本文提出一种启发式策略,根据所给子句、文字数量和出现次数,定义文字相关系数、子句相关系数,进而对初始变量决策过程提供依据；2、基于定义的相关系数,给定冲突状态定义,根据冲突状态下的总的冲突数不断减少的原则,进而定义冲突稳定状态,根据冲突稳定状态制定回溯回退机制策略；3、基于以上两种策略,结合CDCL求解器形成求解SAT问题新算法(Conflict-SAT),并采用SAT竞赛中的问题以及TPTP问题库中旅行商问题进行实例测试,并对测试结果进行分析比较。
[Abstract]:In the field of artificial intelligence, it is very important to study the satisfiability of propositional logic formulas. With the development of science, technology, society and other fields, the scale of SAT problem that needs to be solved becomes larger and larger, but the traditional single algorithm can not adapt to these large-scale SAT problems. Therefore, some solvers for large-scale SAT problems emerge as the times require, such as many famous solvers such as ChaffitzChaff-minisaLingeling and so on. These solvers are not constructed by a single algorithm, but a set of systems based on traditional DPLL algorithms, such as CDCL solvers, which contain multiple decision-making processes and are constantly improved and adjusted in the algorithm process. In order to solve large scale SAT problem more efficiently. These solvers are divided into the following parts: variable decision, conflict analysis, clause learning and backtracking. The variable decision process plays a very important role in the whole algorithm framework. A good variable decision strategy can reduce the conflict and save the solving time. Therefore, it is of great significance to study the strategy of variable decision process. In this paper, combining the CDCL solver architecture, we do the following research work: 1. This paper proposes a heuristic strategy, which defines the text correlation coefficient, clause correlation coefficient and clause correlation coefficient according to the given clause, the number of words and the number of occurrence times. Then it provides the basis for the decision-making process of initial variables, based on the definition of correlation coefficient, given the definition of conflict state, according to the principle that the total number of conflicts in the conflict state is decreasing, and then define the stable state of conflict. Based on the above two strategies, a new algorithm for solving SAT problem, Conflict-SAT, is developed according to the conflict stable state. Based on the above two strategies, the problem in SAT competition and the traveling salesman problem in TPTP problem database are used to test. The test results are analyzed and compared.
【学位授予单位】：西南交通大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：TP18

【相似文献】