• 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)
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 variablewill 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 implicationsExample: \\
+$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.