0w1

Reducing NP problems to SAT

Here are only a few rough notes I have grasped recently, and would probably not make much sense to any of you.

First, it is proved that all NP problems ( Hamiltonian Path, Graph Coloring etc. ) can be reduced to SAT problem.
One example is searching a feasible solution for Sudoku. Any search problem could also be reduced to SAT problem. For this instance, we can set a bunch of boolean variables, let x[ i , j , k ] denote the variable for the cell in row i, column j, having value k. Then we will be able to set the restrictions, and successfully convert the original Sudoku problem to SAT problem. What's interesting is that although SAT problems could potentially and theoretically should run in exponential time, in practice, many efficient SAT-solvers can run most of the cases in a split of a second. One example is MiniSat, an open source code that is a very efficient SAT-solver. Through converting the problem to SAT, most Sudoku puzzles can be solved in less than 10 ms.

In SAT, each clause must only contain NOT and OR logic gates. Clauses are then considered ANDing each other.
To make the converting process easy, we will need to introduce logic gates, such as AND or NOT ( although in MiniSat, - denotes NOT ).
a AND b : ( a OR NOT z )( b OR NOT z )( NOT a OR NOT b OR z )( z )
NOT a : ( a OR z )( NOT a OR NOT z )( z )

Below is a sample code for Sudoku taken from Coursera. ( if I am not allowed to do so, please notify me )

import itertools
import os

puzzle=[
    "5***1***4",
    "***2*6***",
    "**8*9*6**",
    "*4*****1*",
    "7*1*8*4*6",
    "*5*****3*",
    "**6*4*1**",
    "***5*2***",
    "2***6***8"
]

clauses = []

digits = range(1, 10)

def varnum(i, j, k):
    assert(i in digits and j in digits and k in digits)
    return 100*i + 10*j + k


def exactly_one_of(literals):
    clauses.append([l for l in literals])

    for pair in itertools.combinations(literals, 2):
        clauses.append([-l for l in pair])


# cell [i,j] contains exactly one digit
for (i, j) in itertools.product(digits, repeat=2):
    exactly_one_of([varnum(i, j, k) for k in digits])

# k appears exactly once in row i
for (i, k) in itertools.product(digits, repeat=2):
    exactly_one_of([varnum(i, j, k) for j in digits])

# k appears exactly once in column j
for (j, k) in itertools.product(digits, repeat=2):
    exactly_one_of([varnum(i, j, k) for i in digits])

# k appears exactly once in a 3x3 block
for (i, j) in itertools.product([1, 4, 7], repeat=2):
    for k in digits:
        exactly_one_of([varnum(i + deltai, j + deltaj, k) for (deltai, deltaj) in itertools.product(range(3), repeat=2)])


for (i, j) in itertools.product(digits, repeat=2):
    if puzzle[i - 1][j - 1] != "*":
        k = int(puzzle[i - 1][j - 1])
        assert(k in digits)
        # [i,j] already contains k:
        clauses.append([varnum(i, j, k)])

with open('tmp.cnf', 'w') as f:
    f.write("p cnf {} {}\n".format(999, len(clauses)))
    for c in clauses:
        c.append(0);
        f.write(" ".join(map(str, c))+"\n")

os.system("minisat tmp.cnf tmp.sat")

with open("tmp.sat", "r") as satfile:
    for line in satfile:
        if line.split()[0] == "UNSAT":
            print("There is no solution")
        elif line.split()[0] == "SAT":
            pass
        else:
            assignment = [int(x) for x in line.split()]

            for i in digits:
                for j in digits:
                    for k in digits:
                        if varnum(i, j, k) in assignment:
                            print(k, end="")
                            break

                print("")