# Simple SAT Solver In Python

I am interested in improving my coding standards in Python so I decided to post one my more recent and smaller "for fun" projects here for review. The code below implements a rather simple backtracking algorithm to solve SAT, which is based on Knuth's SAT0W found here: http://www-cs-faculty.stanford.edu/~uno/programs.html (While the algorithm is essentially the same as Knuth's, my implementation is heavily simplified compared to Knuth's.)

While I appreciate all feedback, I am more interested in improvements that are Python- or implementation-specific, as opposed to algorithmic improvements, since I know there are many ways of improving the algorithm, as discussed by Knuth as well, which I left out of the code in favour of simplicity and ease of understanding.

First, the command-line driver:

"""
Solve SAT instance by reading from stdin using an iterative or recursive
watchlist-based backtracking algorithm. Iterative algorithm is used by default,
unless the -r flag is given.
"""
from __future__ import division
from __future__ import print_function

from argparse import ArgumentParser
from sys import stdin
from sys import stderr

from satinstance import SATInstance
import recursive_sat
import iterative_sat

__author__ = 'Sahand Saba'

if __name__ == '__main__':
parser = ArgumentParser(description=__doc__)
'--verbose',
help='verbose output.',
action='store_true')
'--recursive',
help='use the recursive backtracking algorithm.',
action='store_true')
'--input',
action='store')
args = parser.parse_args()
instance = None
if args.input:
with open(args.input, 'r') as file:
instance = SATInstance.from_file(file)
else:
instance = SATInstance.from_file(stdin)

alg = recursive_sat.solve if args.recursive else iterative_sat.solve
for assignment in alg(instance, args.verbose):
print(instance.assignment_to_string(assignment))
else:
if args.verbose:
print('No satisfying assignment exists.', file=stderr)


The satinstance.py file:

from __future__ import division
from __future__ import print_function

__author__ = 'Sahand Saba'

class SATInstance(object):
"""
Some notes on encoding:
- Variables are encoded as numbers 0 to n - 1.
- Literal v is encoded as 2 * v and ~v as 2 * v + 1. So the foremost
bit of a literal encodes whether it is negated or not. This can be
tested simply with checking if l & 1 is 0 or 1.
- Similarly, to negate a literal, we just have to toggle the foremost
bit.  This can done easily by XORing with 1: the negation l is l ^ 1.
- To get a literal's variable, we just need to shift to the right. This
can be done with either l >> 1.

Example: Let's say variable b is encoded with number 3. Then literal b
is encoded as 2 * 3 = 6 and ~b as  2 * 3 + 1 = 7.
"""
clause = []
for literal in line.split():
negated = 1 if literal.startswith('~') else 0
variable = literal[negated:]
if variable not in self.variable_table:
self.variable_table[variable] = len(self.variables)
self.variables.append(variable)
encoded_literal = self.variable_table[variable] << 1 | negated
clause.append(encoded_literal)
self.clauses.append(tuple(set(clause)))

@classmethod
def from_file(cls, file):
instance = cls()
instance.variables = []
instance.variable_table = dict()
instance.clauses = []
for line in file:
instance.n = len(instance.variables)
return instance

def literal_to_string(self, literal):
s = '~' if literal & 1 else ''
return s + self.variables[literal >> 1]

def clause_to_string(self, clause):
return ' '.join(self.literal_to_string(l) for l in clause)

def assignment_to_string(self, assignment):
return ' '.join(v if assignment[i] else '~' + v
for i, v in enumerate(self.variables)
if assignment[i] is not None)


And the iterative algorithm:

from __future__ import division
from __future__ import print_function

from watchlist import setup_watchlist
from watchlist import update_watchlist

__author__ = 'Sahand Saba'

def solve(instance, verbose=False):
watchlist = setup_watchlist(instance)
if not watchlist:
return

# The state list wil keep track of what values for which variables
# we have tried so far. A value of 0 means nothing has been tried yet,
# a value of 1 means False has been tried but not True, 2 means True but
# not False, and 3 means both have been tried.
state =  * instance.n
assignment = [None] * instance.n
d = 0  # Current depth in the backtrack tree
while True:
if d == instance.n:
yield assignment
d -= 1
continue
# Let's try assigning a value to v. Here would be the place to insert
# heuristics of which value to try first.
tried_something = False
for a in [0, 1]:
if (state[d] >> a) & 1 == 0:
tried_something = True
# Set the bit indicating a has been tried for d
state[d] |= 1 << a
assignment[d] = a
if not update_watchlist(instance, watchlist,
d << 1 | 1 ^ a,
assignment,
verbose):
assignment[d] = None
else:
d += 1
break

if not tried_something:
if d == 0:
# Can't backtrack further. No solutions.
return
else:
# Backtrack
state[d] = 0
assignment[d] = None
d -= 1


I'm skipping a few of the files like watchlist.py and recursive_sat.py.

This review will focus on the command-line driver. Others will no doubt elaborate on the rest of your code.

## Piece-by-piece review

if __name__ == '__main__':


The Python convention is to extract everything that follows into a function, enabling you to better organize your code. This allows you to call functions defined further down rather than only ones defined above.

    parser = ArgumentParser(description=__doc__)
'--verbose',
help='verbose output.',
action='store_true')
'--recursive',
help='use the recursive backtracking algorithm.',
action='store_true')
'--input',
action='store')
args = parser.parse_args()


This arg-parsing code should be extracted as a function that does one thing, does it well, and does it only.

    instance = None
if args.input:
with open(args.input, 'r') as file:
instance = SATInstance.from_file(file)
else:
instance = SATInstance.from_file(stdin)

alg = recursive_sat.solve if args.recursive else iterative_sat.solve


If you read the argparse documentation more carefully, you will notice that you are not using its full capabilities. You can simplify this part of your program considerably if you let the ArgumentParser store the appropriate implementation of your algorithm directly. It can also handle the optional input file opening for you, falling back to stdin if none is supplied.

    for assignment in alg(instance, args.verbose):
print(instance.assignment_to_string(assignment))
else:
if args.verbose:
print('No satisfying assignment exists.', file=stderr)


The else branch of this for loop does not do what you think it does, so here's your bug:

Your program will always print the error message because the else branch of a for loop is always executed unless a break statement terminates the loop.

# Improved code

def main():
args = parse_args()
with args.input as file:
instance = SATInstance.from_file(file)
result = args.algorithm.solve(instance, args.verbose)
for assignment in result:
print(instance.assignment_to_string(assignment))
if not result and args.verbose:
print('No satisfying assignment exists.', file=stderr)

def parse_args():
parser = argparse.ArgumentParser(description=__doc__)
help='verbose output.',
action='store_true')
help='use the recursive backtracking algorithm.',
action='store_const',
dest='algorithm',
const=recursive_sat,
default=iterative_sat)

• This is great, thank you. Just one subtle correction to your suggestion: type=FileType() should be type=FileType without the () since otherwise it will throw an exception saying FileType requires one parameter. Apr 16, 2014 at 17:23
• On second thought, I realized you had argparse.FileType in mind, whereas my first thought was that it was types.FileType, which is the only FileType I knew about! With argparse.FileType you need the (). So your code is correct for Python 2 as well. Apr 17, 2014 at 0:11