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, ${\displaystyle \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, aussi appelé ASAT pour alternating satisfiability problem par Flum et Grohe^[1]) est la généralisation du problème SAT aux formules booléennes quantifiées. Le problème QBF-SAT est PSPACE-complet^[2].

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 ${\displaystyle \phi }$ est une formule booléenne quantifiée, alors ${\displaystyle \lnot \phi }$ est une formule booléenne quantifiée ;
• Si ${\displaystyle \phi }$ et ${\displaystyle \psi }$ sont deux formules booléennes quantifiées, alors ${\displaystyle \phi \land \psi }$ est une formule booléenne quantifiée ;
• Si ${\displaystyle \phi }$ est une formule booléenne quantifiée et ${\displaystyle p}$ est une variable propositionnelle, alors ${\displaystyle \forall p\phi }$ et ${\displaystyle \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.

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.

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 \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 ${\displaystyle Q_{i}}$ est soit un quantificateur existentiel ${\displaystyle \exists }$ soit un quantificateur universel ${\displaystyle \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 \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ù ${\displaystyle Q_{n}=\exists }$ si ${\displaystyle n}$ est impair et ${\displaystyle Q_{n}=\forall }$ si ${\displaystyle n}$ est pair et ou ${\displaystyle \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 ${\displaystyle \nu }$ et une formule booléenne quantifiée ${\displaystyle \phi }$ que l'on suppose prénexe.

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

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

PSPACE-dur

Pour montrer que QBF-SAT est PSPACE-dur^[2], 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^[2].

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

Hiérarchie polynomiale

Si on borne le nombre d'alternations de quantificateurs dans la formule donnée en entrée du problème QBF-SAT, on obtient des problèmes complets à différents niveaux de la hiérarchie polynomiale :

• Le problème où la formule d'entrée est de la forme ${\displaystyle \displaystyle \exists {\vec {x}}_{1}\phi }$ où ${\displaystyle \displaystyle {\vec {x}}_{1}}$est un ensemble de variables propositionnelles et ${\displaystyle \phi }$ est une formule propositionnelle, alors il s'agit du problème SAT et il est NP-complet ;
• Le problème où la formule d'entrée est de la forme ${\displaystyle \displaystyle \forall {\vec {x}}_{1}\phi }$ où ${\displaystyle \displaystyle {\vec {x}}_{1}}$est un ensemble de variables propositionnelles et ${\displaystyle \phi }$ est une formule propositionnelle, alors il s'agit du problème de la validité d'une formule de la logique propositionnelle et il est coNP-complet ;
• Le problème où la formule d'entrée est de la forme ${\displaystyle \displaystyle \exists {\vec {x}}_{1}\forall {\vec {x}}_{2}\phi }$ où ${\displaystyle \displaystyle {\vec {x}}_{1}}$et ${\displaystyle \displaystyle {\vec {x}}_{2}}$ sont deux ensembles de variables propositionnelles et ${\displaystyle \phi }$ est une formule propositionnelle, alors le problème est ${\displaystyle \Sigma _{2}^{P}}$-complet ;
• Le problème où la formule d'entrée est de la forme ${\displaystyle \displaystyle \forall {\vec {x}}_{1}\exists {\vec {x}}_{2}\phi }$ où ${\displaystyle \displaystyle {\vec {x}}_{1}}$et ${\displaystyle \displaystyle {\vec {x}}_{2}}$ sont deux ensembles de variables propositionnelles et ${\displaystyle \phi }$ est une formule propositionnelle, alors le problème est ${\displaystyle \Pi _{2}^{P}}$-complet ;
• etc.

Système de preuve

Plusieurs systèmes de preuve ont vu le jour et sont fondés sur la résolution : Q-Resolution calculus QRES, Long distance Q-Resolution, QU-Resolution et autres variantes. Nous présentons ici uniquement le système QRES. On démontre avec une formule sous forme prénexe où la formule propositionnelle est en forme normale conjonctive. Les règles sont :

Règles	Explications
${\displaystyle {\frac {}{C}}}$	si C est une clause qui ne contient pas x et non x
${\displaystyle {\frac {C\cup \{\ell \}}{C}}}$	si ${\displaystyle \ell }$ est un littéral tel que la variable propositionnelle associée est quantifiée universellement et ${\displaystyle {C\cup \{\ell \}}}$est une clause qui ne contient pas x et non x et tous les littéraux de C quantifiée existentiellement précède la quantification de ${\displaystyle \ell }$
${\displaystyle {\frac {C_{1}\cup \{p\}~~~~~~~~~C_{2}\cup \{\neg p\}}{C_{1}\cup C_{2}}}}$	si p est quantifiée existentiellement, non p n'apparaît pas dans C1, p n'apparaît pas dans C2, et C1 U C2 ne contient pas x et non x. C'est la règle qui ressemble à la règle de résolution pour la logique propositionnelle classique.

Une formule est insatisfiable si, et seulement il existe une preuve de la clause vide.

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]}.

Implémentations

Contrairement aux solveurs SAT (pour la logique propositionnelle), l'avancée des solveurs QBF est plus récente. Mangassarian écrit^[3] 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 y a une compétition annuelle QBFEVAL (47 systèmes soumis en 2017^[4]).

Formats d'entrée

Certains solveurs prennent un fichier au format QDIMACS^[5] qui est une variante du format DIMACS pour SAT. Il existe le format QCIR (pour Quantified CIRcuit)^[6].

Techniques algorithmiques

Il existe plusieurs techniques algorithmiques pour résoudre QBF-SAT^[7] :

• l'apprentissage de clauses. C'est une technique également utilisé dans l'algorithme DPLL pour SAT ;
• Counterexample guided abstraction refinement (CEGAR)^[8] ;
• Expansion. L'expansion consiste à recopier la formule propositionnelle en instanciant les variables universelles ;
• Calcul de fonctions de Skolem^[9]
• Algorithme FTP en la treewidth du graphe de contraintes (c'est-à-dire pour la relation, "apparaître dans la même clause") et le nombre d'alternation de quantificateur utilisant de la programmation dynamique^{[réf. nécessaire]}. L'algorithme est en temps ${\displaystyle O(2^{2^{2^{.}..^{2^{w+1}}}}\times |\phi |)}$où w est la treewidth, le nombre de 2 dans la tour d'exponentielle est le nombre d'alternation.

Applications pratiques

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

Variantes

Dependency quantified binary formulas

Une extension intéressante est dependency quantified binary formulas (DQBF)^[11]. Dans QBF, une variable quantifiée existentiellement dépend des variables précédentes. Par exemple, dans la formule ${\displaystyle \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 ${\displaystyle y_{1}}$et ${\displaystyle y_{2}}$dépendent toutes les deux des variables ${\displaystyle x_{1}}$, ${\displaystyle x_{2}}$et ${\displaystyle x_{3}}$. En DQBF, on peut spécifier des dépendances plus fines comme ${\displaystyle y_{1}}$ ne dépend que de ${\displaystyle x_{1}}$ et ${\displaystyle x_{2}}$ et ${\displaystyle y_{2}}$ ne dépend que de ${\displaystyle x_{1}}$ et ${\displaystyle x_{3}}$. On écrit une formule comme ${\displaystyle \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.

Une autre formulation de DQBF existe en termes de jeu à trois joueurs^[12] : N, B1 et B2. Il y a deux équipes : l'équipe noire (N) et l'équipe blanche (B1 et B2). L'entrée est une forme normale conjonctive (FNC) sur des variables propositionnelles dans X1 U Y1 U X2 U Y2. L'objectif est de décider le joueur blanc a une stratégie gagnante au jeu suivant. Le joueur noir choisit une assignation des variables dans X1 U X2. Le joueur B1 choisit alors une assignation de Y1, puis le B2 choisit une assignation de Y2. Le joueur i blanc ne voit que les assignations de Xi et Yi. L'équipe blanche (noire) gagne si la FNC est vraie (fausse).

Fragments dans P

Le problème de satisfiabilité des fragments de QBF suivants se décide en temps polynomial :

• lorsque la formule propositionnelle est une conjonction de clauses de Horn^[13] ;
• lorsque la formule propositionnelle est un 2-SAT, c'est-à-dire une conjonction de clauses avec au plus 2 littéraux^[14].

Notes et références

1. J. Flum et M. Grohe, Parameterized Complexity Theory (Texts in Theoretical Computer Science. An EATCS Series), Springer-Verlag New York, Inc., 1^er mars 2006 (ISBN 3540299521, lire en ligne), p. 71, section 4.1
2. (en) Sipser, Michael (1997), « Section 8.3: PSPACE-completeness », Introduction to the Theory of Computation, PWS Publishing, pp. 283–294, (ISBN 0-534-94728-X).
3. (en) H. Mangassarian, A. Veneris et M. Benedetti, « Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test », IEEE Transactions on Computers, vol. 59,‎ 1^er juillet 2010, p. 981–994 (ISSN 0018-9340, DOI 10.1109/TC.2010.74, lire en ligne, consulté le 11 juillet 2016).
4. « QBFEVAL'17 »
5. (en) « QDIMACS ».
6. (en) « Benchmark en QCIR » [PDF].
7. (en) « Tutoriel IJCAI 2016 » [PDF].
8. (en) Mikoláš Janota et Joao Marques-Silva, « Abstraction-based Algorithm for 2QBF », Proceedings of the 14th International Conference on Theory and Application of Satisfiability Testing, Springer-Verlag, sAT'11,‎ 1^er janvier 2011, p. 230–244 (ISBN 9783642215803, lire en ligne, consulté le 11 juillet 2016).
9. (en) Valeriy Balabanov et Jie-Hong R. Jiang, « Resolution Proofs and Skolem Functions in QBF Evaluation and Applications », Proceedings of the 23rd International Conference on Computer Aided Verification, Springer-Verlag, cAV'11,‎ 1^er janvier 2011, p. 149–164 (ISBN 9783642221095, lire en ligne, consulté le 11 juillet 2016).
10. (en) Tamir Heyman, Dan Smith, Yogesh Mahajan et Lance Leong, Dominant Controllability Check Using QBF-Solver and Netlist Optimizer, Springer International Publishing, coll. « Lecture Notes in Computer Science », 14 juillet 2014 (ISBN 9783319092836 et 9783319092843, lire en ligne), p. 227–242
11. (en) « Dependency quantified binary formulas » [PDF].
12. (en) Robert Aubrey Hearn, Games, puzzles, and computation (thèse de doctorat), Massachusetts Institute of Technology, 1^er janvier 2006 (lire en ligne).
13. H. K. Buning, M. Karpinski et A. Flogel, « Resolution for Quantified Boolean Formulas », Information and Computation, vol. 117,‎ 15 février 1995, p. 12–18 (DOI 10.1006/inco.1995.1025, lire en ligne, consulté le 11 juillet 2016).
14. (en) Bengt Aspvall, Michael F. Plass et Robert Endre Tarjan, « A linear-time algorithm for testing the truth of certain quantified boolean formulas », Information Processing Letters, vol. 8,‎ 15 mars 1979, p. 121–123 (DOI 10.1016/0020-0190(79)90002-4, lire en ligne, consulté le 11 juillet 2016).

Liens externes

• (en) « Un solveur QBF »

• Portail de l'informatique théorique
• Portail de la logique