基于警示傳播的啟發(fā)式極性決策算法求解SAT問(wèn)題.pdf

1、本文提出了基于警示傳播的啟發(fā)式極性決策算法(WPDP)，是一個(gè)完全算法，不但能夠解決大部分難解可滿足性實(shí)例，而且能夠驗(yàn)證實(shí)例的不可滿足性。它繼承了Zchaff算法的基本特性，如快速布爾約束推理(BCP)、變量狀態(tài)獨(dú)立下降和(VSIDS)等，同時(shí)引入了變量極性決策，將WP算法得到的近似解作為變量極性決策，引導(dǎo)DPLL算法的搜索。從而有效降低了DPLL算法在搜索過(guò)程中的沖突次數(shù)，加速了算法的搜索速度，提高了算法的效率，而且本算法還可解決WP

2、算法原本無(wú)法解決的難解可滿足性實(shí)例。在此基礎(chǔ)上，接著提出了兩個(gè)類似的啟發(fā)式極性決策算法：基于信念傳播的啟發(fā)式極性決策算法和基于聚類排序選擇的啟發(fā)式極性決策算法?；谛拍顐鞑サ膯l(fā)式算法，是利用信念傳播算法(BP算法)得到一組近似解，作為DPLL算法的變量極性決策，指導(dǎo)DPLL算法的搜索。而基于聚類排序的啟發(fā)式算法，是利用遺傳算法能夠快速得到可滿足性公式解這一特性，并加入了聚類排序選擇算子，得到一組近似解作為DPLL算法的變量極性決策，指

3、導(dǎo)DPLL算法有效搜索。這也是一個(gè)完全算法，能夠有效給出不可滿足性實(shí)例無(wú)解的證明，彌補(bǔ)了遺傳算法不能有效給出不可滿足性實(shí)例解的缺陷。實(shí)驗(yàn)表明，這幾種啟發(fā)式極性決策算法能夠解決目前很多算法無(wú)法解決的難解實(shí)例。而且，其性能明顯優(yōu)于同類算法。本文的主要?jiǎng)?chuàng)新點(diǎn)有：
　　1.對(duì)大量的已有算法進(jìn)行分析，在此基礎(chǔ)上歸納出了原有算法的不足之處，提出了一個(gè)更為有效的解決可滿足性問(wèn)題的完全算法（WPDP）。
　　2.提出了WP算法在某些實(shí)例集上