Thématique abordée

La logique propositionnelle tient une place privilégiée dans de nombreuses applications de déduction automatique. Malgré un pouvoir d'expression a priori limité, elle permet de traiter un grand nombre de problèmes et de concevoir des algorithmes efficaces en pratique. En particulier, le problème SAT, ou test de satisfiabilité, fait l'objet d'importants efforts de recherche, à la fois théorique (problème NP-Complet canonique) et pratique, depuis plus d'une décennie. L'aspect pratique est important dans la mesure où, même si la complexité théorique des problèmes abordés reste bien entendu la même, plusieurs changements de facteurs d'échelle dans la taille des instances traitables ont été observés. Ceci est dû en grande partie à une meilleure connaissance du comportement des algorithmes en pratique, tant sur des exemples concrets, que sur des exemples générés aléatoirement. L'organisation régulière (et de plus en plus rapprochée) de compétitions de démonstrateurs - reflétant l'évolution rapide des performances dans ce domaine - ainsi que la création de sites web (SAT-EX) pour la publication de résultats expérimentaux du domaine y contribuent également.

De nombreux problèmes actuellement traités à l'aide de techniques SAT sont issus d'applications comme la planification, la vérification formelle de microprocesseurs (comme le Bounded Model Checking) ou plus généralement, des problèmes de recherche de point fixe dans l'ensemble des états atteignables d'un automate. Ces applications, très importantes en pratique, impliquent la manipulation de formules de très grande taille (ce qui reflète leur caractère industriel). Nombre de ces problèmes s'expriment en fait à l'origine plus naturellement dans des formalismes plus riches, comme celui des formules booléennes quantifiées (QBF).

Étant donné un ensemble fini $S$ de symboles propositionnels $x_1, \ldots, x_n$ une QBF est une suite $P M$ formée d'un préfixe $P$ et d'une matrice $M$, où $P$ est une suite de quantifications $\forall x$ ou $\exists x$ sur les variables de $S$ et $M$ est une formule propositionnelle classique. Par exemple, étant donnée la formule $g = (\neg x \vee (y \wedge z)) \wedge (x \vee \neg z \vee t)$, la formule $f = \forall x \exists y,z \forall t \; g$ est une QBF.

La validité d'une QBF $f$ se définit alors inductivement comme suit :

• si le préfixe de $f$ est vide, alors $f$ est valide ssi sa matrice l'est (classiquement) ;

• si $f$ s'écrit $\forall x f'$ (où $f'$ est une QBF) alors $f$ est valide ssi quelle que soit la valeur de vérité (vrai ou faux) donnée à $x$ dans $f'$, la formule simplifiée résultante est valide ;

• si $f$ s'écrit $\exists x f'$ (où $f'$ est une QBF) alors $f$ est valide ssi il existe une valeur de vérité (vrai ou faux) pour $x$ dans $f'$ telle que la formule simplifiée résultante soit valide.

Le problème de la validité des formules QBF joue un rôle important en théorie de la complexité. Dans le cas général, i.e. lorsque le nombre d'alternances de quantificateurs n'est pas borné a priori, il constitue le problème PSPACE-complet canonique. Lorsque le nombre d'alternances est fixé au départ, il se décline (selon la nature de la première quantification) en problèmes $\Sigma_k^p$-complets ou $\Pi_k^p$-complets. Pour $k > 1$, les classes $\Sigma_k^p$ et $\Pi_k^p$ se situent au dessus de $NP$ et $coNP$ et en dessous de la classe $PSPACE$. Or, une quantité importante de problèmes d'IA (mais aussi d'autres domaines) ont une complexité théorique dans ces classes. C'est le cas par exemple pour divers problèmes d'inférence (abduction, révision, mise à jour, circonscription, inférence en logique des défauts, etc.) et de planification non déterministe. Lorsque les classes considérées sont fermées par réduction polynomiale, il est théoriquement possible de ramener la résolution de toute instance de tels problèmes à celle de la validité d'une QBF. Cela fait l'objet de recherches, essentiellement à l'étranger, depuis deux ans maintenant. Des résultats intéressants on été obtenus tant d'un point de vue « théorique », par la mise en évidence de réductions depuis un nombre conséquent de problèmes d'IA, que pratique, en montrant que l'approche consistant à coder des problèmes en QBF puis à résoudre ces dernières est tout à fait viable et donne des résultats très compétitifs par rapport à certains algorithmes spécialisés.

Si quelques premiers algorithmes permettant de déterminer directement la validité d'une QBF ont été proposés, ils restent encore assez simples et peu performants. La maturité des démonstrateurs SAT actuels est telle que, dans nombre de cas, il est souvent plus efficace de passer par une réduction en instance SAT que de résoudre directement les QBF considérées. Cependant, une telle réduction induit généralement un accroissement en espace très important des instances produites. Pour certains problèmes industriels, elles ne peuvent alors tout simplement pas tenir en mémoire et, en dépit des énormes progrès réalisés durant ces dernières années sur les démonstrateurs SAT, restent hors de portée des meilleurs démonstrateurs actuels. De plus, ces techniques de transformation ne sont possibles que pour des QBF n'impliquant qu'un nombre réduit d'alternances de quantificateurs. Il est donc important de pouvoir proposer de nouveaux algorithmes pour la résolution directe - et pratique - de QBF.