转换器从SAT至3-SAT

问题描述

有谁知道一个很好的方案，以CNF文件转换任意数量的每个条款变量CNF文件，每个条款（3-CNF）正好3个变量的？我已经看到了这个算法，计算机科学书籍，但无法找到一个实现随时随地，真舍不得浪费时间实现它自己，如果别人已经做到了。谢谢！

Does anyone know of a good program to convert CNF files with any number of variables per clause to CNF files with exactly 3 variables per clause (3-CNF)? I've seen this algorithm in computer science books but can't find an implementation anywhere and would hate to waste time implementing it myself if others have already done it. Thanks!

推荐答案

我不知道任何程序做，要么，但算法是非常简单，所以只是我写了下面的python脚本（的），它读取DIMACS格式的通用CNF和写入的等效3-SAT问题CNF在DIMACS格式为：

I didn't know any program to do that either, but the algorithm is really simple so just I wrote the following python script (download) that reads a general CNF in DIMACS format and writes the CNF of an equivalent 3-SAT problem in DIMACS format:

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子句：循环，需要坐存储在 CNF 把它转换为存储在 new_cnf A 3-SAT实例。它通过把一个条款，如不这样

The interesting bit is of course the for clause in cnf: loop that takes the general sat problem stored in cnf and transforms it into a 3-sat instance stored in new_cnf. It does this by translating a clause such as

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

进入条款下面的一组。

into the following set of clauses.

(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这样的算法是重新运行在这最后的条款，得到了以下新的条款：

The first three clauses are added to new_cnf. The last clause is not 3-sat so the algorithm is re-run on this last clause, yielding the following new clauses:

(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条款都离开了。最后一句的长度大约减半，每次重复。）

This are all 3-sat clauses, so they are added to new_cnf and the algorithm continues with the next clause from cnf. (If the last clause were not 3-sat, the algorithm would keep working on it until only 3-sat clauses are left. The length of the last clause approximately halves with each iteration.)

这篇关于转换器从SAT至3-SAT的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！