Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:normal_forms_for_propositional_logic [2008/03/06 13:55] vkuncak |
sav08:normal_forms_for_propositional_logic [2008/03/09 15:39] thibaud Filled-in SAT preserving transformation to CNF |
||
---|---|---|---|
Line 2: | Line 2: | ||
=== Negation-Normal Form === | === 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} | ||
+ | \lnot (p \land q) \leftrightarrow (\lnot p) \lor (\lnot q) \\ | ||
+ | p \leftrightarrow \lnot (\lnot p) \\ | ||
+ | (p \rightarrow q) \leftrightarrow ((\lnot p) \lor q) \\ | ||
+ | \lnot (p \lor q) \leftrightarrow (\lnot p) \land (\lnot q) | ||
+ | \end{array} | ||
+ | \] | ||
+ | Note that this transformation is linear in the size of the formula. No exponential blow-up. | ||
Recall [[homework01]]. | Recall [[homework01]]. | ||
Polarity of formula. | Polarity of formula. | ||
- | |||
- | Size of NNF ? | ||
=== Disjunctive Normal Form === | === Disjunctive Normal Form === | ||
+ | Formulas in Disjunctive-normal form look like this: | ||
+ | $(x_1 \land x_2 \land \lnot x_3) \lor (\lnot x_1 \land x_3 \land x_4) \lor ...$ \\ | ||
+ | More formally $F = \bigvee^{n}_{i=1} D_i$ where $n \geq 0$. \\ | ||
+ | Each $D_i$ is a clause and is defined as $D_i = \bigwedge_{j=1}^{n_i} L_{ij}$. \\ | ||
+ | Each $L_{ij}$ is a literal. It's either an elementary proposition or its negation. | ||
- | Complete disjunctive normal form and truth tables. | + | Solving the SAT problem for DNF formulas is in P, but transforming an arbitrary propositional formula to DNF causes an exponential blow-up. |
- | * generating DNF from truth table | + | |
- | * generating DNF by transformations | + | |
- | === Conjunctive Normal Form === | + | DNF formulas can be easily generated from truth tables. Each row of the truth table that makes the formula true can be written as a clause. Here is an example: |
+ | ^ $x_1$ ^ $x_2$ ^ $F$ ^ | ||
+ | | 0 | 0 | 0 | | ||
+ | | 1 | 0 | 1 | | ||
+ | | 0 | 1 | 1 | | ||
+ | | 1 | 1 | 0 | | ||
+ | The corresponding formula in DNF is $(x_1 \land \lnot x_2) \lor (\lnot x_1 \land x_2)$ | ||
- | CNF | + | For a formula over $n$ variables, there are $2^{n}$ rows in the truth table. Over $n$ variables, there are $2^{2^{n}}$ different (i.e. non-equivalent) formulas. |
- | Literal. Clause. | + | === Conjunctive Normal Form === |
- | No polynomial-time equivalence preserving transformation to CNF or to DNF. | + | Formulas in Conjunctive-normal form look like this: |
+ | $(x_1 \lor x_2 \lor \lor x_3) \land (\lnot x_1 \lor x_3 \lor x_4) \land ...$ \\ | ||
+ | It's defined as $F = \bigwedge^{n}_{i=1} \bigvee_{j=1}^{n_i} L_{ij}$ \\ | ||
+ | Like for DNF, $L_{ij}$ are elementary propositions or their negation. The terminology of clauses and literals also applies to CNF. | ||
+ | |||
+ | There is no polynomial-time equivalence preserving transformation to CNF or to DNF. | ||
=== Complete Sets of Connectives === | === Complete Sets of Connectives === | ||
Line 40: | Line 62: | ||
=== Circuits === | === Circuits === | ||
- | Circuits (acyclic graph labelled by propositional operators) and formulas. if-then-else expression. Fresh variables. | + | Formulas can be represented as abstract syntax tree (AST) where each node is labeled with an operator that applies to the sub-tree(s). If two sub-trees are identical, instead of duplicating the sub-tree in each place where its used, one can make all the references to this sub-tree point to a unique representation of it. This is called a circuit. |
+ | |||
+ | 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. 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. |
+ | |||
+ | The key transformation steps are: | ||
+ | \[\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} | ||
+ | \] | ||
- | Satisfiability preserving transformation to CNF. | + | 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. | ||