線性公式可滿足性判定問題的復(fù)雜性.pdf

1、可滿足性問題(SAT)是計(jì)算機(jī)科學(xué)的中心問題之一，也是第一個(gè)被證明的NP-完全問題，并且是一大類NP-完全問題的核心。SAT問題是指可滿足布爾表達(dá)式的集合，它在數(shù)理邏輯、人工智能、約束可滿足性問題、VLSI集成電路設(shè)計(jì)與檢測、計(jì)算機(jī)科學(xué)理論、計(jì)算機(jī)視覺、機(jī)器定理證明、機(jī)器人規(guī)劃、機(jī)器學(xué)習(xí)等領(lǐng)域具有廣闊的應(yīng)用背景。一個(gè)CNF公式F稱為線性的，如果F中任意兩個(gè)不同的子句中至多包含一個(gè)相同的變元。一個(gè)CNF公式F稱為嚴(yán)格線性的，如果F中任兩個(gè)

2、不同的子句恰好包含一個(gè)相同的變元。所有嚴(yán)格線性公式是可滿足的([33]S.Porschenetc.,2006)。對于線性公式類LCNF，判定問題LSAT是NP-完全的。對于LCNF的子類LCNF≥k(其公式中每個(gè)子句的長度至少為k)，如果在LCNF≥k公式中存在一個(gè)不可滿足公式，則判定問題LSAT≥k是NP-完全的([31，32]S.Porschen，E.Speckenmeyer,2006)。因此，對于LCNF≥k(k≥3)公式，判定問

3、題LSAT≥k的NP-完全性取決于在LCNF≥k公式中是否存在不可滿足公式。在([31，32]S.Porschen.E.Speckenmeyer,2006)中，通過構(gòu)造超圖和拉丁方陣，已經(jīng)證明了LCNF≥3和LCNF≥4都包含不可滿足公式，并提出了一個(gè)公開問題：當(dāng)k≥5時(shí)，在LCNF≥k公式中是否存在不可滿足公式。 本文基于線性公式的結(jié)構(gòu)與特點(diǎn)，提出了線性化算法，使用該算法可以在|F|多項(xiàng)式時(shí)間內(nèi)把任一公式F轉(zhuǎn)化為線性公式Fli