CDCL SAT求解器中的分支变量启发式算法研究

发布时间：2018-02-11 05:44

本文关键词： SAT问题分支变量启发式算法变量活性奖励函数　出处：《西南交通大学》2017年硕士论文　论文类型：学位论文

【摘要】：命题逻辑公式的可满足性问题(即SAT问题)是人工智能和计算机科学领域的核心问题之一。1971年Stephen.Cook从算法时间复杂度的角度证明了 SAT问题是NP完全问题,而NP完全问题在七大数学难题中排在首位,可见SAT问题是一类非常困难的问题。由于SAT问题在约束可满足问题、数理逻辑、自动推理、软件及硬件验证等领域具有广泛的应用,因此研究SAT问题的求解具有重要的理论价值和应用前景。目前求解SAT问题的算法大致可归为两类:一类是完备的求解算法;一类是不完备的求解算法。基于DPLL算法的CDCL(Conflict Derive Clause Learning)算法是目前比较流行的完备算法,由该算法设计的求解器(CDCLSAT求解器)的求解过程主要分为三大阶段,分别是分支变量选择阶段、布尔约束传播阶段和冲突分析及回溯阶段。其中,变量选择阶段的分支变量启发式算法可归结为两类:第一类是没有与冲突分析过程相结合的启发式算法,比如JW算法(Jeroslow-Wang)、DLIS(Dynamic Larger Independent Sum)算法等;第二类是与冲突分析过程相结合的启发式算法,比如VSIDS(Variable State Independent Decaying Sum)算法、CHB(Conflict History-based Branching Heuristic)算法、LRB(Learning Rate Branching)算法等。由于第一类分支变量启发式算法计算代价大,第二类分支变量启发式算法未能很好地利用子句固有的信息以及未体现出学习子句中变量的不同。故为了尽可能减少这些算法的不足以及选出更好的分支变量,本文以经典的VSIDS算法为基本框架设计了基于奖励的分支变量启发式算法,并用该算法代替MiniSat求解器中的分支变量启发式算法,得到新的求解器一Modified-MiniSat 求解器。本文就新算法的提出主要做了以下四方面的工作:1.对于一般的SAT问题,短子句较长子句更难被满足,依据子句的长度赋予每个子句权重,进而给出变量在子句以及子句集中的权重的定义。并用变量在子句集中的权重刻画变量的活性,从而尽可能准确地反映变量在子句集中的活跃度。2.设计了与决策层有关的奖励函数。在问题求解过程中,当学习子句添加到子句集时,根据学习子句中变量所在决策层的不同,奖励变量,以便增大学习子句中的变量活性。3.基于上述两方面的工作,给出了基于奖励的分支变量启发式算法,并用该算法代替MiniSat求解器中的分支变量启发式算法,设计了相应的求解器-Modified-MiniSat求解器。4.选择2013 SAT竞赛以及2016年SAT竞赛例作为测试例,对Modified-MiniSat求解器和MiniSat求解器做对比测试,通过分析实验结果得知Modified-MiniSat求解器有一定的优势,从而说明了改进后的分支变量启发式算法的有效性。
[Abstract]:The satisfiability problem of propositional logic formula (SAT problem) is one of the core problems in the field of artificial intelligence and computer science. In 1971, Stephen.Cook proved that the SAT problem is NP-complete problem from the angle of algorithm time complexity. The NP-complete problem ranks first among the seven mathematical problems. It can be seen that the SAT problem is a kind of very difficult problem. Because the SAT problem has a wide range of applications in the fields of constrained satisfiability problem, mathematical logic, automatic reasoning, software and hardware verification, etc. Therefore, it has important theoretical value and application prospect to study the solution of SAT problem. At present, the algorithms for solving SAT problem can be classified into two categories: one is complete algorithm; One is incomplete algorithm. The CDCL(Conflict Derive Clause learning algorithm based on DPLL algorithm is a popular complete algorithm. The solver designed by this algorithm is divided into three stages. They are branch variable selection, Boolean constraint propagation and conflict analysis and backtracking. In the stage of variable selection, the branch variable heuristic algorithm can be divided into two categories: the first is a heuristic algorithm that does not combine with the conflict analysis process, such as the JW algorithm Jeros low-Wangli dynamic Larger Independent Sumet, etc. The second is the heuristic algorithm combined with the conflict analysis process, such as VSIDS(Variable State Independent Decaying summing (VSIDS(Variable State Independent Decaying summing) algorithm and so on. The second kind of heuristic algorithm of branch variable can not make good use of the inherent information of clause and the difference of variable in learning clause, so in order to minimize the deficiency of these algorithms and select better branch variable, In this paper, the classical VSIDS algorithm is used as the basic framework to design a heuristic algorithm for branching variables based on rewards, and the algorithm is used to replace the branch variable heuristic algorithm in the MiniSat solver. A new solver, Modified-MiniSat solver, is obtained. In this paper, the following four aspects of the proposed algorithm are mainly done: 1. For a general SAT problem, the short clause is more difficult to satisfy than the long clause, and each clause is given weight according to the length of the clause. Then the definition of the weight of variable in clause and clause set is given, and the activity of variable in clause set is characterized by the weight of variable in clause set. The reward function related to the decision level is designed. In the process of solving the problem, when the learning clause is added to the clause set, the variable in the learning clause is different from the decision layer in the learning clause. Reward variables in order to increase the activity of variables in the learning clause. 3. Based on the above two aspects of work, a heuristic algorithm of branch variables based on reward is presented, and the heuristic algorithm of branch variables in MiniSat solver is replaced by the heuristic algorithm. The corresponding solver -Modified-MiniSat solver .4.Selects the 2013 SAT contest and the 2016 SAT contest as test examples, and makes a comparative test of Modified-MiniSat solver and MiniSat solver. Through the analysis of the experimental results, it is found that Modified-MiniSat solver has some advantages. Thus, the effectiveness of the improved heuristic algorithm for branch variables is demonstrated.
【学位授予单位】：西南交通大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：O141

【相似文献】