合取范式的可满足性完备算法研究与实现
开篇：润墨网以专业的文秘视角，为您筛选了一篇合取范式的可满足性完备算法研究与实现范文，如需获取更多写作素材，在线客服老师一对一协助。欢迎您的阅读与分享！
摘要：把可满足性算法应用到合取范式中并加以分析，借助改进的数据结构实现该算法。在四色图着色中应用该算法找出一组图着色方案，并与DPLL算法进行了性能比较。
关键词：合取范式；可满足性；布尔约束推导；冲突分析
DOIDOI：10.11907/rjdk.161162
中图分类号：TP312
文献标识码：A文章编号：16727800（2016）010003203
0引言
合取范式的可满足性问题（SAT）是理论计算机科学和人工智能中的著名问题。寻求其有效算法一直都是计算机理论及实际应用的重要任务。SAT算法又分为完备算法和不完备算法两大类。1960年，Davis和Putnam[1]提出的DPLL算法是最早提出的完备算法，它有变量决策、赋值过程、回溯过程等几个主要机制。此后提出的SAT算法大都基于DPLL算法[23]，从变量决策和回溯机制来提高算法的性能[4]。此外，为了减少回溯次数，提出了一种冲突分析机制[5]，可满足性完备算法即由这几个部分组成[6]。
目前SAT以完备算法为主，算法有两种：一是1960年由Davis和Putnam提出的DPLL算法以及改进版；另一个是Bart Selman提出的贪婪搜索算法。以上算法都只停留在算法思想上，难于实际应用。SAT算法的改进对计算机科学的发展有着重要作用。
本文研究了基于DPLL的SAT算法，采用改进的数据结构实现了DPLL算法的几个主要机制。运用这几个机制实现了基于CNF的可满足性问题完备算法，并将该算法应用到地图着色问题中，与原DPLL算法相比，效率有所提高。
1基于CNF的SAT算法
1.1算法总体框架
基于CNF的SAT算法主要有读取文件、变量决策、回溯过程、冲突分析等几个过程，算法框架如图1所示。SAT算法的实现包含5个关键机制，分别为分支决策算法decide（）、冲突分析算法diagnose（）、布尔约束推导deduce（）、回溯机制backtrace（）和判定计算compute（），它们共同影响着整个算法效率。其中，判定计算是算法的核心。
SAT算法中的决策变量选择直接影响着BCP过程，进而影响算法的效率。常用的SAT算法在决策变量的选择上有多种方法，如动态排序、最短子句出现频率最大JW策略和动态筛选策略等。
本算法使用动态筛选策略。动态筛选策略的核心思想是：对每个变量打分，以分数最高的变量作分支决策变量。打分规则为：在CNFa中对变量p打分。在CNFa中对p赋值为真，得到CNFh；对CNFh使用单子句规则降维，直至不能再降为止，最后结果记为CNFd。在CNFa中对p赋值为假，得到CNFc；对CNFc使用单子句规则降维，直至不能再降为止，最后结果记为CNFd。改进规则为：如果当前节点是根节点，那么对每个变元用上述的打分规则打分，直至打分完毕；否则对每个变元考虑是否照抄它在当前的结点父节点的得分。当变元在父节点对p打的分数小于一个绝对常数时，就照抄在父节点对p打的分数，否则在当前节点对它重打分。
回溯函数backtrace的设计使用基于冲突学习的非同步回溯，是一种智能回溯机制。
判定计算函数是整个算法的框架，它把各个算法机制联系起来，控制着整个算法的调度。通过冲突分析和分支决策，把决策变量选取后，利用DPLL算法的单子句规则和分裂规则化简合取范式，对决策变量赋值，并存放在EV中。结果集合包含限制集合中的某一组集合，也就是发生冲突时需要调用回溯函数，回溯到第0层且集合为空，此时问题是不可满足的；或者限制集合中的每个元素都被计算过且没有发生冲突，此时问题是可满足的。流程如图2所示。
1.2决策策略算法
决策策略算法与传统的SAT算法不同之处在于其使用的是动态筛选策略。动态筛选策略能快速筛选出绝大多数的高价值变量，并将这些变量限定在很小的范围内。无论规模大小，这种策略都能使算法性能提高。
查找分支决策变量是SAT算法的关键问题之一，它由限制集合CT中的每一个元素与结果集合的补集所决定。这是一个循环过程，循环次数由当前限制集合中活跃子句的数目确定。不断循环这个过程，直到找到最小的补集，在该补集中选择一个决策变量。如果出现补集为空则需要回溯。分支决策实现流程如图3所示。
1.3改进的BCP过程
BCP就是变量不断被赋值，子句中未赋值的变量数不断减少。由于BCP过程占用了整个算法执行过程的80%以上，所以BCP过程对于算法效率有着显著的影响。
传统的BCP方法是：给一个变量赋值时，用穷举法搜索所有子句，找出由于该变量的赋值而变为单子句的子句，记录它索引指针并对其赋值。本算法使用改进的BCP过程，它是一种动态筛选过程，在CT中确定了决策变量p后，只需要将MN[p]放入EV中即可，这样能快速选出待赋值变量。
1.4冲突分析和回溯机制
本算法采用的冲突分析和非同步回溯算法，是一种蕴含点算法。蕴含图中有一个特殊节点，即冲突节点，以冲突节点为终点的边对应所有文字为0的子句。
该算法没有使用传统的回溯思想，它将变量设置成不同判定级别。在属于当前判定级时，在第一独特蕴含点赋值，导致冲突变量路径的节点都划分到冲突部分，而把其它节点划分到原来的部分，这样就可以得到一个尽可能接近冲突变量的划分，从而获得更有效的学习子句。
对冲突结点的处理及回溯问题，是所有赋值变量将自身的逻辑值取反、作为对应文字的逻辑符号而产生的。当它被加入到子句库中时，在当前赋值状态下其逻辑值肯定是假，也就是一定会发生冲突，解决这一冲突必须对分支变量进行回溯操作。所有分支变量的逻辑值都是由布尔约束推导算法通过各种方式进行逻辑推导而得出的。
2在四色图着色问题中的应用
2.1四色定理与四色图着色问题
根据四色定理，任意一个地图都可以用4种颜色染色，使得任意两个相邻的地方颜色不同。以中国地图为例，使用该算法用A、B、C、D四种颜色为中国地图着色，使相邻的省不能有相同的颜色。本文将基于CNF的SAT算法应用于四色图着色。
2.2问题编码
中国地图中有34个省域。先把34个省域看成34个点，编号为1到34，把相连部分看作两个点之间有边相连，每个点最多有A，B，C，D四种颜色可选，将问题转化成CNF形式，用136个变量表示这个合取范式。假设这136个变量为V1，V2，…，V136，那么其表示的含义为：
当程序规模很大时，本文算法的平均冲突次数有了一定程度的提高，但仍然有点大。可见，对SAT完备算法的研究是一个长期的过程。
参考文献参考文献：
[1]M DAVIS，H PUTNAM.A computing procedure for quantification theory[J].Journal of ACM7，1960（1）：1620.
[2]黄文奇，王磊.一种采用继承策略的李初民算法的改进[J].江汉石油学院学报，2001（3）：254259.
[3]RAINER SCHULER.An algorithum for the satisfiability problem of formulas in conjuctive form[J].Science Direct，2004（8）：12541260.
[4]张德富.求解难可满足性问题的混合算法[J].小型微型计算机系统，2003（4）：112116.
[5]徐成刚.可满足性问题的约束规划算法研究[J].北京化工大学学报，2007（5）：2629.
[6]许有军.基于扩展规则的若干SAT问题研究[J].吉林大学学报，2011（6）：3638.