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/09 12:45] thibaud Filled-in negation-normal paragraph |
sav08:normal_forms_for_propositional_logic [2008/03/09 15:39] thibaud Filled-in SAT preserving transformation to CNF |
||
---|---|---|---|
Line 18: | Line 18: | ||
=== 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 === |
+ | |||
+ | 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. | ||
- | No polynomial-time equivalence preserving transformation to CNF or to DNF. | + | There is no polynomial-time equivalence preserving transformation to CNF or to DNF. |
=== Complete Sets of Connectives === | === Complete Sets of Connectives === | ||
Line 48: | 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. | ||