Erfüllbarkeitsproblem für quantifizierte boolesche Formeln

Das Erfüllbarkeitsproblem für quantifizierte boolesche Formeln ist eine Verallgemeinerung des Erfüllbarkeitsproblems der Aussagenlogik. Es gehört zur Komplexitätstheorie und wird oft nur kurz QBF oder QSAT genannt. Dieses Entscheidungsproblem untersucht, ob eine aussagenlogische Formel, die mit Quantoren versehen ist, erfüllbar oder wahr ist.

QBF ist das kanonische PSPACE-vollständige Problem (also das klassische Beispiel eines PSPACE-vollständigen Problems).

Wird die Erfüllbarkeit von booleschen Formeln ohne freie Variable betrachtet, ist Erfüllbarkeit äquivalent zu Wahrheit. Das so entstehende Problem True Quantified Boolean Formula, kurz TQBF, ist ebenfalls PSPACE-vollständig.