Formule booléenne quantifiée

En théorie de la complexité, en informatique théorique, en logique mathématique, une formule booléenne quantifiée (ou formule QBF pour quantified binary formula en anglais) est une formule de la logique propositionnelle où les variables propositionnelles sont quantifiées. Par exemple, est une formule booléenne quantifiée et se lit « pour toute valeur booléenne x, il existe une valeur booléenne y et une valeur booléenne z telles que ((x ou z) et y) ». Le problème QBF-SAT (ou QSAT, ou TQBF pour true quantified binary formula, aussi appelé ASAT pour alternating satisfiability problem par Flum et Grohe) est la généralisation du problème SAT aux formules booléennes quantifiées. Le problème QBF-SAT est PSPACE-complet. L'ensemble des formules booléennes quantifiées est défini par induction : Une variable propositionnelle est une formule booléenne quantifiée ; Si est une formule booléenne quantifiée, alors est une formule booléenne quantifiée ; Si et sont deux formules booléennes quantifiées, alors est une formule booléenne quantifiée ; Si est une formule booléenne quantifiée et est une variable propositionnelle, alors et sont des formules booléennes quantifiées. On définit le fait qu'une assignation satisfait une formule booléenne quantifiée par induction. Si une formule booléenne quantifiée est close (toutes les variables sont sous la portée d'un quantificateur), alors la valeur de vérité de la formule ne dépend pas de l'assignation. Si toute assignation satisfait la formule, on dira que cette formule est vraie. Il existe une autre définition équivalente de la sémantique en matière de jeux à deux joueurs. Le joueur 1 attribue des valeurs aux variables propositionnelles quantifiées existentiellement et le joueur 2 attribue des valeurs aux variables propositionnelles quantifiées universellement. Les joueurs donnent les valeurs aux variables dans l'ordre des quantifications. Le joueur 1 gagne si à la fin du jeu la formule propositionnelle est vraie. Une formule QBF est satisfiable si le joueur 1 a une stratégie gagnante.