3
\$\begingroup\$

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.

\$\endgroup\$
3
\$\begingroup\$

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__)
    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()

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__)
    parser.add_argument('-v', '--verbose',
                        help='verbose output.',
                        action='store_true')
    parser.add_argument('-r', '--recursive',
                        help='use the recursive backtracking algorithm.',
                        action='store_const',
                        dest='algorithm',
                        const=recursive_sat,
                        default=iterative_sat)
    parser.add_argument('-i', '--input',
                        help='read from given file instead of stdin.',
                        type=argparse.FileType(),  # opens the supplied file
                        default=stdin)
    return parser.parse_args()


if __name__ == '__main__':
    main()
\$\endgroup\$
3
  • \$\begingroup\$ 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. \$\endgroup\$ – Sahand Apr 16 '14 at 17:23
  • \$\begingroup\$ 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. \$\endgroup\$ – Sahand Apr 17 '14 at 0:11
  • 1
    \$\begingroup\$ @Sahand ah, that makes sense. Sorry for the confusion, I should have included the full name. \$\endgroup\$ – Adam Apr 17 '14 at 0:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.