有谁知道一个好的程序可以将每个子句具有任意数量的变量的 CNF 文件转换为每个子句恰好有 3 个变量的 CNF 文件(3-CNF)?我在计算机科学书籍中看到过这种算法,但在任何地方都找不到实现,如果其他人已经完成了,我不想浪费时间自己实现它。谢谢!
问问题
3910 次
2 回答
5
我也不知道有什么程序可以做到这一点,但是算法真的很简单,所以我只写了以下 python 脚本(下载),它读取 DIMACS 格式的一般 CNF,并在 DIMACS 中写入等效 3-SAT 问题的 CNF格式:
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:
循环,它将存储在中的一般 sat 问题cnf
转换为存储在中的 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 子句。每次迭代最后一个子句的长度大约减半。)
于 2014-12-21T11:31:58.247 回答
2
SAT 在多项式时间内是不可解的(根据目前的知识)。2-SAT 在多项式时间内是可解的。
所以从通用 SAT 到 2-SAT 的转换不会很快(不是在多项式时间内),否则我们会找到 SAT 的多项式时间算法。
换句话说,将 SAT 转换为 2-SAT 所需的时间与仅解决 SAT 所需的时间大致相同。
也许您的意思是 3-SAT,而不是 2-SAT?
于 2014-12-03T00:41:48.540 回答