Reintroducing the Second Player in EPR

Résumé Technique : Reintroducing the Second Player in EPR

1. Problématique et Contexte

L'article s'attaque à la complexité computationnelle des fragments de la logique du premier ordre (FOL), en se concentrant spécifiquement sur la classe Bernays-Schönfinkel (également connue sous le nom de EPR - Effectively Propositional).

• Le constat : La classe EPR complète est NEXPTIME-complète, ce qui la rend extrêmement coûteuse à résoudre. Elle est considérée comme l'analogue logique du problème des formules booléennes quantifiées dépendantes (DQBF).
• Le défi : Bien que des restrictions sur les connecteurs logiques (comme les fragments Horn ou Krom) permettent d'obtenir des problèmes PSPACE-complets au sein de l'EPR, ces fragments ne conservent pas les propriétés structurelles naturelles des Formules Booléennes Quantifiées (QBF). En particulier, ils perdent la sémantique de jeu à deux joueurs (universel vs existentiel) et la capacité naturelle à capturer les niveaux de la hiérarchie polynomiale (PH) par simple restriction.
• L'objectif : Définir un nouveau fragment de l'EPR qui soit PSPACE-complet, qui préserve une sémantique de jeu à deux joueurs similaire aux QBF, et qui reste clos sous les règles de résolution de Robinson.

2. Méthodologie et Définitions Clés

Les auteurs introduisent une observation fondamentale sur la structure des preuves de réfutation dans l'EPR, menant à la définition d'un nouveau fragment appelé QEALM (QBF-like EPR via Alternating Level-ordered Miniscoping).

• Observation 1 (Complexité de Herbrand) : Dans une clause insatisfiable de l'EPR, il est possible d'identifier un terme de base (ground term) qui apparaît systématiquement comme premier argument de tous les littéraux d'une clause, ou qui peut être unifié pour le devenir. Cela suggère que certains arguments agissent comme des « variables extérieures » (outer variables) qui scoppent toute la clause.

• Définition du fragment QEALM : Un problème Bernays-Schönfinkel appartient au fragment QEALM si, dans chaque clause :

  1. Si une variable apparaît dans plusieurs littéraux, sa première occurrence se fait à la même position (indice) dans tous ces littéraux.
  2. Pour tous les littéraux, les arguments précédant cette première occurrence de la variable sont identiques (un segment initial partagé).
     Cette structure impose un ordre strict sur les arguments, permettant de simuler la dépendance entre les quantificateurs.

• Algorithme de décision (Algorithme 1) :
  Les auteurs proposent un algorithme récursif qui alterne entre deux phases, mimant un jeu à deux joueurs :

  • Recherche Universelle : Si toutes les clauses sont « inséparables » (tous les littéraux partagent une variable), l'algorithme itère sur toutes les assignations possibles des variables « extérieures » (outer variables).
  • Recherche Existentielle : Si les clauses sont séparables en « composantes » (sous-clauses inséparables disjointes), l'algorithme choisit une composante par clause (stratégie existentielle) pour vérifier la satisfiabilité.
    Cette alternance correspond directement à la structure des QBF, où les quantificateurs universels et existentiels s'alternent.

3. Contributions Principales

1. Définition du fragment QEALM : C'est le premier fragment de l'EPR qui est naturellement isomorphe aux QBF, tout en restant dans le cadre de la logique du premier ordre.
2. Preuve de Complétude PSPACE : L'article démontre que le fragment QEALM est PSPACE-complet.
   • Inclusion : L'algorithme récursif utilise un espace polynomial (la profondeur de la pile de récursion est bornée par le nombre de variables et la taille des clauses).
   • Dureté : Une réduction polynomiale est établie depuis les QBF vers le fragment QEALM (inspirée de l'outil qbf2epr mais adaptée pour respecter les contraintes du fragment).
3. Hiérarchie Polynomiale et Indices de Fourche (Fork Indices) :
   • Les auteurs définissent les « indices de fourche » (fork indices) pour quantifier le nombre d'alternances existentielles possibles.
   • Ils montrent que le fragment QEALM peut capturer des problèmes complets pour les classes $\Sigma^P_{2k-1}$ et $\Pi^P_{2k}$ de la hiérarchie polynomiale, en fonction du nombre d'indices de fourche.
4. Robustesse Structurelle :
   • Clos sous la Résolution : Contrairement à certaines traductions QBF, le fragment QEALM est clos sous les règles de résolution de Robinson.
   • Intersection avec d'autres fragments : Le fragment reste PSPACE-dur même lorsqu'il est intersecté avec les fragments Krom (clauses à 2 littéraux), Horn (au plus un littéral positif) et Affine. C'est une propriété rare, car l'intersection de QBF avec ces fragments réduit généralement la complexité.

4. Résultats Expérimentaux

Les auteurs ont analysé la bibliothèque TPTP (Thousand Problems for Theorem Proving) version 9.1.0 :

• Sur 936 problèmes Bernays-Schönfinkel, 308 ont été identifiés comme appartenant au fragment QEALM.
• Parmi ceux-ci, on trouve des problèmes de logique modale (traduits en logique du premier ordre) et des formules de comptage binaire.
• L'analyse a permis de classer ces problèmes selon leur niveau dans la hiérarchie polynomiale (de $\Sigma^P_1$ à des niveaux supérieurs selon le nombre d'indices de fourche).
• Ils notent que la traduction standard qbf2epr ne produit pas directement des instances QEALM, mais que celles-ci peuvent être récupérées par élimination de prédicats.

5. Signification et Perspectives

• Théorique : Ce travail comble un fossé entre la logique du premier ordre (EPR) et la logique propositionnelle quantifiée (QBF). Il offre un cadre naturel pour étudier la complexité PSPACE et la hiérarchie polynomiale dans un contexte de logique du premier ordre, sans recourir à des connecteurs propositionnels restreints.
• Pratique : Bien que l'algorithme actuel soit purement théorique (PSPACE), la structure du fragment ouvre la voie à l'adaptation de techniques de résolution avancées issues du domaine des QBF (comme l'apprentissage de clauses ou CEGAR) pour les solveurs de logique du premier ordre.
• Limites et Futur : L'article note que la complexité de preuve par résolution de Robinson reste exponentielle pour ce fragment (phénomène de « dureté sémantique »), ce qui suggère que de nouveaux systèmes de preuve ou des optimisations spécifiques seront nécessaires pour une application pratique efficace.

En résumé, cet article réintroduit la notion de « deuxième joueur » (le joueur existentiel) dans le cadre de l'EPR, permettant de définir un fragment de logique du premier ordre qui partage la richesse structurelle et la complexité des QBF, tout en conservant des propriétés algébriques fortes comme la clôture sous la résolution.