Simplest SAT solver in ~120 lines

(The following text has been moved to the article at https://yurichev.com/tmp/SAT_SMT_DRAFT.pdf.)

This is simplest possible backtracking SAT solver written in Python (not a DPLL one). It uses the same backtracking algorithm you can find in many simple Sudoku and 8 queens solvers. It works significantly slower, but due to its extreme simplicity, it can also count solutions. For example, it count all solutions of 8 queens problem. Also, there are 70 solutions for POPCNT4 function (the function is true if any 4 of its input 8 variables are true):

SAT
-1 -2 -3 -4 5 6 7 8 0
SAT
-1 -2 -3 4 -5 6 7 8 0
SAT
-1 -2 -3 4 5 -6 7 8 0
SAT
-1 -2 -3 4 5 6 -7 8 0
...

SAT
1 2 3 -4 -5 6 -7 -8 0
SAT
1 2 3 -4 5 -6 -7 -8 0
SAT
1 2 3 4 -5 -6 -7 -8 0
UNSAT
solutions= 70

It was also tested on my Minesweeper cracker, and finishes in reasonable time (though, slower than MiniSat by a factor of ~10).

On bigger CNF instances, it gets stuck.

Source code:

#!/usr/bin/env python

count_solutions=True
#count_solutions=False

import sys

def read_text_file (fname):
    with open(fname) as f:
        content = f.readlines()
    return [x.strip() for x in content] 

def read_DIMACS (fname):
    content=read_text_file(fname)

    header=content[0].split(" ")

    assert header[0]=="p" and header[1]=="cnf"
    variables_total, clauses_total = int(header[2]), int(header[3])

    # array idx=number (of line) of clause
    # val=list of terms
    # term can be negative signed integer
    clauses=[]
    for c in content[1:]:
        clause=[]
        for var_s in c.split(" "):
            var=int(var_s)
            if var!=0:
                clause.append(var)
        clauses.append(clause)

    # this is variables index.
    # for each variable, it has list of clauses, where this variable is used.
    # key=variable
    # val=list of numbers of clause
    variables_idx={}
    for i in range(len(clauses)):
        for term in clauses[i]:
            variables_idx.setdefault(abs(term), []).append(i)

    return clauses, variables_idx

# clause=list of terms. signed integer. -x means negated.
# values=list of values: from 0th: [F,F,F,F,T,F,T,T...]
def eval_clause (terms, values):
    try:
        # we search for at least one True
        for t in terms:
            # variable is non-negated:
            if t>0 and values[t-1]==True:
                return True
            # variable is negated:
            if t<0 and values[(-t)-1]==False:
                return True
        # all terms enumerated at this point
        return False
    except IndexError:
        # values[] has not enough values
        # None means "maybe"
        return None

def chk_vals(clauses, variables_idx, vals):
    # check only clauses which affected by the last (new/changed) value, ignore the rest
    # because since we already got here, all other values are correct, so no need to recheck them
    idx_of_last_var=len(vals)
    # variable can be absent in index, because no clause uses it:
    if idx_of_last_var not in variables_idx:
        return True
    # enumerate clauses which has this variable:
    for clause_n in variables_idx[idx_of_last_var]:
        clause=clauses[clause_n]
        # if any clause evaluated to False, stop checking, new value is incorrect:
        if eval_clause (clause, vals)==False:
            return False
    # all clauses evaluated to True or None ("maybe")
    return True

def print_vals(vals):
    # enumerate all vals[]
    # prepend "-" if vals[i] is False (i.e., negated).
    print "".join([["-",""][vals[i]] + str(i+1) + " " for i in range(len(vals))])+"0"

clauses, variables_idx = read_DIMACS(sys.argv[1])

solutions=0

def backtrack(vals):
    global solutions

    if len(vals)==len(variables_idx):
        # we reached end - all values are correct
        print "SAT"
        print_vals(vals)
        if count_solutions:
            solutions=solutions+1
            # go back, if we need more solutions:
            return
        else:
            exit(10) # as in MiniSat
        return

    for next in [False, True]:
        # add new value:
        new_vals=vals+[next]
        if chk_vals(clauses, variables_idx, new_vals):
            # new value is correct, try add another one:
            backtrack(new_vals)
        else:
            # new value (False) is not correct, now try True:
            continue

# try to find all values:
backtrack([])
print "UNSAT"
if count_solutions:
    print "solutions=", solutions
exit(20) # as in MiniSat


As you can see, all it does is enumerate all possible solutions, but prunes search tree as early as possible. This is backtracking.

The files: https://github.com/dennis714/yurichev.com/tree/master/blog/SAT_backtrack.

My other notes about SAT/SMT: https://yurichev.com/writings/SAT_SMT_draft-EN.pdf.

Some comments: https://www.reddit.com/r/compsci/comments/6jn3th/simplest_sat_solver_in_120_lines/.


→ [list of blog posts, my twitter/facebook]

Please drop me email about any bug(s) and suggestion(s): dennis(@)yurichev.com.