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!

Elliot Gorokhovsky
  • 3,610
  • 2
  • 31
  • 56
  • To convert clauses with more than 3 literals into 3-CNF clauses, you could convert each clause in a nested Boolean expression and apply Tseitin encoding as sketched in a related posting: http://stackoverflow.com/questions/22925923/how-can-i-recast-a-cnf-expression-to-3-cnf/23511304#23511304 – Axel Kemper Dec 03 '14 at 21:47
  • @AxelKemper do you know of any programs I could download for that? – Elliot Gorokhovsky Dec 03 '14 at 22:02
  • I don't know of such a program. But I have another posting which might help: http://math.stackexchange.com/questions/498128/converting-into-cnf-form/509925#509925 – Axel Kemper Dec 03 '14 at 22:53

2 Answers2

6

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

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

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

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

CliffordVienna
  • 7,995
  • 1
  • 37
  • 57
2

SAT is not solvable in polynomial time (according to the current knowledge). 2-SAT is solvable in polynomial time.

So a conversion from generic SAT to 2-SAT will not be fast (not in polynomial time), otherwise we would find a polynomial-time algorithm for SAT.

In other words, the time needed to convert SAT to 2-SAT is roughly the same as the time to just solve SAT.

Maybe you mean 3-SAT, not 2-SAT?

Sergii Dymchenko
  • 6,890
  • 1
  • 21
  • 46