LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:normal_forms_for_propositional_logic [2008/03/09 13:33]
thibaud Filled-in CNF
sav08:normal_forms_for_propositional_logic [2008/03/09 15:39]
thibaud Filled-in SAT preserving transformation to CNF
Line 26: Line 26:
 Solving the SAT problem for DNF formulas is in P, but transforming an arbitrary propositional formula to DNF causes an exponential blow-up. 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. 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.+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 === === Conjunctive Normal Form ===
Line 32: Line 40:
 Formulas in Conjunctive-normal form look like this:  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 ...$ \\ $(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} ​D_i$ and $D_i = \bigvee_{j=1}^{n_i} L_{ij}$ \\+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. Like for DNF, $L_{ij}$ are elementary propositions or their negation. The terminology of clauses and literals also applies to CNF.
  
Line 54: Line 62:
 === Circuits === === Circuits ===
  
-Circuits ​(acyclic graph labelled by propositional operatorsand 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 equivalentNote 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 variablewill 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 implicationsExample: \\ 
 +$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.