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, $\forall x\ \exists y\ \exists z\ ((x\lor z)\land y)$ 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) est la généralisation du problème SAT aux formules booléennes quantifiées. Le problème QBF-SAT est PSPACE-complet.

Terminologie

Syntaxe

L'ensemble des formules booléennes quantifiées est défini par induction :

• Une variable propositionnelle est une formule booléenne quantifiée ;
• Si $\phi$ est une formule booléenne quantifiée, alors $\lnot \phi$ est une formule booléenne quantifiée ;
• Si $\phi$ et $\psi$ sont deux formules booléennes quantifiées, alors $\phi \land \psi$ est une formule booléenne quantifiée ;
• Si $\phi$ est une formule booléenne quantifiée et $p$ est une variable propositionnelle, alors $\forall p\phi$ et $\exists p\phi$ sont des formules booléennes quantifiées.

Sémantique

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.

Forme normale prénexe

Une formule booléenne quantifiée est en forme normale prénexe si tous les quantificateurs sont regroupés à l'avant de la formule, c'est à dire de la forme $\displaystyle Q_{1}x_{1}Q_{2}x_{2}\cdots Q_{n}x_{n}\phi (x_{1},x_{2},x_{3},\dots ,x_{n})$ où chaque $Q_{i}$ est soit un quantificateur existentiel $\exists$ soit un quantificateur universel $\forall$. Toute formule booléenne quantifiée est équivalente à une formule booléenne quantifiée en forme normale prénexe. On peut même transformer, quitte à rajouter des variables inutiles, toute formule prénexe en formule équivalente de la forme $\displaystyle \exists x_{1}\forall x_{2}\exists x_{3}\cdots Q_{n}x_{n}\phi (x_{1},x_{2},x_{3},\dots ,x_{n})$

où $Q_{n}=\exists$ si $n$ est impair et $Q_{n}=\forall$ si $n$ est pair et ou $\phi (x_{1},x_{2},x_{3},\dots ,x_{n})$ est une formule de la logique propositionnelle.

Le problème QBF-SAT

Le problème QBF-SAT est le problème de décision, qui étant donné une formule booléenne quantifiée close, détermine si cette formule est vraie.

Dans PSPACE

On donne un algorithme en espace polynomial qui prend en entrée une assignation $\nu$ et une formule booléenne quantifiée $\phi$ que l'on suppose prénexe.

  qbf-sat($\nu$, $\phi$)
    si $\phi$ est propositionnelle
           retourner oui si $\nu \models \phi$ ; non sinon.
    sinon si $\phi$ est de la forme $\exists p\psi$
           retourner qbf-sat($\nu [p:=0]$, $\psi$) ou qbf-sat($\nu [p:=1]$, $\psi$)
    sinon si $\phi$ est de la forme $\forall p\psi$
           retourner qbf-sat($\nu [p:=0]$, $\psi$) et qbf-sat($\nu [p:=1]$, $\psi$)

où $\nu [p:=0]$ est l'assignation $\nu$ sauf pour $p$ qui est fausse et $\nu [p:=1]$ est l'assignation $\nu$ sauf pour $p$ qui est vraie.

PSPACE-dur

Pour montrer que QBF-SAT est PSPACE-dur, on considère un problème A dans PSPACE et on donne une réduction polynomiale de A dans QBF-SAT. A toute instance x de A, on construit une formule booléenne quantifiée close tr(x) telle que x est une instance positive de A ssi tr(x) est vraie. L'idée est que tr(x) code l'existence d'une exécution acceptante d'une machine de Turing pour A sur l'entrée x. Pour que tr(x) reste de taille polynomiale, on utilise le paradigme diviser pour régner.

La réduction précédente fonctionne si A est dans NPSPACE. Ainsi, on a donné une preuve alternative de PSPACE = NPSPACE (cas particulier du théorème de Savitch).

Application théorique ː démontrer la PSPACE-dureté

Comme le problème QBF-SAT est PSPACE-dur, il permet, par réduction polynomiale, de montrer que d'autres problèmes sont PSPACE-dur. Voici une liste de problèmes de décision PSPACE-complets dont la PSPACE-dureté peut être démontré par réduction polynomiale ː

• Le problème de satisfiabilité de la logique modale K ^{[réf. nécessaire]}
• Le jeu de géographie généralisé^{[réf. nécessaire]}

Algorithmes

Contrairement aux solveurs SAT, l'avancée des solveurs QBF est plus récente. Mangassarian écrit en 2010 ː

Admittedly, the theory and results of this paper emphasize the need for further research in QBF solvers [. . . ] Since the first complete QBF solver was presented decades after the first complete engine to solve SAT, research in this field remains at its infancy.

(Apparemment, la théorie et les résultats de ce papier montre le besoin de continuer les recherches sur les solveurs QBF [...] Comme le premier solveur QBF complet a été présenté des dizaines d'années après le premier solveur SAT complet, la recherche dans ce domaine est encore à ses balbutiements)

Il existe plusieurs techniques algorithmiques pour résoudre QBF-SAT ː

• l'apprentissage de clauses. C'est une technique également utilisé dans l'algorithme DPLL pour SAT ;
• Counterexample guided abstraction refinement (CEGAR)
• Expansion. L'expansion consiste à recopier la formule propositionnelle en instanciant les variables universelles.
• Calcul de fonctions de Skolem.

Applications pratiques

Il existe quelques applications potentielles. On peut utiliser QBF pour vérifier des circuits.

Variantes

Dependency quantified binary formulas

Une extension intéressante est dependency quantified binary formulas (DQBF). Dans QBF, une variable quantifiée existentiellement dépend des variables précédentes. Par exemple, dans la formule $\displaystyle \forall x_{1}\forall x_{2}\forall x_{3}\exists y_{1}\exists y_{2}\phi (x_{1},x_{2},y_{1})\land \psi (x_{1},x_{3},y_{2})$, les variables propositionnelles $y_{1}$et $y_{2}$dépendent toutes les deux des variables $x_{1}$, $x_{2}$et $x_{3}$. En DQBF, on peut spécifier des dépendences plus fines comme $y_{1}$ ne dépend que de $x_{1}$ et $x_{2}$ et $y_{2}$ ne dépend que de $x_{1}$ et $x_{3}$. On écrit une formule comme $\displaystyle \forall x_{1}\forall x_{2}\forall x_{3}\exists y_{1}(x_{1},x_{2})\exists y_{2}(x_{1},x_{3})\phi (x_{1},x_{2},y_{1})\land \psi (x_{1},x_{3},y_{2})$. Le problème de satisfiabilité d'une formule de DQBF est NEXPTIME-complet.

Liens externes

• « Un solveur QBF »