LARA

QBF and Quantifier Elimination

Quantified Propositional Formula Syntax

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

\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) \\
      & \mid & \forall V. F\ \mid\ \exists V. F
\end{array}
\end{equation*}

Eliminating quantifiers by expansion

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)
\end{equation*}

\begin{equation*}
    \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.

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.

Observation: Formula $F$ is valid iff $\forall 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:

\begin{equation*}
   \forall p. \exists q. ((p \rightarrow q) \land (q \rightarrow r))
\end{equation*}

Quantified Propositional Formula Semantics

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

Summary of Computational Complexity of Problems

  • checking satisfiability of propositional formula $F$ is NP-complete
  • checking validity of propositional formula $F$ is coNP-complete
  • checking truth value of arbitrary QBF formula is PSPACE-complete