可滿足問(wèn)題求解算法DPLL的優(yōu)化技術(shù)研究.pdf

1、求解效率一直是可滿足性問(wèn)題(SAT)的研究熱點(diǎn)，因?yàn)樘岣咝士梢杂行У臄U(kuò)大SAT的應(yīng)用范圍。長(zhǎng)期以來(lái)，研究者們對(duì)此進(jìn)行了不斷地探索，并提出了多種算法，如Tableau、DPLL、GRASP等。隨著研究的進(jìn)一步深入，人們發(fā)現(xiàn)DPLL算法具有高效、易操作等優(yōu)點(diǎn)，所以對(duì)DPLL算法的優(yōu)化與改進(jìn)逐漸成為SAT求解算法的核心。本文在DPLL算法的基礎(chǔ)上，針對(duì)它在選取判定變量時(shí)過(guò)于隨機(jī)的問(wèn)題，提出了兩種判定層優(yōu)化技術(shù)。具體研究?jī)?nèi)容如下:
　　

2、1、提出了基于變量個(gè)數(shù)的判定啟發(fā)式策略。該策略是在對(duì)DPLL完備算法的學(xué)習(xí)和不同形式下對(duì)子句文字排序處理研究的基礎(chǔ)上提出的，它通過(guò)統(tǒng)計(jì)子句集中每個(gè)變量的出現(xiàn)次數(shù)，并考慮變量中正負(fù)文字的出現(xiàn)次數(shù)，然后挑選出次數(shù)最高的進(jìn)行賦值。實(shí)例結(jié)果表明，應(yīng)用該策略求解時(shí)可以有效簡(jiǎn)化實(shí)例的求解空間，減少求解步驟，盡早剪除不滿足解空間，從而有效提高求解效率。
　　2、提出了基于文字分?jǐn)?shù)的判定啟發(fā)式策略。該策略是在考慮子句長(zhǎng)短和變量正負(fù)出現(xiàn)對(duì)變量判定影