Satisfiability problem for quantified Boolean formulas

The satisfiability problem for quantified Boolean formulas is a generalization of the satisfiability problem in propositional logic . It belongs to the complexity theory and is often only called QBF or QSAT for short . This decision problem examines whether a propositional formula that is provided with quantifiers is satisfiable or true .

QBF is the canonical PSPACE - complete problem (i.e. the classic example of a PSPACE-complete problem).

If the satisfiability of Boolean formulas without a free variable is considered, satisfiability is equivalent to truth. The resulting problem of True Quantified Boolean Formula , TQBF for short , is also PSPACE-complete.

Quantified Boolean Formulas

Every propositional formula can be expanded by adding universal and existential quantifiers. The semantics of a formula formed in this way are similar to the semantics of predicate logic formulas .

syntax

The set of quantified Boolean formulas can be inductively defined as follows:

• Each proposition variable is a quantified Boolean formula. occurs freely in the formula . ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle x}$
• Are and quantified Boolean formulas, so are and . A proposition variable from or is free in the formulas, if in or is free. ${\displaystyle \varphi }$ ${\displaystyle \psi }$ ${\displaystyle \neg \varphi ,(\varphi \wedge \psi )}$ ${\displaystyle (\varphi \vee \psi )}$ ${\displaystyle x}$ ${\displaystyle \varphi }$ ${\displaystyle \psi }$ ${\displaystyle x}$ ${\displaystyle \varphi }$ ${\displaystyle \psi }$
• Is a quantified boolean formula and a Boolean variable, so are and quantified boolean formulas. The area of ​​validity of or extends to every free occurrence of in . Every other unbound proposition variable is free in and . ${\displaystyle \varphi }$ ${\displaystyle x}$ ${\displaystyle \forall x\varphi }$ ${\displaystyle \exists x\varphi }$ ${\displaystyle \forall x}$ ${\displaystyle \exists x}$ ${\displaystyle x}$ ${\displaystyle \varphi }$ ${\displaystyle \forall x\varphi }$ ${\displaystyle \exists x\varphi }$

semantics

The semantics of quantified Boolean formulas are closely based on the semantics of predicate logic: The value of a quantified Boolean formula of the form is determined by replacing with, where and arise from each occurrence of being replaced by 0 or 1. Similarly, every occurrence of is replaced by. ${\displaystyle \forall x\varphi }$ ${\displaystyle \varphi }$ ${\displaystyle \varphi _{x=0}\wedge \varphi _{x=1}}$ ${\displaystyle \varphi _{x=0}}$ ${\displaystyle \varphi _{x=1}}$ ${\displaystyle x}$ ${\displaystyle \exists x\varphi }$ ${\displaystyle \varphi _{x=0}\vee \varphi _{x=1}}$

A formula that does not contain any free variables is either true or false.

Prenex normal form

→ Main article : Prenex form

A quantified Boolean formula is in prenex normal form if it is of the form where and are variables of a propositional formula without quantifiers. The expression is called a quantifier block . ${\displaystyle Q_{1}x_{1}Q_{2}x_{2}\ldots Q_{n}x_{n}\varphi }$ ${\displaystyle Q_{1},\ldots ,Q_{n}\in \{\forall ,\exists \}}$ ${\displaystyle x_{1},\ldots ,x_{n}}$ ${\displaystyle \varphi }$ ${\displaystyle Q_{1}x_{1}\ldots Q_{n}x_{n}}$

Since for every quantified Boolean formula there is an equivalent formula in prenex normal form and this can be constructed in polynomial time, this form is often assumed in proofs.

The satisfiability problem

The satisfiability problem for quantified Boolean formulas is to decide whether a given quantified Boolean formula with no free variables is true or false.

From the definition of the semantics for quantified Boolean formulas, a simple recursive algorithm can be derived that solves the satisfiability problem for quantified Boolean formulas in prenex normal form: When entering a formula of the form

${\displaystyle Q_{1}x_{1}Q_{2}x_{2}\cdots Q_{n}x_{n}\varphi }$

for a propositional formula and quantifiers the value of is calculated if no quantifiers are available. Otherwise in the case the value of and in the case the value of is calculated. ${\displaystyle \varphi }$ ${\displaystyle Q_{1},\ldots ,Q_{n}\in \{\forall ,\exists \}}$ ${\displaystyle \varphi }$ ${\displaystyle Q_{1}=\forall }$ ${\displaystyle Q_{2}x_{2}\ldots Q_{n}x_{n}(\varphi _{x_{1}=0}\wedge \varphi _{x_{1}=1})}$ ${\displaystyle Q_{1}=\exists }$ ${\displaystyle Q_{2}x_{2}\ldots Q_{n}x_{n}(\varphi _{x_{1}=0}\vee \varphi _{x_{1}=1})}$

In the case of a quantified Boolean formula with quantifiers, the algorithm therefore requires steps . However, the space required is the square of the length of the formula, so the problem lies in PSPACE. Furthermore it could be shown that the decision problem is PSPACE-difficult. This problem is therefore complete for the PSPACE class. ${\displaystyle n}$ ${\displaystyle O(2^{n})}$

Change of quantifier and polynomial time hierarchy

From the structure of the quantifier block of a quantified Boolean formula in prefix normal form, conclusions can be drawn about complexity-theoretical properties. The classes of the true quantified Boolean formulas in prefix normal form are complete for one level of the polynomial time hierarchy , depending on the number of alternations of universal and existential quantifiers and their order . The following is the notation for a quantifier for any number . ${\displaystyle Q\in \{\forall ,\exists \}}$ ${\displaystyle QX_{i}}$ ${\displaystyle Qx_{i1},Qx_{i2},...,Qx_{ik}}$ ${\displaystyle k}$

Is the class of all true quantified Boolean formulas without free variables of the form ${\displaystyle \Sigma _{k}}$

${\displaystyle \exists X_{1}\forall X_{2}\exists X_{3},\ldots ,Q_{k}X_{k}}$with if is even and otherwise ${\displaystyle Q_{k}=\forall }$ ${\displaystyle k}$ ${\displaystyle Q_{k}=\exists }$

and the class of all true quantified Boolean formulas with no free variables of form ${\displaystyle \Pi _{k}}$

${\displaystyle \forall X_{1}\exists X_{2}\forall X_{3},\ldots ,Q_{k}X_{k}}$with , if is even and otherwise , ${\displaystyle Q_{k}=\exists }$ ${\displaystyle k}$ ${\displaystyle Q_{k}=\forall }$

so applies to all : ${\displaystyle k\geq 0}$

• ${\displaystyle \Sigma _{k}}$is -complete and ${\displaystyle \Sigma _{k}^{\rm {P}}}$
• ${\displaystyle \Pi _{k}}$is -complete. ${\displaystyle \Pi _{k}^{\rm {P}}}$

Individual references and sources

1. ↑ Michael R. Garey, David Stifler Johnson : Computers and intractability. A guide to the theory of NP-completeness . 24th Pr. Freeman Press, New York 2003, ISBN 0-7167-1044-7 .
2. ^ Larry J. Stockmeyer: The polynomial-time hierarchy . In: Theoretical Computer Science , Volume 3, 1976, Issue 1, pp. 1-22, ISSN  0304-3975 .