simple-sat, 在 python 中，编写了简单的递归和迭代SAT求解器.zip

#!/usr/bin/env python """ Solves SAT instance by reading from stdin using an iterative or recursive watchlist-based backtracking algorithm. Iterative algorithm is used by default, unless the --recursive flag is given. Empty lines and lines starting with a # will be ignored. """ from __future__ import division from __future__ import print_function from argparse import ArgumentParser from argparse import FileType from sys import stdin from sys import stdout from sys import stderr from satinstance import SATInstance from solvers.watchlist import setup_watchlist from solvers import recursive_sat from solvers import iterative_sat __author__ = 'Sahand Saba' def generate_assignmnets(instance, solver, verbose=False): """ Returns a generator that generates all the satisfying assignments for a given SAT instance, using algorithm given by alg. """ n = len(instance.variables) watchlist = setup_watchlist(instance) if not watchlist: return () assignment = [None] * n return solver.solve(instance, watchlist, assignment, 0, verbose) def run_solver(input_file, output_file, solver, brief, verbose, output_all, starting_with): """ Run the given solver for the given file-like input object and write the output to the given output file-like object. """ instance = SATInstance.from_file(input_file) assignments = generate_assignmnets(instance, solver, verbose) count = 0 for assignment in assignments: count += 1 if verbose: print('Found satisfying assignment #{}:'.format(count), file=stderr) assignment_str = instance.assignment_to_string( assignment, brief=brief, starting_with=starting_with ) output_file.write(assignment_str + '\n') if not output_all: break if verbose and count == 0: print('No satisfying assignment exists.', file=stderr) def main(): args = parse_args() with args.input: with args.output: run_solver(args.input, args.output, args.solver, args.brief, args.verbose, args.all, args.starting_with) def parse_args(): parser = ArgumentParser(description=__doc__) parser.add_argument('-v', '--verbose', help='verbose output.', action='store_true') parser.add_argument('-a', '--all', help='output all possible solutions.', action='store_true') parser.add_argument('-b', '--brief', help=('brief output:' ' only outputs variables assigned true.'), action='store_true') parser.add_argument('--starting_with', help=('only output variables with names' ' starting with the given string.'), default='') parser.add_argument('--iterative', help='use the iterative algorithm.', action='store_const', dest='solver', default=recursive_sat, const=iterative_sat) parser.add_argument('-i', '--input', help='read from given file instead of stdin.', type=FileType('r'), default=stdin) parser.add_argument('-o', '--output', help='write to given file instead of default stdout.', type=FileType('w'), default=stdout) return parser.parse_args() if __name__ == '__main__': main()