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

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

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

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