You can work on this homework problem by yourself or with a
partner. Please let me know by Wednesday Oct 6th whether you will
work alone or with a partner, and, if you are working with a
partner, who that is.

For this assignment, you will implement a DPLL-Based SAT
solver. You can use whatever language you want, as long as it is
easy to execute your code on a linux machine.

I plan on having you extend your SAT solver in later assignments,
so try to write code that is well-designed so that you can modify
it later, as needed.

Make sure that you do the following.

Two good references for 1-3, below, in addition to the handout I
gave you can be found here:
http://www.ccs.neu.edu/home/pete/courses/Computational-Logic/2010-Fall/
Zhang_Malik_Quest_Efficient_Boolean_Satisfiability_Solvers.pdf

http://www.ccs.neu.edu/home/pete/courses/Computational-Logic/2010-Fall/
Een_Sorensson_Extensible_SAT_Solver.pdf

0. Use the standard DIMAS format (CNF).  See
http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html or any
other refernce.

1. Use a reasonable decision heuristic for selecting the next
variable. 

2. You must implement clause learning and non-chronological
backjumping.

3. SAT solvers spend most of their time performing BCP (or unit
resolution), so try to make this efficient (see the discussion in
the above paper about the 2-literal watching scheme).

4. Try your SAT solver on benchmark problems (see 2010 SAT race,
http://baldur.iti.uka.de/sat-race-2010/, or any other sources)
and compare your results with precosat
(http://fmv.jku.at/precosat/).

You should at least try the following benchmarks. From:

http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html

try the uf20-91 formulas, which should be *real* easy.  Even
the uuf250 class are easy for state of the art solvers.

Note, for the above problems, I needed to remove the last 3 lines
of the cnf files in order to have valid DIMACS files that
standard SAT solvers don't complain about.

Here is a simple example of how to do that.

First,

wc uuf250-098.cnf

reports 1076, so subtract 3 to get 1073 and run:

head -n 1073 uuf250-098.cnf >t-098.cnf

Also, these examples are characterized wrt whether they are sat
or not, so you could test your solver using them.

5. If you want to, you can implement restarts, learned clause
removal, etc, but this is entirely optional.

6. What you will hand in is your code, as well as a description of
your system that addresses the following points: 

- what language did you use and why?
- an overview of the techniques you implemented and how.
- experimental evaluation (see 4 above).
- if you worked with a partner, report on who did what and how
  successful the collaboration was.
- any interesting observations you made.