Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:homework04 [2008/03/12 18:37] vkuncak |
sav08:homework04 [2008/03/12 18:41] vkuncak |
||
|---|---|---|---|
| Line 11: | Line 11: | ||
| 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 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, the SAT solver should produce unsatisfiability proof in some format (we recommend that you use proof trees for resolution proofs, whose nodes indicate the variable on which resolution is performed and contain subtrees for proofs of clauses 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. | 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. | ||