algorithm - 从 SAT 到 3-SAT 的转换器

Question

有谁知道一个好的程序可以将每个子句具有任意数量变量的 CNF 文件转换为每个子句恰好有 3 个变量的 CNF 文件 (3-CNF)？我在计算机科学书籍中看到过这种算法，但无法在任何地方找到实现，如果其他人已经实现，我不愿意浪费时间自己实现它。谢谢!

Answer 1

我也不知道有什么程序可以做到这一点，但是算法真的很简单所以我只写了下面的 python 脚本(download)读取 DIMACS 格式的通用 CNF 并写入等效的 CNF 3 -DIMACS 格式的 SAT 问题:

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")

当然，有趣的一点是 cnf 中的 for 子句: 循环获取存储在 cnf 中的一般 sat 问题并将其转换为存储在中的 3-sat 实例new_cnf。它通过翻译一个子句来做到这一点，例如

(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 子句。最后一个子句的长度在每次迭代中大约减半。)