LARA

Differences

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

Link to this comparison view

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]
Line 1: Line 1:
-====== Normal Forms for Propositional Logic ====== 
- 
-=== 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]]. 
- 
-Polarity of formula. 
- 
-=== 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. 
- 
-Solving the SAT problem for DNF formulas is in P, but transforming an arbitrary propositional formula to DNF causes an exponential blow-up. 
- 
-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)$ 
- 
-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 === 
- 
-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 === 
- 
-If we can express every formula. ​ Examples: 
-  * $\{\land, \lor, \lnot\}$ because every formula has DNF (or CNF) 
- 
-  * $\{\land,​\lnot\}$ 
- 
-  * $\{\lor,​\lnot\}$ 
- 
-  * $\{\rightarrow,​{\it false}\}$ 
- 
-  * $\{\barwedge\}$ 
- 
-  * $\{\veebar\}$ 
- 
-=== Circuits === 
- 
-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 === 
- 
-Fresh variable idea: general technique for eliminating (or postponing) exponential blowup. 
- 
-Satisfiability preserving transformation to CNF. 
- 
-Flattening, expressing everything using $\land, \lnot$ which in turn become clauses. 
- 
-Optimization:​ for cases of only positive or only negative polarity.