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:

Form into groups of two.
CHOOSE ONE of the following to implement:

The DPLL systematic satisfiability solver with the MOMS heuristic (i.e., at each step choosing the variable with the Maximum number of Occurrences in Minimum Size clauses).
The WALKSAT stochastic satisfiability solver.

Experiment with the solver. You will be provided with a generator that outputs random CNFs (see below). This program will allow you to vary the number of clauses and variables (and optionally, the clause length). Report how the time to solution varies with the ratio of clauses to variables.

You can earn up to 5% extra credit on this assignment by doing extended experimentation with satisfiability solvers. Explain any extra work that you've done in your write-up. You will be awarded extra points based on how original and well-justified your extra experimentation is. To earn the full 5% extra credit, implement and test your own satisfiability solver. Your solver can be a refinement of DPLL, a refinement of WALKSAT, combine elements of both, or incorporate a new approach of your own design.

What to turn in:

The code you wrote: DPLL or WALKSAT, and your own algorithm if you implemented one. Make sure to include any other code you used to run experiments. The code should be clear and reasonably documented (comments, brief description of architecture / guide to the code, and brief user manual). Also include instructions for building the executables and any command line options the grading program should use.
A description of what parts of the project were done by each of the two group members.
A report describing your experiments and results (and your solver, if you implemented one). This report should have a maximum of six letter-sized pages in 12pt font with 1" margins, including all tables and figures.

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

Stephen A. Cook and David G. Mitchell, Finding Hard Instances of the Satisfiability Problem: A Survey. In Satisfiability Problem: Theory and Applications. Du, Gu and Pardalos (Eds). Dimacs Series in Discrete Mathamatics and Theoretical Computer Science, Volume 35.

http://www.cs.utoronto.ca/~mitchell/papers/cook-mitchell.ps

Joao P. Marques-Silva, An Overview of Backtrack Search Satisfiability Algorithms. In Proc. Fifth International Symposium on Artificial Intelligence and Mathematics, January 1998.
[http://algos.inesc.pt/pub/users/jpms/papers/ai-math98/ai-math98.ps.gz]
David McAllester, Bart Selman, and Henry Kautz, Evidence for Invariants in Local Search. In Proc. AAAI-97, Providence, RI, 1997.
[http://www.research.att.com/~kautz/papers-ftp/invariants.ps]
Bart Selman, Henry Kautz, and David McAllester, Ten Challenges in Propositional Reasoning and Search. In Proc. IJCAI-97, Nagoya, Japan, 1997.
[http://www.research.att.com/~kautz/challenge/challenge.ps]
David S. Johnson, A Theoretician's Guide to the Experimental Analysis of Algorithms. Technical report, AT&T Research.
[http://www.research.att.com/~dsj/papers/exper.ps]

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:

numvars
numclauses
clauselength
clause1
clause2
...
clausen

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:

4
5
3
( 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:

Solution:
( 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.

The program "gen_cnf" will randomly generate CNFs using parameters you specify for the number of clauses and variables. For example, the command
```
 gen_cnf -c 5 -v 4 
```
... will generate a 5 clause, 4 variable 3-CNF on stdout. (The default clause length is 3, but this parameter can be varied as well with the -l switch). Use "gen_cnf -h" to get a listing of all the possible switches, and their syntax. gen_cnf for the FreeBSD OS is here. It has also been compiled for Linux and DOS.
The file run-exp.pl will 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 will check that the solution returned by your solver is valid.
Finally, you can download valid-prob.pl to generate valid problems.

Good luck!