Differences

This shows you the differences between two versions of the page.

--- sav08:homework04 [2008/03/11 18:52]
vkuncak
+++ sav08:homework04 [2008/03/12 18:37]
vkuncak
@@ Line 9: / Line 9: @@
 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.)
-If a given formula is unsatisfiable, the SAT solver should produce unsatisfiability proof in some format.
+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, the SAT solver should produce an assignment to all variables for which the formula evaluates to //true//.
+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).
 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.