- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

sav08:qbf_and_quantifier_elimination [2008/03/10 11:17] vkuncak |
sav08:qbf_and_quantifier_elimination [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 1: | Line 1: | ||

====== QBF and Quantifier Elimination ====== | ====== QBF and Quantifier Elimination ====== | ||

- | === Quantified Propositional Formula Syntax === | + | ===== Quantified Propositional Formula Syntax ===== |

We extend the definition of formulas with quantifiers $\forall p.F$ and $\exists p.F$ where $p \in V$: | We extend the definition of formulas with quantifiers $\forall p.F$ and $\exists p.F$ where $p \in V$: | ||

- | \[\begin{array}{rcl} | + | \begin{equation*}\begin{array}{rcl} |

F & ::= & V \mid {\it false} \mid {\it true} \mid (F \land F) \mid (F \lor F) \mid (\lnot F) \mid (F \rightarrow F) \mid (F \leftrightarrow F) \\ | F & ::= & V \mid {\it false} \mid {\it true} \mid (F \land F) \mid (F \lor F) \mid (\lnot F) \mid (F \rightarrow F) \mid (F \leftrightarrow F) \\ | ||

& \mid & \forall V. F\ \mid\ \exists V. F | & \mid & \forall V. F\ \mid\ \exists V. F | ||

\end{array} | \end{array} | ||

- | \] | + | \end{equation*} |

- | === Eliminating quantifiers by expansion === | + | ===== Eliminating quantifiers by expansion ===== |

We can apply the following rules to eliminate propositional quantifiers: | We can apply the following rules to eliminate propositional quantifiers: | ||

- | \[ | + | \begin{equation*} |

\exists p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \lor subst(\{p \mapsto {\it true}\},F) | \exists p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \lor subst(\{p \mapsto {\it true}\},F) | ||

- | \] | + | \end{equation*} |

- | \[ | + | \begin{equation*} |

\forall p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \land subst(\{p \mapsto {\it true}\},F) | \forall p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \land subst(\{p \mapsto {\it true}\},F) | ||

- | \] | + | \end{equation*} |

Note that the expansion can produce exponentially larger formula. | Note that the expansion can produce exponentially larger formula. | ||

Notion of quantifier elimination applies to other logic as well. | Notion of quantifier elimination applies to other logic as well. | ||

- | Definition: A logic has //quantifier elimination// if for every formula in the logic, there exists an equivalent formula without quantifiers. | + | **Definition:** A logic has //quantifier elimination// if for every formula in the logic, there exists an equivalent formula without quantifiers. |

- | Definition: A quantifier elimination algorithm is an algorithm that takes a formula in a logic and converts it into an equivalent formula without quantifiers. | + | **Definition:** A quantifier elimination algorithm is an algorithm that takes a formula in a logic and converts it into an equivalent formula without quantifiers. |

- | Note: Formula $F$ is valid iff $\forall p_1,\ldots,p_n. F$ is true. | + | **Observation:** Formula $F$ is valid iff $\forall p_1,\ldots,p_n. F$ is true. |

- | Note: Formula $F$ is satisfiable iff $\exists p_1,\ldots,p_n. F$ is true. | + | **Observation:** Formula $F$ is satisfiable iff $\exists p_1,\ldots,p_n. F$ is true. |

In general QBF formulas can have alternations between $\forall$ and $\exists$ quantifiers: | In general QBF formulas can have alternations between $\forall$ and $\exists$ quantifiers: | ||

- | \[ | + | \begin{equation*} |

\forall p. \exists q. ((p \rightarrow q) \land (q \rightarrow r)) | \forall p. \exists q. ((p \rightarrow q) \land (q \rightarrow r)) | ||

- | \] | + | \end{equation*} |

- | === Quantified Propositional Formula Semantics === | + | ===== Quantified Propositional Formula Semantics ===== |

We can similarly provide recursive semantic function definition for propositional logic. | We can similarly provide recursive semantic function definition for propositional logic. | ||

- | === Notes on Computational Complexity === | + | ===== Summary of Computational Complexity of Problems ===== |

* checking satisfiability of propositional formula $F$ is NP-complete | * checking satisfiability of propositional formula $F$ is NP-complete |