Presentation and submission of report: Monday 4 June

There are a number of ways to enumerate all models of a CNF formula F. Consider the following three:

Run directed resolution on F, construct a decision tree from the result, and enumerate models from the decision tree.
Run a SAT solver on F; if a model is found, add an appropriate clause to F to eliminate that model (and nothing else), and run the SAT solver again; repeat until the SAT solver reports "unsatisfiable."
Compile F into a propositional language that supports model enumeration, and enumerate models from the result.

Implement two of these methods, and run your programs on some CNF formulas. Write a report in which you (1) describe what you have done, (2) compare the performance of the two programs in terms of their running time on the set of CNF formulas used (the model count should also be reported for each CNF formula), (3) discuss any findings or thoughts you may have. You will be given 10 minutes to present your report during class on Friday 1 June.

Notes:

You can download CNF formulas from SATLIB. Note that some formulas can have a large number of models, so start with the smaller ones, uf20-91 and flat30-60 for example.
For Method 2, you can use any publicly available SAT solver, or your own if you have written one.
For Method 3, you can use the C2D compiler, which compiles CNF formulas into d-DNNF. Use the following command line when running C2D: "c2d -dt_method 4 -in foo.cnf" where "foo.cnf" is the name of your CNF file. It will save the d-DNNF in a file named "foo.nnf".