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

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:]:
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"

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]:
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.

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