Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:homework04 [2008/03/12 18:37] vkuncak |
sav08:homework04 [2008/03/13 11:47] (current) vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Homework 04 -DRAFT ====== | + | ====== Homework 04 - due 19 March 2008 at 11:00 ====== |
| ===== Problem 1 ===== | ===== Problem 1 ===== | ||
| Line 7: | Line 7: | ||
| ===== Problem 2 ===== | ===== Problem 2 ===== | ||
| - | Build a SAT solver that accepts input in the CNF version of the [[DIMACS format]]. (The input file is a formula in conjunctive normal form, where each clause is given on a separate line as a list of indices denoting propositional variables, a negative index indicates a negated propositional variable.) | + | Implement the basic [[DPLL Algorithm for SAT]]. Your program should accepts input in the CNF version of the [[DIMACS format]]. (This input file is a formula in conjunctive normal form, where each clause is given on a separate line as a list of indices denoting propositional variables, a negative index indicates a negated propositional variable.) |
| - | If a given formula is satisfiable, the SAT solver should produce an assignment to all variables such that the formula evaluates to //true// under this assignment. | + | If a given formula is satisfiable, your SAT solver should produce an assignment to all variables such that the formula evaluates to //true// under this assignment. |
| - | If a given formula is unsatisfiable, the SAT solver should produce unsatisfiability proof in some format (we recommend that you use resolution trees, whose tree constructors take resolution subtrees and the variable on which resolution is performed). | + | If a given formula is unsatisfiable, for now the SAT solver can simply say "false". |
| - | You can look at the source code of existing implementations to gain insight into techniques (such as http://sourceforge.net/projects/dpt ) but you are not allowed to copy it, you must write your own implementation. | + | The expected level of sophistication is the simple DPLL solver with unit propagation described in [[DPLL Algorithm for SAT]], it is not required that you implement advanced techniques or very efficient data structures. |
| - | The expected level of sophistication is a DPLL solver with unit propagation, but you are encouraged to implement additional techniques. | + | You will extend your solver in [[homework05]]. |
| - | We will run a small competition of implemented solvers. | ||