基于子句权重求解SAT问题算法的研究

发布时间：2018-04-28 03:58

本文选题：SAT问题 + CDCL算法　；参考：《西南交通大学》2017年硕士论文

【摘要】：SAT问题是判断命题逻辑公式可满足性,也是NP完全问题之首,在计算机科学和人工智能等领域有重要的理论和应用价值,成为了这些领域的一个热点研究问题。长期以来,人们对SAT问题的求解进行了深入研究,提出了很多求解SAT问题的算法,其中最流行的要数CDCL算法。基于CDCL算法,有许多的求解器被开发出来,如Chaff、zChaff、Minisat、Glucose、Lingeling等著名求解器。这些求解器都是通过对CDCL算法的变量决策、冲突分析、子句学习、回溯回退等主要部分进行不断地替换和调整而来。本文着重研究了 CDCL算法的决策过程,也对变量决策过程进行改进。在决策过程中考虑了子句长短不一的问题,采用优先满足短子句的思想,利用单子句的蕴含原理和满足较多的短子句方法,尽可能早的产生冲突或减少冲突的产生,提高算法求解SAT问题的效率。基于CDCL算法结构框架,对算法做了相应部分的替换,主要的研究工作如下:1.基于优先满足短子句的思想,依据子句固有的结构信息,满足较多的子句,尽可能减少一些冲突的产生,提高算法求解SAT问题的效率,首先以在子句集中出现频率较多且大多出现在短子句中的变量作为选择前提,结合子句的长度,给出变量在子句中的平均长度的概念及一些相关的性质;然后将变量在子句中的平均长度,与变量出现的次数相联系,设计变量权重的计算函数;最后提出一种初始变量决策策略。2.依据子句长度在决策过程中的影响,以短子句为出发点,为了能够发现较多的单子句,采用单子句的蕴含原理,尽可能早地发现冲突或避免一些冲突的产生,提高算法求解SAT问题的时间效率,首先以生成单子句为目的,结合子句的长度,构造子句权重的计算函数;然后提出一种新的分支变量选择策略。3.基于初始变量选择策略和分支变量选择策略形成两种新算法,在CDCL算法结构框架上分别做了一些相应部分的改进,集成VW-SAT求解器和CW-SAT求解器,并进一步通过2015年SAT竞赛中的竞赛例和SAT问题库测试例,验证了算法的有效性。
[Abstract]:SAT problem is not only the satisfiability of judging propositional logic formula, but also the head of NP complete problem. It has important theoretical and application value in computer science and artificial intelligence, and has become a hot research problem in these fields. For a long time, people have deeply studied the solution of SAT problem, and put forward many algorithms to solve SAT problem, among which the most popular one is CDCL algorithm. Based on the CDCL algorithm, many solvers have been developed, such as the famous solvers such as ChaffitzChaffa Minisatt Glucose Lingeling and so on. These solvers are used to replace and adjust the main parts of CDCL algorithm, such as variable decision, conflict analysis, clause learning, backtracking and so on. In this paper, the decision process of CDCL algorithm is studied, and the variable decision process is improved. In the decision-making process, the problem of different length of clause is considered, the idea of priority satisfying short clause is adopted, the principle of implication of single child sentence and the method of satisfying more short clauses are used to produce conflict or reduce conflict as early as possible. The efficiency of the algorithm for solving SAT problem is improved. Based on the CDCL algorithm framework, the corresponding part of the algorithm is replaced. The main research work is as follows: 1. Based on the idea of first satisfying the short clause and according to the inherent structure information of the clause, it can satisfy more clauses, reduce some conflicts as far as possible, and improve the efficiency of the algorithm to solve the SAT problem. Firstly, the concept of the average length of the variable in the clause and some related properties are given by taking the variable which appears frequently in the set of clauses and mostly in the short clause as the premise of selection, combined with the length of the clause. Then the average length of the variable in the clause is related to the number of times the variable appears, and the calculation function of the variable weight is designed. Finally, an initial variable decision strategy .2. is proposed. According to the influence of clause length in the decision-making process, taking the short clause as the starting point, in order to find more single sub-sentences and adopt the implication principle of single clause, we can find conflicts or avoid some conflicts as early as possible. In order to improve the time efficiency of the algorithm for solving the SAT problem, a new branch variable selection strategy, .3., is proposed, which combines the length of the clause with the length of the clause, and constructs the function of calculating the weight of the clause. Based on the initial variable selection strategy and the branch variable selection strategy, two new algorithms are formed, and some corresponding improvements are made on the framework of the CDCL algorithm, which integrates the VW-SAT solver and the CW-SAT solver. Furthermore, the effectiveness of the algorithm is verified by the competition examples in the 2015 SAT competition and the test examples of the SAT problem library.
【学位授予单位】：西南交通大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：O141

【相似文献】