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

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

2、不同的子句恰好包含一個相同的變元。所有嚴格線性公式是可滿足的([33]S.Porschenetc.,2006)。對于線性公式類LCNF，判定問題LSAT是NP-完全的。對于LCNF的子類LCNF≥k(其公式中每個子句的長度至少為k)，如果在LCNF≥k公式中存在一個不可滿足公式，則判定問題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都包含不可滿足公式，并提出了一個公開問題：當k≥5時，在LCNF≥k公式中是否存在不可滿足公式。 本文基于線性公式的結(jié)構(gòu)與特點，提出了線性化算法，使用該算法可以在|F|多項式時間內(nèi)把任一公式F轉(zhuǎn)化為線性公式Fli