论文部分内容阅读
命题逻辑公式的可满足性问题(SAT)是计算机科学和人工智能中一个重要问题。它是第一个被证明了的NP完全问题,由Stephen Cook于1971年提出。SAT问题在人工智能、软件工程、VLSI集成电路设计等领域具有广泛的应用。3-SAT问题是每个子句的文字个数固定为3的SAT问题。作为SAT问题的子问题之一,3-SAT问题也是NP完全问题。3-SAT问题有来自工业问题转化的实际问题,也有机器自动生成的。来自工业问题转化的3-SAT问题在数目和结构上都有很大的限制,根本不能满足各类SAT算法的测试需求,所以目前大部分的3-SAT问题来自机器自动生成,这类问题又称为随机3-SAT问题。当变元的数目达到1000乃至1兆的规模时,3-SAT问题的求解变得异常困难,所以对大规模随机3-SAT的求解是一个比较有前景的研究领域。自从20世纪80年代随机3-SAT问题被提出以来,很多学者在这方面做了大量的工作,提出了各种各样的算法。当前较为高效的算法有Sparrow2011算法、ProbSAT算法、CCMC算法等。然而这些算法,在求解较大规模的随机3-SAT问题上的效率仍不够理想。本文在综合分析以往SAT问题算法的基础上,在提高随机3-SAT问题的求解效率方面主要做了如下工作：1、基于SAT问题的自身结构,研究各个文字在子句集中出现的频率,挖掘出文字与子句集可满足性判定的关系。给出文字的关键度和关键文字的概念,利用关键文字规则和DPLL规则设计出了对子句集初始真值指派的优化策略。2、给出了基于优化后的初始真值指派的新的WASAT算法,算法先是运用真值指派综合评估函数来寻求更优的赋值,然后运用子句权重重置的策略,跳出局部最优解开辟新的搜索区域。3、运用来自SAT竞赛网站的不同规模的随机3-SAT实例设计实验并得出结果。通过对比Sparrow2011算法、ProbSAT算法、CCMC算法,评估并分析了新的权重分析算法的效率。