啟發(fā)式將3-SAT化為2-SAT的DPLL算法.pdf

1、可滿足性問(wèn)題(SAT)研究如何判定一個(gè)任意給定的邏輯表達(dá)式是否存在可滿足真值指派。SAT在數(shù)理邏輯、人工智能、計(jì)算機(jī)算法設(shè)計(jì)與分析以及工程應(yīng)用等領(lǐng)域有著重要的地位，而且SAT問(wèn)題是第一個(gè)被證明的NP完全問(wèn)題。 3SAT是一類特殊的可滿足性問(wèn)題，它的子句中所包含的文字個(gè)數(shù)最多只有3個(gè)，3SAT也是NP-完全問(wèn)題之一。它可以從很多實(shí)際問(wèn)題抽象出來(lái)，其在邏輯推理、人工智能的專家系統(tǒng)、數(shù)據(jù)庫(kù)維護(hù)和檢索、VLSI設(shè)計(jì)及檢測(cè)等領(lǐng)域有廣泛的應(yīng)

2、用，它的廣泛的應(yīng)用背景促使人們對(duì)它進(jìn)行深入細(xì)致的研究。 目前求解SAT問(wèn)題的算法分為完全性算法和局部搜索算法。前者主要有窮舉法，DPLL算法，松馳法等；后者的代表性算法主要是局部搜索算法，如GSAT。這些算法的一個(gè)特點(diǎn)是直接對(duì)3SAT判斷其可滿足性。而本文采取的方法不是直接判定3SAT可滿足性的問(wèn)題，而是將3SAT化為2SAT的問(wèn)題。因?yàn)?SAT是可多項(xiàng)式時(shí)間內(nèi)判定的，所以如果能在多項(xiàng)式時(shí)間內(nèi)將3SAT化為2SAT，那么我們就能

3、在多項(xiàng)式時(shí)間內(nèi)判定3SAT是否可滿足。 本文將啟發(fā)式策略與DPLL算法相結(jié)合，從快速求解的角度來(lái)設(shè)計(jì)算法。先將原始公式用DP算法化簡(jiǎn)：用DP算法中的重言式規(guī)則、單子句規(guī)則、純文字規(guī)則將公式中的重言式、單子句將純文字消除，如果公式中子句集為空，則公式可滿足；如果子句集不為空，但是公式中沒(méi)有包含3個(gè)文字的子句，則說(shuō)明已經(jīng)將公式化為2SAT，否則對(duì)公式中包含3個(gè)文字的子句集分別統(tǒng)計(jì)變?cè)霈F(xiàn)與負(fù)出現(xiàn)的次數(shù)，然后選取正出現(xiàn)與負(fù)出現(xiàn)的次數(shù)