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

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

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

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