开题报告(王晓峰).ppt

1、基于WP的启发式极性决策算法解SAT问题,研究生：王晓峰导师:许道云教授,可行性分析,汇报提纲,研究内容,选题意义,研究意义(1)可满足性问题(SAT问题)是计算机科学中的核心问题。SAT问题是一类有名的NP-完全问题，直观上它超出了现代计算机的计算能力，从理论上讲，SAT问题不能在多项式时间内解决。然而，在实际应用中不可回避这一问题。因此，高效适用的SAT算法是目前研究的热点。(2)根据能否证明一个实例的不可满足性，SAT算法可分为完全算法和不完全算法两大类。尽管不完全算法对大多数可满足性实例很快能够找到一个解。但不能证明一个SAT实例是不可满足的。完全算法能够验证一个SAT实例满足或者不满

2、足，但在满足实例上的整体效果不如不完全算法。而在许多应用领域，如EDA的等价性验证或者属性检验需要证明一个实例不满足，因此，DPLL完全算法受到更为广泛的关注。,选题意义,国外研究现状：几个优秀算法Zchaff、MiniSat信息传播算法WP、BP、SP国内研究现状：荆明娥,周电等.启发式极性决策算法解SAT问题;邵明,李光辉,李晓维.求解可满足问题的调查传播算法以及步长的影响规律；李韶华，张健.一种求解SAT的高效算法；,研究内容,WP算法简单介绍警示传播(WarningPropagation,WP)算法是源于物理学的一个不完全算法，它在解决变元数很多的实例上表现不错。WP算法是在因子图上通

3、过某种警示信息的迭代，算法收敛时得到一组稳定的警示信息，并利用局部腔域得到公式变元的赋值，通常能够对原问题进行简化。实验表明，这种算法在变量数目很大的难解区域，有不错的表现，并且在SAT/UNSAT的相变区域也有优越的表现，能固定10%-50%的变量赋值。但遗憾的是，WP算法常常在相变区域不收敛，在这种情况下，得到的子公式往往是UNSAT的，或者用其它解决器在短时间内难以求解。特别是在RB模型产生的实例集上，WP算法在相变区域基本不收敛。,研究内容,研究WP算法的基本原理，分析WP算法的收敛性研究WP算法在不收敛时的改进策略，使之更有效的解决难解区域实例和相变区域实例研究加速WP算法收敛的改进

4、策略设计出一个有效的求解SAT问题的完全算法,研究方案,1）掌握WP算法和DPLL算法的基本原理2）掌握Zchaff算法基本思想，并进行实验验证3）分析WP算法的收敛性，并给出算法的改进策略，进行实验验证4）设计出一个求解SAT问题的完全算法5）给出新算法的实验验证6）对算法进行评价，与已有算法进行比较，给出评价参数指标,可行性分析,可满足性问题算法研究，国内外的专家学者已经做了大量的研究，大量的参考资料可以获取。我们在阅读大量的参考资料的同时，收集了大量的实例集，进行了大量的科学实验，取得较好的实验结果。本研究有望达到预期结果。此外，本课题在导师的指导下，已经完了初步设计，确保该课题的可行性。,预期结果,设计基于WP的启发式极性决策算法搭建实验平台，对算法进行实验验证,任务安排,该课题研究的起止年限是2009年4月至2010年5月。任务安排如下：2009年4月2009年6月：查阅相关文献；收集资料，掌握本领域的研究现状，并掌握一些工具的使用。2009年6月2009年10月：研究问题；对课题进行详细分析，给出粗略的设计方案。2009年10月2010年1月：解决问题；给出详细的设计方案，