Конвертер из SAT в 3-SAT

Question

Кто-нибудь знает хорошую программу для преобразования файлов CNF с любым количеством переменных в предложении в файлы CNF с ровно 3 переменными в предложении (3-CNF)? Я видел этот алгоритм в книгах по информатике, но нигде не могу найти реализацию и не хотел бы тратить время на его реализацию сам, если другие уже сделали это. Спасибо!

Answer 1

Я также не знал ни одной программы для этого, но алгоритм действительно прост, поэтому я написал следующий скрипт на python ( скачать), который читает общий файл CNF в формате DIMACS и записывает файл CNF с аналогичной проблемой 3-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: цикл, который принимает общую проблему Sat хранится в cnf и преобразует его в 3-х экземплярах, хранящихся в 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-сат, поэтому алгоритм перезапускается на этом последнем предложении, приводя к следующим новым предложениям:

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

(Y[1] or Y[2])

Это все 3-спальные пункты, поэтому они добавляются в new_cnf и алгоритм продолжается со следующего пункта из cnf, (Если бы последнее предложение не было 3-насыщенным, алгоритм продолжал бы работать над ним до тех пор, пока не останутся только 3-насыщенные предложения. Длина последнего предложения приблизительно уменьшается вдвое с каждой итерацией.)

Answer 2

SAT не разрешим в полиномиальное время (согласно современным знаниям). 2-SAT разрешима за полиномиальное время.

Таким образом, преобразование из общего SAT в 2-SAT не будет быстрым (не за полиномиальное время), в противном случае мы бы нашли алгоритм полиномиального времени для SAT.

Другими словами, время, необходимое для преобразования SAT в 2-SAT, примерно равно времени, необходимому для решения SAT.

Может быть, вы имеете в виду 3-SAT, а не 2-SAT?