SAT solver in Python (~175 SLOC) with watch lists

These are couple of my remakes of Donald Knuth's SAT0W SAT solver (CWEB file on his website), which is very basic and only serves as a demonstration of watch lists. Read more about it in TAOCP (algorithm B, pp. 30-31).

In short:

#!/usr/bin/env python

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

    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
    for c in content[1:]:
        if c.startswith ("c "):
        for var_s in c.split(" "):
            if var!=0:

    if clauses_total != len(clauses):
        print "warning: header says ", clauses_total, " but read ", len(clauses)
    return variables_total, clauses

# variable numbers and corresponding literal numbers (the last bit is 1 for a positive variable and 0 for a negative variable):
# -1 : 0
# 1  : 1
# -2 : 2
# 2  : 3
# -3 : 4
# 3  : 5
# etc

def var2lit(var):
    if var<0:
        return (abs(var)-1)*2
        return (abs(var)-1)*2+1

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

literals_total = variables_total*2

# key = literal
# val = watched list of clauses
for l in range(literals_total):

# set initial watched lists by attaching first variable of each clause to the corresponding literal
# first literal/variable of each clause is the default watchee
for clause in clauses:

# array of choices, 0 for False, 1 for True

# if the variable is already assigned?
def var_already_assigned_to_false (var):
    global move
    return move[abs(var)-1]==0

def var_already_assigned_to_true (var):
    global move
    return move[abs(var)-1]==1

# find a place for a clause to reattach it
def find_better_place_for_clause(level, c_no):
    global clauses, move, literals, variables_total
    if len(clauses[c_no])==1: # unit clause? we can't do anything
        return False
    # enumerate all literals/variables in clause except first:
    for v in range(1, len(clauses[c_no])):
        # this variable/literal isn't yet assigned
        # so we can "postpone" it for future
        if (abs(var)-1) > level:
            # reattach clause:
            # swap first variable/literal in clause with newly watchee
            clauses[c_no][v], clauses[c_no][0] = clauses[c_no][0], clauses[c_no][v]
            return True

        # this variable/literal is already assigned and it's value coincides with our variable:
        cond1 = var_already_assigned_to_false(var) and var<0
        cond2 = var_already_assigned_to_true(var) and var>0
        if cond1 or cond2:
            # reattach clause:
            # swap first variable/literal in clause with newly watchee
            clauses[c_no][v], clauses[c_no][0] = clauses[c_no][0], clauses[c_no][v]
            return True

    return False

# "disembowel" a watch list by reattaching all clauses in WL to other literals/watch lists:
def reconnect_all_clauses(level):
    global clauses, move, literals, variables_total
    # which literal to "disembowel"?
    if move[level]==0:
    # list of clauses in WL to "disembowel":
    for i in range(len(tmp)):
        if find_better_place_for_clause(level, tmp[i]):
            # delete first element. maybe slow?
            # there is a contradicted clause we can't reattach, so return False
            return False
    # all clauses from WL has been reconnected, proceed further
    return True

def try_bits(level):
    #print "try_bit(", level, ")"
    global clauses, move, literals, variables_total
    #print move
    if level==variables_total:
    # all variables are assigned, and we are here, hence, all satisfied, so we stop here
        print "SAT"
        for i in range(variables_total):
            if move[i]==1:
                s=s+str(i+1)+" "
                s=s+"-"+str(i+1)+" "
        print s
    # if the "positive" literal has a watch list attached, start with True, then switch to False
    # because there is a chance after backtrack that "negative" literal has no watch list attached, so why do unneeded work
    # by reattaching?
    # otherwise, start with False and switch to True
    if len(literals[level*2+1])>0:
        first_alternative, second_alternative = 1,0
        first_alternative, second_alternative = 0,1

    # try to reconnect all clauses
    # proceed deeper in case of success
    if reconnect_all_clauses(level):

    # no success, remove first_alternative from move[], proceed to the second one:
    if reconnect_all_clauses(level):

    # no luck with both alternatives, so we backtrack by returning from recursive call
    # if there is no place to return (level=0), the instance cannot be satisfied:
    if level==0:
        print "UNSAT"


It can solve tiny SAT instances such as queens on a 10*10 chess board, etc.

Now my second solver in C/C++, which works almost like Donald Knuth's SAT0W. My goal was to remake it precisely, so that I can be sure I understood everything well. To be fast, there is no recursion.

~540 SLOC of C/C++.

Also, as we may notice, clauses are not to be added to a watch list or removed. They are rather moved. Also, order of clauses in watch list is not important at all. Hence, by moving a clause from one WL to another, we can add it to the front of destination WL.

My solution is single-linked lists, but with no pointers, rather indices are stored (and -1 is a terminating value). Like Donald Knuth's SAT0W, my solver can even factorize small 8-bit numbers.

Needless to say, an order of variables influences the process drastically. Hence, my solver can behave differently if it reads DIMACS CNF file or Knuth-style SAT file (where variable names are used instead of numbers). However, finding a best order of variables is a problem comparable to SAL solving itself.

Also, my primitive and naive SAT solver I wrote 2 years ago, but just 120 SLOC.

→ [list of blog posts]

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