Computer Science 242

Homework 3

You are asked to write a program which solves satisfiability problems using the Davis Putnam (DPLL) algorithm. You need to implement the following basic features of the algorithm:

Backtracking search

Early termination

Unit clause heuristic

Pure literal heuristic

Discussion Your README should explain how your implementation is organized, and analyze the benefit of the unit clause and pure literal heuristics.

The input and output formats should be as in HW 1, and the executable should be named sat. You can use the smoke_test script from hw1 to test your program.

Your program should take comand line options --nounit and --nopure to disable the unit clause heuristic and the pure literal heuristic. There are test input files under /u/cs242/hw3/inputs.

We have a checker that will validate your output. If you have an executable named sat in a directory named, for example, hw3, you can run

/u/cs242/hw3/checker hw3

The checker will run the test cases in /u/cs242/hw3/inputs/. It will check that your answer "satisfiable"/"unsatisfiable" is correct, and, if the answer is "satisfiable", it will check that the variable assignment printed by your program does in fact satisfy the sentence.