• English only

# Differences

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

 sav08:normal_forms_for_propositional_logic [2008/03/09 15:03]thibaud Filled-in Circuits sav08:normal_forms_for_propositional_logic [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2008/03/09 15:39 thibaud Filled-in SAT preserving transformation to CNF2008/03/09 15:03 thibaud Filled-in Circuits2008/03/09 13:33 thibaud Filled-in CNF2008/03/09 13:25 thibaud Filled-in DNF2008/03/09 12:45 thibaud Filled-in negation-normal paragraph2008/03/06 13:55 vkuncak 2008/03/06 13:54 vkuncak 2008/03/06 13:54 vkuncak 2008/03/06 13:34 vkuncak 2008/03/06 12:15 vkuncak 2008/03/06 11:47 vkuncak 2008/03/06 11:38 vkuncak 2008/03/06 11:26 vkuncak 2008/03/06 11:25 vkuncak 2008/03/06 11:21 vkuncak 2008/03/05 21:12 vkuncak 2008/03/05 20:46 vkuncak created Next revision Previous revision 2008/03/09 15:39 thibaud Filled-in SAT preserving transformation to CNF2008/03/09 15:03 thibaud Filled-in Circuits2008/03/09 13:33 thibaud Filled-in CNF2008/03/09 13:25 thibaud Filled-in DNF2008/03/09 12:45 thibaud Filled-in negation-normal paragraph2008/03/06 13:55 vkuncak 2008/03/06 13:54 vkuncak 2008/03/06 13:54 vkuncak 2008/03/06 13:34 vkuncak 2008/03/06 12:15 vkuncak 2008/03/06 11:47 vkuncak 2008/03/06 11:38 vkuncak 2008/03/06 11:26 vkuncak 2008/03/06 11:25 vkuncak 2008/03/06 11:21 vkuncak 2008/03/05 21:12 vkuncak 2008/03/05 20:46 vkuncak created Line 4: Line 4: In Negation-normal from, negations are only allowed on elementary proposition. Moreover, NNF formulas contain no implication,​ so the only binary operators are conjunctions and disjunctions. The following rules can be used to turn arbitrary propositional formulas into negation-normal form. In Negation-normal from, negations are only allowed on elementary proposition. Moreover, NNF formulas contain no implication,​ so the only binary operators are conjunctions and disjunctions. The following rules can be used to turn arbitrary propositional formulas into negation-normal form. - $\begin{array}{l} + \begin{equation*}\begin{array}{l} \lnot (p \land q) \leftrightarrow (\lnot p) \lor (\lnot q) \\ \lnot (p \land q) \leftrightarrow (\lnot p) \lor (\lnot q) \\ p \leftrightarrow ​ \lnot (\lnot p) \\ p \leftrightarrow ​ \lnot (\lnot p) \\ Line 10: Line 10: \lnot (p \lor q) \leftrightarrow (\lnot p) \land (\lnot q) \lnot (p \lor q) \leftrightarrow (\lnot p) \land (\lnot q) \end{array} \end{array} -$ + \end{equation*} Note that this transformation is linear in the size of the formula. No exponential blow-up. Note that this transformation is linear in the size of the formula. No exponential blow-up. Line 66: Line 66: The if-then-else primitive, written $ite(p, q ,r)$, that yields $q$ whenever $p$ is true and $r$ otherwise, can be encoded with the following propositional logic formula: $(p \land q) \lor (\lnot p \land r)$ The if-then-else primitive, written $ite(p, q ,r)$, that yields $q$ whenever $p$ is true and $r$ otherwise, can be encoded with the following propositional logic formula: $(p \land q) \lor (\lnot p \land r)$ - For each node of an AST, it is possible to replace it with a fresh variable, provided that a clause is added that makes sure that the fresh variable and the sub-tree it represents are equivalent. + For each node of an AST, it is possible to replace it with a fresh variable, provided that a clause is added that makes sure that the fresh variable and the sub-tree it represents are equivalent. Note that this transformation preserve equisatisfiability but not equivalence,​ because it introduces new variables. === Satisfiability-Preserving Transformation === === Satisfiability-Preserving Transformation === - Fresh variable ​idea: general technique for eliminating ​(or postponing) exponential ​blowup. + There exists a linear transformation from arbitrary formulas to CNF preserving equisatisfiability. The main idea is to use fresh variables as described above. For each node of the AST, a representative ​(i.e. a fresh variable) will be introduced. We need to add clauses to ensure that a sub-formula and its representative are equivalent. To avoid exponential ​blow-up, we will not use the sub-formulas'​ children directly, but their representative when expressing this constraint. - Satisfiability preserving ​transformation to CNF. + The key transformation ​steps are: + \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 \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} + \end{equation*} + + Each equivalence between a representative and the ones from the sub-formulas has to be flatten to conjunctive-normal form. This can be done by splitting the equivalences into two implications. Example: \\ + $p \leftrightarrow q_1 \land q_2$ becomes $(\lnot p \lor q_1) \land (\lnot p \lor q_2) \land (\lnot q_1 \lor \lnot q_2 \lor p)$ - Flattening, expressing everything using $\land, \lnot$ which in turn become clauses. + Recall [[homework03]]. Optimization:​ for cases of only positive or only negative polarity. Optimization:​ for cases of only positive or only negative polarity.