LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
Next revision Both sides next revision
sav08:homework03 [2008/03/06 18:59]
vkuncak 		sav08:homework03 [2008/03/06 19:27]
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 produce equisatisfiable formulas. 
  
 ===== Problem 3: Equivalence Preserving Transformation to CNF ===== ===== Problem 3: Equivalence Preserving Transformation to CNF =====
Line 22: Line 30:
 in conjunctive normal form.  You do not need to use any deep results of complexity theory. in conjunctive normal form.  You do not need to use any deep results of complexity theory.
  
-Specifically,​ prove that there exists an infinite family of formulas $F_1, F_2,\ldots$ such that for each $n$ //any// algorithm that transforms $F_n$ to CNF needs exponential time.  (Note that it is not enough to prove that one particular algorithm will take exponential time, you need to prove that every algorithm would need exponential time.)+Specifically,​ prove that there exists an infinite family of formulas $F_1, F_2,\ldots$ such that for each $n$, //every// algorithm that transforms $F_n$ to CNF needs exponential time.  (Note that it is not enough to prove that one particular algorithm will take exponential time, you need to prove that every algorithm would need exponential time.)
  
 ===== Problem 4: NAND ===== ===== Problem 4: NAND =====
Line 31: Line 39:
 \] \]
 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.
-