# First Project: Satisfiability Solvers

## Due Date: Friday, May 5, 2000

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

## What to do:

• Form into groups of two. Provide the necessary information for your group here.
• 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.
• A generator of satisfiability problems in CNF (conjunctive normal form).

• This generator will input the desired number of variables, clauses, variables per clause, and any other parameters you may decide to allow, and output a random CNF formula. Successive calls to the generator should produce different random CNFs.
• Study and compare the two solvers experimentally.

• Characterize the hard and easy (types of) problems for each. Identify the similarities and differences between the problems that are hard for DPLL and those that are hard for WALKSAT. "Hard" and "easy" should be measured in terms of how long it takes to produce an answer, be it positive or negative (and of the percentage of problems for which the time bounds you set were exceeded). In other words, the fundamental dependent variable in your empirical study will be the time to solution, and the independent variables will be the parameters you allow in the generator and relations among them (e.g., the ratio of clauses to variables). Note that the algorithms may require significant parameter tuning to perform well, and that this tuning is a significant part of the experimental work. Your writeup (see below) should discuss this process and what you learned from it.
• For extra credit (an additional 5% of the class grade, for a total of 30% for this project), 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. Your grade in this part of the project will depend on how original and well-justified your solver is, and on how well it does in the experiments compared to DPLL and WALKSAT.

## What to turn in:

• The code you wrote: DPLL, WALKSAT, your own algorithm if you implemented one, problem generator(s), and 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.

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:
```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 )```
Would be represented by the file:
```4
5
3
( 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:
```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 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. 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.  They're both perl scripts, so after saving them on a unix system, you'll have to make them executable. (The previous version of run-exp.pl is renamed to old-run-exp.pl and is here.)
`chmod 700 run-exp.pl check-soln.pl`