patternpythonMinor

Simple SAT Solver In Python

Submitted by: @import:stackexchange-codereview·Mar 10, 2026·

Viewed 0 times

satsolversimplepython

Problem

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 = SATI

Solution

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

Code Snippets

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)

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

Context

StackExchange Code Review Q#47312, answer score: 3

Revisions (0)

No revisions yet.