This is an old revision of the document!
QBF and Quantifier Elimination
Quantified Propositional Formula Syntax
We extend the definition of formulas with quantifiers and
where
:
\[\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) \\ & \mid & \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)
\] \[
\forall p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \land subst(\{p \mapsto {\it true}\},F)
\] Note that the expansion can produce exponentially larger formula.
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 quantifier elimination algorithm is an algorithm that takes a formula in a logic and converts it into an equivalent formula without quantifiers.
Note: Formula is valid iff
is true.
Note: Formula is satisfiable iff
is true.
In general QBF formulas can have alternations between and
quantifiers:
\[
\forall p. \exists q. ((p \rightarrow q) \land (q \rightarrow r))
\]
Quantified Propositional Formula Semantics
We can similarly provide semantic function definition for propositional logic.
Notes on Computational Complexity
- checking satisfiability of propositional formula
is NP-complete
- checking validity of propositional formula
is coNP-complete
- checking truth value of arbitrary QBF formula is PSPACE-complete