- English only

# Lab for Automated Reasoning and Analysis LARA

# 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 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. | ||