1、命題變?cè)捌浞穸ńy(tǒng)稱為文字。文字的析取稱為子句，子句的合取稱為合取范式(CNF公式)。如果存在一個(gè)賦值使得公式的值為1，則稱該公式可滿足：否則稱該公式不可滿足。判定一個(gè)公式是否是可滿足的問(wèn)題稱為可滿足性問(wèn)題，簡(jiǎn)稱為SAT問(wèn)題。解決SAT問(wèn)題的一個(gè)重要算法是DPLL算法。一個(gè)公式是極小不可滿足的是指該公式本身不可滿足，但是從中刪去任意一個(gè)子句后得到的公式可滿足。德國(guó)學(xué)者H.K.Biining，O.Kullmann等人在這方面做了許多重要的

2、工作。極小不可滿足公式的結(jié)構(gòu)和性質(zhì)將有助于判定SAT算法的研究。對(duì)于3-SAT來(lái)說(shuō)，很多學(xué)者所做的大量實(shí)驗(yàn)表明，在m/n大約為4.26時(shí)(其中m是子句個(gè)數(shù)，n是變?cè)獋€(gè)數(shù))，可滿足概率為0.5。一般認(rèn)為，在這個(gè)比值下隨機(jī)生成的3-SAT問(wèn)題實(shí)例非常難解決，而在其它比值下生成的實(shí)例容易解決，這種容易-困難-容易的現(xiàn)象就是所謂的相變現(xiàn)象，它原本是物理學(xué)中的概念?；谙嘧儸F(xiàn)象，Monasson等人于1999年介紹了最大可滿足公式的脊。在最大可滿

3、足賦值中均取真的文字構(gòu)成的集合稱為最大可滿足公式的脊。Dubois等人于2001年根據(jù)可滿足公式脊的概念，定義了尋找可滿足公式的脊的啟發(fā)式算法，但是沒(méi)有進(jìn)行理論研究。 本文在啟發(fā)式算法的基礎(chǔ)上，一方面定義可滿足公式的關(guān)鍵文字，研究關(guān)鍵文字的性質(zhì)，給出DPLL算法的一種改進(jìn)方法；另一方面，利用極小不可滿足公式的特殊結(jié)構(gòu)，定義極小不可滿足公式的相對(duì)關(guān)鍵文字，研究相對(duì)關(guān)鍵文字與極小不可滿足公式之間的關(guān)系，可以證明，儀使用關(guān)鍵文字規(guī)則和