开题报告(王晓峰).ppt

《开题报告(王晓峰).ppt》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

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

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

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

4、收敛性研究WP算法在不收敛时的改进策略，使之更有效的解决难解区域实例和相变区域实例研究加速WP算法收敛的改进策略设计出一个有效的求解SAT问题的完全算法研究方案1）掌握WP算法和DPLL算法的基本原理2）掌握Zchaff算法基本思想，并进行实验验证3）分析WP算法的收敛性，并给出算法的改进策略，进行实验验证4）设计出一个求解SAT问题的完全算法5）给出新算法的实验验证6）对算法进行评价，与已有算法进行比较，给出评价参数指标可行性分析可满足性问题算法研究，国内外的专家学者已经做了大量的研究，大量的参考资料可以获取。我们在阅读大量的参考资料的同时，收集了大量的实例集，进行

5、了大量的科学实验，取得较好的实验结果。本研究有望达到预期结果。此外，本课题在导师的指导下，已经完了初步设计，确保该课题的可行性。预期结果设计基于WP的启发式极性决策算法搭建实验平台，对算法进行实验验证任务安排该课题研究的起止年限是2009年4月至2010年5月。任务安排如下：2009年4月—2009年6月：查阅相关文献；收集资料，掌握本领域的研究现状，并掌握一些工具的使用。2009年6月—2009年10月：研究问题；对课题进行详细分析，给出粗略的设计方案。2009年10月—2010年1月：解决问题；给出详细的设计方案，并设计出算法。写出相应的程序，进行实验验证，对算法

6、进行复杂性分析，给出算法的有效性。2010年1月—2010年5月：论文修整，整理稿件成文。谢谢