First Project: A Satisfiability Solver

Due Date: Friday, October 27th

In this project you will implement either a systematic satisfiability solver or a stochastic one, and study it experimentally.

What to do:

What to turn in:

We may ask you to do a demo / oral discussion of the project.
Acceptable languages for the project are: LISP, C/C++, and Java. Other languages may be allowed by special request.

Background reading:

(Not indispensable, but helpful.) 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 must 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) v ( ~A1 v A2 v A3 )
Will be output by the generator as:
( 1 -2 3 )
( -3 -1 4 )
( 2 1 -4 )
( -2 3 -4 )
( -1 2 3 )
Your 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. The grading program will require that you follow the correct format exactly.

Your program should be able to read the generator output from the standard input stream. Any parameters your program uses should be set using command line options (again, which you've taken care to document). 

Code provided:

To help with the experimentation phase, we are providing some infrastructure. NOTE: After saving these files on a Unix system, you'll have to make them executable. Use "chmod 700 [filename]" to change the permissions on the files.

Good luck!