Lab for Automated Reasoning and Analysis 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] (current)
Line 4: Line 4:
  
 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. 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}+\begin{equation*}\begin{array}{l}
   \lnot (p \land q) \leftrightarrow (\lnot p) \lor (\lnot q) \\   \lnot (p \land q) \leftrightarrow (\lnot p) \lor (\lnot q) \\
   p \leftrightarrow ​ \lnot (\lnot p) \\   p \leftrightarrow ​ \lnot (\lnot p) \\
Line 10: Line 10:
   \lnot (p \lor q) \leftrightarrow (\lnot p) \land (\lnot q)   \lnot (p \lor q) \leftrightarrow (\lnot p) \land (\lnot q)
 \end{array} \end{array}
-\]+\end{equation*}
 Note that this transformation is linear in the size of the formula. No exponential blow-up. Note that this transformation is linear in the size of the formula. No exponential blow-up.
  
Line 66: Line 66:
 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)$ 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.+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 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
  
-Satisfiability preserving ​transformation to CNF.+The key transformation ​steps are: 
 +\begin{equation*}\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} 
 +\end{equation*} 
 + 
 +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.
  
 
sav08/normal_forms_for_propositional_logic.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice