極小不可滿足公式在CNF公式類歸約中的應(yīng)用.pdf

1、經(jīng)典邏輯中的SAT問題是指布爾表達(dá)式的可滿足性問題，它是計算機科學(xué)中的核心問題。SAT問題是NP完全問題，從理論上說，SAT問題不能在多項式時間內(nèi)解決，它超出了現(xiàn)代計算機的能力。所以，SAT問題是計算機科學(xué)發(fā)展中的“瓶頸”問題，計算機科學(xué)家們一直都在尋求各種快速策略和方法試圖改進(jìn)SAT問題的求解?！　∫粋€CNF公式是有限個子句的合取，k-CNF是子句長度不超過k的公式類，k-SAT就是判定給定的k-CNF公式是否有可滿足的解。眾所周知

2、，2-SAT問題是線性時間可解的，而k-SAT問題是NP完全的。近年來，尋找k-SAT的最優(yōu)算法一直沒有停止過。最新研究結(jié)果表明改進(jìn)的關(guān)于k-SAT的指數(shù)時間算法的復(fù)雜度隨k的遞增而增加。在文獻(xiàn)[IP99]中，R.Impagilazzo和R.Paturi定義了一個參數(shù)Sk=inf{δ|存在解決k-SAT的復(fù)雜度為o(2δn)的算法}，同時，還證明了在關(guān)于k-SAT有指數(shù)時間算法的假設(shè)下，{sk}是一個關(guān)于k的遞增序列。于是，在文獻(xiàn)[IP

3、99]中，提出了一個公開問題：如何有效的將k-CNF類公式歸約為t-CNF類公式(t＜k)?？梢钥闯?，解決上述問題對于k-SAT問題的研究有重要意義?！　O小不可滿足公式的研究是近年來興起的關(guān)于SAT問題的一個熱點方向。一個CNF公式F稱為極小不可滿足的(MU)，如果F是不可滿足，并且在F中刪去任意一個子句后所得到的公式是可滿足的。MU(k)表示子句數(shù)與變元數(shù)的差為k的極小不可滿足公式的類。極小不可滿足公式的一些結(jié)構(gòu)和性質(zhì)將有助于研究