论文部分内容阅读
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问题库测试例,验证了算法的有效性。