启发式将3-SAT化为2-SAT的DPLL算法

论文摘要

可满足性问题（SAT）研究如何判定一个任意给定的逻辑表达式是否存在可满足真值指派。SAT在数理逻辑、人工智能、计算机算法设计与分析以及工程应用等领域有着重要的地位,而且SAT问题是第一个被证明的NP完全问题。3SAT是一类特殊的可满足性问题,它的子句中所包含的文字个数最多只有3个,3SAT也是NP-完全问题之一。它可以从很多实际问题抽象出来,其在逻辑推理、人工智能的专家系统、数据库维护和检索、VLSI设计及检测等领域有广泛的应用,它的广泛的应用背景促使人们对它进行深入细致的研究。目前求解SAT问题的算法分为完全性算法和局部搜索算法。前者主要有穷举法,DPLL算法,松驰法等;后者的代表性算法主要是局部搜索算法,如GSAT。这些算法的一个特点是直接对3SAT判断其可满足性。而本文采取的方法不是直接判定3SAT可满足性的问题,而是将3SAT化为2SAT的问题。因为2SAT是可多项式时间内判定的,所以如果能在多项式时间内将3SAT化为2SAT,那么我们就能在多项式时间内判定3SAT是否可满足。本文将启发式策略与DPLL算法相结合,从快速求解的角度来设计算法。先将原始公式用DP算法化简:用DP算法中的重言式规则、单子句规则、纯文字规则将公式中的重言式、单子句将纯文字消除,如果公式中子句集为空,则公式可满足;如果子句集不为空,但是公式中没有包含3个文字的子句,则说明已经将公式化为2SAT,否则对公式中包含3个文字的子句集分别统计变元正出现与负出现的次数,然后选取正出现与负出现的次数的和最多的变元为消解变元。这样,不仅可以快速地将3SAT化为2SAT,而且有可能直接求得公式的可满足解。但是在此过程中,有可能会出现矛盾子句。对此,我们引入了冲突消解机制来消除矛盾子句。我们采取的是预先探测的方法,也就是在每次的消解过程中搜索有可能会在当次的消解过程中产生矛盾子句的子句集,然后对消解变元赋予适当的值,消除矛盾子句。

论文目录

• 摘要
• Abstract
• 第一章 前言
• 1.1 SAT问题研究现状与背景
• 1.2 论文选题的依据及意义
• 第二章 预备知识
• 2.1 命题逻辑
• 2.2 DP算法简介
• 2.3 计算复杂性简介
• 第三章 可满足性问题概述和传统算法简介
• 2.1 可满足性问题概述
• 2.2 传统算法简介
• 2.2.1 完备性算法
• 2.2.2 局部搜索算法
• 第四章 算法设计
• 4.1 算法中的一些基本概念
• 4.2 算法的基本思路
• 4.3 算法详细设计
• 4.4 冲突消解
• 4.5 算法模块实现
• 第五章 实验数据和结论
• 5.1 实验数据与结论
• 5.2 存在的问题
• 5.3 后续工作
• 致谢
• 参考文献
• 附录一
• 附录二: 源代码