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)
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 =  * 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