Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:qbf_and_quantifier_elimination [2008/03/10 11:13] vkuncak |
sav08:qbf_and_quantifier_elimination [2008/03/10 11:16] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== QBF and Quantifier Elimination ====== | ====== QBF and Quantifier Elimination ====== | ||
| - | Quantified Propositional Formulas: syntax and semantics. | + | === Quantified Propositional Formula Syntax === |
| - | Eliminating quantifiers by expansion: | + | We extend the definition of formulas with quantifiers $\forall p.F$ and $\exists p.F$ where $p \in V$: |
| + | \[\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) \\ | ||
| + | & & \forall V. F\ \mid\ \exists V. F | ||
| + | \end{array} | ||
| + | \] | ||
| + | |||
| + | === Eliminating quantifiers by expansion === | ||
| + | |||
| + | We can apply the following rules to eliminate propositional quantifiers: | ||
| \[ | \[ | ||
| \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) | ||
| Line 14: | Line 23: | ||
| Notion of quantifier elimination applies to other logic as well. | Notion of quantifier elimination applies to other logic as well. | ||
| - | 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. |
| - | 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. |
| - | Formula $F$ is valid iff $\forall p_1,\ldots,p_n. F$ is true. | + | Note: Formula $F$ is valid iff $\forall p_1,\ldots,p_n. F$ is true. |
| - | Formula $F$ is satisfiable iff $\exists p_1,\ldots,p_n. F$ is true. | + | Note: 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: | ||
| Line 27: | Line 36: | ||
| \] | \] | ||
| - | Note: | + | === Notes on Computational Complexity === |
| * checking satisfiability of propositional formula $F$ is NP-complete | * checking satisfiability of propositional formula $F$ is NP-complete | ||
| * checking validity of propositional formula $F$ is coNP-complete | * checking validity of propositional formula $F$ is coNP-complete | ||
| * checking truth value of arbitrary QBF formula is PSPACE-complete | * checking truth value of arbitrary QBF formula is PSPACE-complete | ||