Quantified Boolean Formulae

A quantified boolean formula (QBF) is a boolean formula extended with the quantifiers $\forall$ and $\exists$. An occurrence of a variable modified by a quantifier is bound, and otherwise free. A formula containing only bound occurrences is closed.

A formula $F(p_1,\dots ,p_n)$ is:

• Satisfiable iff $\exists p_1\dots \exists p_{n}F(p_1,\dots ,p_n)$
• Valid iff $\forall p_1\dots \forall p_{n}F(p_1,\dots ,p_n)$