從SAT轉換到3-SAT

Question

有誰知道一個好的程序，將每個子句的任意數量的變量轉換爲CNF文件，每個子句只有3個變量（3-CNF）？我在計算機科學書籍中看到過這種算法，但是無法在任何地方找到實現，並且如果其他人已經做到了，就不願意浪費時間實施它。謝謝！

Answer 1

我不知道任何程序要做，但算法非常簡單，所以我只寫了下面的Python腳本（download），它以DIMACS格式讀取一個通用的CNF， SAT問題DIMACS格式：

from __future__ import print_function 
import fileinput 

cnf = list() 
cnf.append(list()) 
maxvar = 0 

for line in fileinput.input(): 
    tokens = line.split() 
    if len(tokens) == 0 or tokens[0] == "p" or tokens[0] == "c": 
     continue 
    for tok in tokens: 
     lit = int(tok) 
     maxvar = max(maxvar, abs(lit)) 
     if lit == 0: 
      cnf.append(list()) 
     else: 
      cnf[-1].append(lit) 

assert len(cnf[-1]) == 0 
cnf.pop() 

new_cnf = list() 
for clause in cnf: 
    while len(clause) > 3: 
     new_clause = list() 
     for i in range(0, len(clause), 2): 
      if i+1 < len(clause): 
       new_cnf.append(list()) 
       new_cnf[-1].append(clause[i]) 
       new_cnf[-1].append(clause[i+1]) 
       maxvar += 1 
       new_cnf[-1].append(-maxvar) 
       new_clause.append(maxvar) 
      else: 
       new_clause.append(clause[i]) 
     clause = new_clause 
    new_cnf.append(clause) 

print("p cnf %d %d" % (maxvar, len(new_cnf))) 
for clause in new_cnf: 
    print(" ".join([ "%d" % lit for lit in clause ]) + " 0") 

感興趣的是當然的for clause in cnf:循環，是以一般坐在存儲在cnf問題，並將其轉換爲存儲在new_cnf 3 SAT實例。它通過將一個子句如

(A[1] or A[2] or A[3] or A[4] or A[5] or A[6] or A[7]) 

轉換成以下一組子句。

(A[1] or A[2] or ~X[1]) 
(A[3] or A[4] or ~X[2]) 
(A[5] or A[6] or ~X[3]) 

(X[1] or X[2] or X[3] or A[7]) 

前三個條款被添加到new_cnf。最後一句話，是不是3-SAT這樣的算法是重新運行在這最後一句，產生了以下新的條款：

(X[1] or X[2] or ~Y[1]) 
(X[3] or A[7] or ~Y[2]) 

(Y[1] or Y[2]) 

這都是3-SAT條款，從而將其添加到new_cnf和算法繼續從cnf的下一個子句。 （如果最後一個子句不是3-sat，算法會繼續工作直到只剩下3個sat子句，最後一個子句的長度約爲每次迭代的一半）。

Answer 2

SAT在多項式時間內不可解（根據當前的知識）。 2-SAT可用多項式時間求解。因此，從一般SAT到2-SAT的轉換不會很快（不是在多項式時間內），否則我們會找到SAT的多項式時間算法。

換句話說，將SAT轉換爲2-SAT所需的時間與剛剛解決SAT的時間大致相同。

也許你的意思是3-SAT，而不是2-SAT？