Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next 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 13:25] thibaud Filled-in DNF |
||
---|---|---|---|
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 | + | 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. 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. |
=== Conjunctive Normal Form === | === Conjunctive Normal Form === |