CSE logo

University of Washington Department of Computer Science & Engineering

 CSE 573 – Artificial Intelligence - Autumn 2004



Mini Project 1 - Satisfiability

[ CSE 573 2004 Autumn Home | Problem Sets | Mini Project 2 ]

In this project you should experiment with (at least) two different satisfiability solvers. An natural direction would be to compare a systematic algorithm (such as DPLL) and a stochastic one. Alternatively, you could pick one algorithmic family and try several variations, heuristics, data structures, or bookkepping strategies. In any case, you should study them experimentally, and try to design and test your own improved solver. Below, I describe one way that you might go, but feel free to try something different. Regardless of your approach, however, I would like you to abide by the file formats described below.

Recommended reading:

Much of the recent research on satisfiability has appeared in AAAI, the National Conference on Artificial Intelligence. The proceedings are available in the library, and many of the papers can be found online.

Standard file formats to be used:

Your sat-solver should accept files of the following format:


Where numvars, numclauses and clauselength are integers and the format for a clause is a parenthesized list of literals.

( lit1 lit2 ... litm )
Literals will be represented by integers, with negated literals represented by negative numbers. For example, the 5-clause, 4-variable 3-CNF formula
( A1 v ~A2 v A3) ^ ( ~A3 v ~A1 v A4 ) ^ ( A2 v A1 v ~A4 ) 
  ^ ( ~A2 v A3 v ~A4) ^ ( ~A1 v A2 v A3 )
Would be represented by the file:
( 1 -2 3 )
( -3 -1 4 )
( 2 1 -4 )
( -2 3 -4 )
( -1 2 3 )
The program should have, somewhere in its output, a line that reads "Solution:" followed by a line with the string "Fail" if no solution was found or a parenthesized list of variable assignments sorted by variable number.  So for the input above, the program might print:
( 1 2 -3 -4 )
Meaning that the variable assignment:
A1 = True, A2 = True, A3 = False, A4 = False
was found as a solution to this problem.

Note the spaces before and after each literal in the above i/o formats.

Your program should be able to read the test file from the standard input stream. Any parameters your program uses should be set using command line options.  For example, if you want to be able to control the number of restarts and flips, you should create command line options.

walksat -r10000 -f1000 < problem.wff > problem.out
The generate program should take at least three inputs: numvars, numclauses and clauselen. Any other inputs you'd like to specify should be clearly documented.

Code provided: To help with the experimentation phase, we are providing some infrastructure, but note that this has not been checked and may suffer from bit-rot. No warranty provided. The file run-exp.pl should do multiple runs of your program over test files.  See the file itself for a description of how to use it.  The file check-soln.pl should check that the solution returned by your solver is valid.  They're both perl scripts, so after saving them on a unix system, you'll have to make them executable.

chmod 700 run-exp.pl

Computer Science & Engineering Department
University of Washington
PO Box 352350

Seattle, WA 98195-2350 USA