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:homework03 [2008/03/06 19:06] vkuncak |
sav08:homework03 [2008/03/06 19:26] vkuncak |
||
|---|---|---|---|
| Line 15: | Line 15: | ||
| ===== Problem 2: Satisfiability-Preserving Translation to CNF ===== | ===== Problem 2: Satisfiability-Preserving Translation to CNF ===== | ||
| - | Prove correctness of polarity-based improvements for satisfyability-preserving transforming to CNF. | + | Your goal here is to prove key steps in transformation of a formula containing $\land,\lor,\lnot$ to equisatisfiable CNF formula. The key transformation steps that introduce fresh variables for formula subtrees can be summarized as follows: |
| + | \[\begin{array}{l} | ||
| + | F\ \ \leadsto\ \ (p_i \leftrightarrow (q \land r)) \land subst(\{q \land r \mapsto p_i\},F) \\ | ||
| + | F\ \ \leadsto\ \ (p_i \leftrightarrow (q \lor r)) \land subst(\{q \lor r \mapsto p_i\},F) \\ | ||
| + | F\ \ \leadsto\ \ (p_i \leftrightarrow (\lnot q)) \land subst(\{(\lnot q) \mapsto p_i\},F) \\ | ||
| + | \end{array} | ||
| + | \] | ||
| + | Note that each introduced equivalence such as $(p_i \leftrightarrow (q \land r))$ can generate several clauses. Suppose now that $F$ is in negation-normal form. Show that we can replace some of these equivalences with implications. Write the new transformation rules and prove that they are satisfiability-preserving. | ||
| ===== Problem 3: Equivalence Preserving Transformation to CNF ===== | ===== Problem 3: Equivalence Preserving Transformation to CNF ===== | ||
| Line 31: | Line 38: | ||
| \] | \] | ||
| Show that for each propositional formula $F$ there exists an equivalent formula that uses $\barwedge$ as the only operator. | Show that for each propositional formula $F$ there exists an equivalent formula that uses $\barwedge$ as the only operator. | ||
| - | |||