可滿足公式到MU（1）公式的擴(kuò)張.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)題的求解。 極小不可滿足公式的研究是近年來(lái)興起的關(guān)于SAT問(wèn)題的一個(gè)熱點(diǎn)方向。一個(gè)CNF公式(CNF公式是有限個(gè)子句的合取)F稱為極小不可滿足的

2、(MU)，如果F是不可滿足，并且在F中刪去任意一個(gè)子句后所得到的公式是可滿足的。MU(k)表示子句數(shù)與變?cè)獢?shù)的差為k的極小不可滿足公式的類。Kleine Buning.H等人的研究結(jié)果表明：如果k≤ 0，則公式不是極小不可滿足的，也就是說(shuō)，所有極小不可滿足公式其子句數(shù)必定大于公式中的變量個(gè)數(shù)。 在本文中，我們將給出一個(gè)在多項(xiàng)式時(shí)間內(nèi)判定可滿足公式到MU(1)公式擴(kuò)張問(wèn)題的算法。關(guān)于公式擴(kuò)張問(wèn)題，Kleine Buning H和Z

3、hao X S已經(jīng)做出了若干結(jié)果，他們得出：Horn公式到MU(1)公式的擴(kuò)張問(wèn)題可在多項(xiàng)式時(shí)間內(nèi)判定，問(wèn)題MU-EXT[ext=t]為Dp-難，問(wèn)題MU-EXT[ext=1]在PNP[logn]之中，問(wèn)題MU-EXT[ext=t，defi=k]可在多項(xiàng)式時(shí)間內(nèi)判定，這里記MU-EXT[ext=t，defi=k]={F∈CNF|()G：F+G∈MU(k)，var(G)() var(F)，| G|=t)。在本論文中，我們考慮對(duì)一個(gè)給定可滿