## 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 7.2.2.2 (algorithm B, pp. 30-31).

In short:

• Variable is what you see in DIMACS CNF file. A number. Can be positive or negative. 1234 and -1234 are the same variable.
• Literal is a variable + sign. 1234 and -1234 are different literals. Clause consists of literals. CNF instance consists of clauses.
• We need to find an assignment for all SAT variables so that all clauses in CNF would be satisfied.
• We don't need to take into account all variables in each clause. Only one literal in each clause must be true to satisfy the whole CNF instance.
• A literal of our importance in each clause is called "watched literal" or "watchee". Each watchee is connected to a literal in a database, forming a "watch list". Default watchee is a first literal of a clause.
• "Assignment" is a goal of a SAT solver: a list of false/true variables. "Partial assignment" is an assigment of several variables, not all. During solving, each watchee is either connected to a literal in a partial assignment, or to (yet) unassigned literal.
• When we switch a variable from false to true (or back) in a partial assignment, a watch list connected to a false literal is to be "disemboweled": all clauses in watch list are to be reconnected to other literals, either under partial assignment, or "shoved" into yet unassigned literals (in other words, postponed to future). Reconnecting involves finding another watchee to be picked from a literals in a clause. If you can't find another watchee, either switch to another alternative for this variable (false/true) or backtrack.
• Several books and articles says that in this scheme, all clauses are always satisfied, this is like invariant. This is not correct. All clauses connected to watch lists under partial assignment during solving are satisfied, so far. While we can't say this about other clauses connected to wach lists behind partial assignment: they are to be processed in future.
• Essentially, the whole process of SAT solving in this tiny SAT solver is moving clauses from one watch list to another.
#!/usr/bin/env python

import sys

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

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

if clauses_total != 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
else:
return (abs(var)-1)*2+1

literals_total = variables_total*2

# key = literal
# val = watched list of clauses
literals={}
for l in range(literals_total):
literals[l]=[]

# 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
c_no=0
for clause in clauses:
first_var=clause[0]
l=var2lit(first_var)
literals[l].append(c_no)
c_no=c_no+1

# array of choices, 0 for False, 1 for True
move=[]

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

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])):
var=clauses[c_no][v]
# this variable/literal isn't yet assigned
# so we can "postpone" it for future
if (abs(var)-1) > level:
# reattach clause:
literals[var2lit(var)].append(c_no)
# 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:
if cond1 or cond2:
# reattach clause:
literals[var2lit(var)].append(c_no)
# 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:
lit=level*2+1
else:
lit=level*2
# list of clauses in WL to "disembowel":
tmp=literals[lit][:]
for i in range(len(tmp)):
if find_better_place_for_clause(level, tmp[i]):
# delete first element. maybe slow?
literals[lit]=literals[lit][1:]
else:
# 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"
s=""
for i in range(variables_total):
if move[i]==1:
s=s+str(i+1)+" "
else:
s=s+"-"+str(i+1)+" "
print s
exit(0)
# 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?
if len(literals[level*2+1])>0:
first_alternative, second_alternative = 1,0
else:
first_alternative, second_alternative = 0,1

move.append(first_alternative)
# try to reconnect all clauses
# proceed deeper in case of success
if reconnect_all_clauses(level):
try_bits(level+1)

# no success, remove first_alternative from move[], proceed to the second one:
move=move[:-1]
move.append(second_alternative)
if reconnect_all_clauses(level):
try_bits(level+1)
move=move[:-1]

# 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"
exit(0)

try_bits(level=0)



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.

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.