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

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

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

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