關鍵文字和極小不可滿足公式.pdf

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

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

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