论文部分内容阅读
命题公式的可满足问题是首个被证明为NP的问题，而且是计算机科学中很多领域的重要问题，包括计算机科学基础理论、人工智能、数理逻辑。在1997年和2003年人工智能会议上提出了SAT问题面临的十大挑战性问题，在2001年和2007年两年都对当时的SAT问题现状进行了完整的总结。这十大挑战性问题的提出对SAT问题的理论研究和算法改进起到了很强的推动作用。目前的SAT问题主要应用在电子设计自动化中，在此同时，许多世界上现实的实际问题都可以转化为SAT问题。很多的研究者也投入在SAT高效的求解算法的研究中，主要包括两大算法：完备求解算法和不完备求解算法。完备算法的SAT求解算法主要是基于DPLL求解的，该类算法能够证明命题公式是否有解，但是效率比较低；而不完备算法主要是通过局部搜索算法，进行求解，基于局部搜索求解的，该类算法可以很快的找到解，但是当没有找到解退出的时候，不能说明命题公式是否有解。随着发展，扩展出一些SAT的分支问题：最大可满足问题、量化的布尔公式、可满足性模块理论等。在SAT问题中，骨架变量是在所有可满足赋值中都恒取定值的变量，骨架变量的规模与SAT问题中的搜索规模有着密切的关系。这种特性可以用来减少一些问题的复杂性，所以骨架变量在一些SAT问题中，可以进行一些优化，例如故障诊断、随机3-SAT问题、概率信息传递算法等。因为骨架变量的这些优势，目前提出了很多计算骨架变量的算法，这些算法主要是基于迭代、基于分块、基于不可满足核的算法。其中，也可以组合这些思想，变成混合算法进行求解骨架变量。本文主要利用改进的变量选择策略应用到基于迭代的骨架变量算法中。首先利用基于DPLL的SAT完备算法中层的概念，作为变量选择策略，应用到骨架变量的求解中。利用层信息动态地选择变量去求解骨架变量，提高算法的效率：可以连续地运用可满足的增量信息，还可以尽早地加速削减搜索空间。然后本文回顾了在SAT不完备算法中的邻居策略。本文把基于邻居策略的思想，利用到骨架变量的求解中，通过尽早地找到骨架变量，减少表达式的复杂性，加速了算法的求解。实验结果表明，两种新的变量选择策略，都可以提高算法的性能，对比两者可以得到，基邻居的策略表现出更好的性能。