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__)
parser.add_argument('-v',
'--verbose',
help='verbose output.',
action='store_true')
parser.add_argument('-r',
'--recursive',
help='use the recursive backtracking algorithm.',
action='store_true')
parser.add_argument('-i',
'--input',
help='read from given file instead of stdin.',
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):
def _parse_and_add_clause(self, line):
"""
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._parse_and_add_clause(line)
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 = [0] * 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.
