Department of Computer Science and Engineering CSE 150
University of California at San Diego Fall 2004

 

Assignment 2

DUE MONDAY NOVEMBER 1 AT 5 PM.


The purpose of this project is to implement two different algorithms for testing propositional satisfiability, namely the DPLL and Walksat algorithms explained in class, and to do interesting experiments with them.

For this project, you may use Java, C, or C++.  If you want to use a different language, contact the instructor.  Using C is strongly recommended, because speed is very important for SAT solvers.  Think carefully what data structures you need to use to make your implementations fast. 

Both the DPLL and Walksat algorithm use heuristics.  Your job is to invent your own heuristic for each algorithm, and to do an experimental study of its success.  Use your creativity, but also use your knowledge and your ability to think critically!  For DPLL you should invent a heuristic for variable ordering.  For Walksat you should invent a heuristic for which variable to choose, among all variables belonging to unsatisfied clauses.

You can debug your implementations using the random 3SAT problem instances with 20 variables available at http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html.  Note that these small 3SAT instances are all satisfiable. 

WHAT TO PUT IN YOUR REPORT

In your report, you should explain your heuristics in high-level pseudocode.  You should also explain brief motivations for them, i.e. why they seem like good choices.  You must think about your heuristics at a conceptual level.  You should also explain how you make Walksat deal with unsatisfiable 3SAT instances.  When (e.g. after how many flips) is it reasonable for Walksat to stop and declare failure?

Run both your algorithms systematically on all 2000 3SAT instances with 100 variables and 430 clauses available in SATLIB (these files are named uf100-430 and uuf100-430).  For each algorithm and each instance, measure the runtime.  For Walksat, also measure the number of variable flips.  For DPLL, measure the search tree size.  For each algorithm, plot graphically the measurements you get for satisfiable instances, and separately the measurements for unsatisfiable instances.  In your report, explain briefly the conclusions you draw from these plots.

CODING INSTRUCTIONS

Your DPLL and Walksat programs should compile with the command make.  Each should take exactly one command line argument, a file name.  The named file will contain one well-formatted 3-CNF formula.  Make sure you understand the input format of the problem instances.  Each program should determine if the formula is satisfiable or not. For example, if the names of your executables are dpll and walksat, and the input file is named uf50-01.cnf, then the commands would be:

./dpll uf50-01.cnf
./walksat uf50-01.cnf

There should be no inputs to your programs other than the file name.  All algorithm parameters should be set in your code to good values that you determine experimentally. 

The output for DPLL should have the following form:

Satisfying assignment found: 0 or 1

The output for Walksat should have the following form:

Number of restarts performed: an integer
Number of flips performed: an integer
Satisfying assignment found: 0 or 1

GENERAL INSTRUCTIONS

Here are detailed instructions for how to submit your code.  You will submit a printout of your report at the start of class on the due date.  The maximum length of the report is four pages single-spaced, not counting the title page.  The recommended length is about three pages single-spaced.  Remember to check the class web page and WebCT regularly for possible updates to this project description.

This project will be graded as follows:

Your software should have good organization, useful comments, and decent speed.  It must be as concise and straightforward as possible.  For this project, you should work by yourself or in a team of two students.  You may get assistance from the TAs, the 134A discussion board, the web, and books, but not from students outside your team.  You should not copy any existing code.  Complete academic honesty is always required.

Your report should be written using a word processor and printed on 8.5x11 paper.  It should be concise but complete enough to be understandable by itself, and written in good English.  The report should include a short introduction and be divided into appropriate sections.  Use diagrams, tables, and charts when necessary.  Avoid spelling and grammar mistakes by repeated proofreading.  Remember that these mistakes and incorrect vocabulary tend to make readers underestimate the value of your technical work.