Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:homework03 [2008/03/06 19:29] vkuncak |
sav08:homework03 [2015/04/21 17:30] (current) |
||
|---|---|---|---|
| Line 4: | Line 4: | ||
| Extend propositional formulas with NAND operator, denoted $\barwedge$ and defined by | Extend propositional formulas with NAND operator, denoted $\barwedge$ and defined by | ||
| - | \[ | + | \begin{equation*} |
| x \barwedge y = \lnot (x \land y) | x \barwedge y = \lnot (x \land y) | ||
| - | \] | + | \end{equation*} |
| 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. | ||
| Line 12: | Line 12: | ||
| 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: | 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} | + | \begin{equation*}\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 \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 (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) \\ | F\ \ \leadsto\ \ (p_i \leftrightarrow (\lnot q)) \land subst(\{(\lnot q) \mapsto p_i\},F) \\ | ||
| \end{array} | \end{array} | ||
| - | \] | + | \end{equation*} |
| 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 produce equisatisfiable formulas. | 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 produce equisatisfiable formulas. | ||