DPLL到（1，1）-消解的轉(zhuǎn)換及其復(fù)雜性分析.pdf

1、命題公式的滿足性問題(簡(jiǎn)稱SAT問題)是指布爾表達(dá)式的可滿足性問題.它是理論計(jì)算機(jī)科學(xué)中的一個(gè)重要問題.在數(shù)理邏輯、人工智能、約束滿足問題、VLSI集成電路設(shè)計(jì)與檢測(cè)以及計(jì)算機(jī)科學(xué)理論等領(lǐng)域具有廣闊的應(yīng)用背景。SAT問題是第一個(gè)NP-完全問題，并且是一大類NP-完全問題的核心。 一個(gè)CNF公式(conjunctivenormalform)是有限個(gè)子句的合取，(r.s)-CNF公式是指每個(gè)子句恰恰含有r個(gè)不同的文字，且每個(gè)變量出現(xiàn)

2、的次數(shù)最多出現(xiàn)s次的CNF公式類，(r.s)-SAT是限定在(r.s)-CNF上的命題滿足性實(shí)例。一個(gè)SAT算法能在有限時(shí)間內(nèi)判定任意給定的CNF公式是否可滿足，DPLL算法和消解反駁法是判定SAT問題的兩個(gè)重要方法。OlgaTveretina和HansZantema已經(jīng)詳細(xì)分析了DPLL算法到消解的轉(zhuǎn)換，并證明了，如果有一個(gè)長度為s的DPLL反駁，結(jié)點(diǎn)數(shù)為r，且每個(gè)結(jié)點(diǎn)標(biāo)記的單位消解序列是完備的，則存在一個(gè)長度為s-r的消解反駁，顯然

3、這個(gè)長度已經(jīng)優(yōu)于s。我們已經(jīng)知道，對(duì)于任意一個(gè)MU(1)公式對(duì)應(yīng)一個(gè)(1，1)-消解。極小不可滿足公式的研究是近年來興起的問題的一個(gè)熱點(diǎn)方向。德國學(xué)者H.KleineBüning，O.kullmann等人在這方面做了許多重要的工作。極小不可滿足公式的一些結(jié)構(gòu)和性質(zhì)將有助于判定SAT算法的研究。 本文通過研究極小不可滿足公式的樹消解證明及極小不可滿足公式的分裂，構(gòu)建了(r，s)-SAT中的一些極小不可滿足實(shí)例。并在此基礎(chǔ)上，表示了