Differences

This shows you the differences between two versions of the page.

--- 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:03]
thibaud Filled-in Circuits
@@ Line 18: / Line 18: @@
 === 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 ===
@@ Line 48: / Line 62: @@
 === 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.
 === Satisfiability-Preserving Transformation ===