Résumé Technique : Au-delà des Encodages Éager : Une Approche Indépendante de la Théorie pour l'Énumération de Lemmes Théoriques en SMT

1. Énoncé du Problème

Dans la Satisfiabilité Modulo Théories (SMT), le relèvement des techniques de raisonnement booléen nécessite souvent la génération de lemmes théoriques (T-lemmes). Ce sont des clauses T-valides qui éliminent les affectations de vérité qui sont propositionnellement satisfaisantes mais T-incohérentes.

Bien que la résolution SMT standard génère ces lemmes de manière « paresseuse » à la demande durant la recherche, certaines tâches SMT complexes — telles que l'extraction minimale de noyaux insatisfaisables, MaxSMT, et la compilation de T-OBDD ou T-SDD — requièrent le pré-calcul « éager » d'un ensemble complet de T-lemmes dès le départ.

Les encodages SMT « classiques » éager existants sont insuffisants à cette fin car :

1. Ils sont spécifiques à quelques théories simples (par exemple, EUF, DL, LRA).
2. Ils ne respectent pas la combinaison de théories.
3. Ils produisent souvent un nombre excessif de lemmes inutiles.

Actuellement, il manque des méthodes indépendantes de la théorie pour énumérer efficacement des ensembles complets de T-lemmes pour des formules arbitraires, en particulier pour les applications de Compilation de Connaissances (KC) où la surcharge computationnelle est reportée dans une phase hors ligne pour permettre des requêtes en temps polynomial en ligne.

2. Méthodologie

Les auteurs proposent un cadre pour l'énumération de T-lemmes qui est indépendant de la théorie sous-jacente. L'approche s'appuie sur une méthode de base utilisant AllSMT (énumération de toutes les affectations T-satisfaisables) et introduit trois améliorations orthogonales et composites pour renforcer l'évolutivité :

2.1 Base : Énumération Totale AllSMT

La méthode de base (Algorithme 2) effectue une énumération totale, non projetée, AllSMT sur la formule d'entrée $\phi[\alpha]$. Elle trouve itérativement des affectations de vérité totales T-satisfaisables, les bloque, et collecte les T-lemmes appris par le solveur jusqu'à ce que la formule devienne insatisfaisable.

• Limitation : Cette approche repose sur l'énumération d'affectations totales. Comme démontré dans l'Exemple 2, une énumération partielle naïve peut échouer à générer les T-lemmes nécessaires car le solveur peut ne jamais explorer l'affectation totale T-incohérente spécifique qui déclenche un conflit. Cependant, l'énumération de toutes les affectations totales est souvent computationnellement intraitable en raison de l'explosion combinatoire.

2.2 Amélioration 1 : Diviser pour Régner (D&C)

Pour atténuer le coût de l'énumération totale, les auteurs proposent une stratégie Diviser pour Régner (Algorithme 3) :

1. Effectuer une énumération AllSMT partielle pour décomposer l'espace de recherche booléen en un ensemble d'affectations partielles disjointes et T-satisfaisables ($M_{\alpha}^p$).
2. Pour chaque affectation partielle $\mu \in M_{\alpha}^p$, effectuer une énumération AllSMT totale sur la formule restreinte $\phi \land \mu$.
3. Les énumérations totales sont exécutées en parallèle.

• Raison d'être : Cela transforme une unique énumération totale grande et intraitable en une étape de décomposition moins coûteuse plus de nombreuses énumérations totales plus petites et gérables.

2.3 Amélioration 2 : Énumération Projetée

Les auteurs observent que l'incohérence T est déterminée exclusivement par l'affectation aux atomes de théorie ($\alpha_T$), et non aux atomes booléens ($\alpha_B$).

• Méthode : Effectuer une énumération AllSMT projetée uniquement sur $\alpha_T$ (Algorithme 4).
• Fondement Théorique : Le Théorème 1 prouve que projeter l'énumération sur les atomes T produit un ensemble complet de T-lemmes.
• Avantage : Cela réduit drastiquement la dimension de recherche. Une seule affectation T-satisfaisable sur $\alpha_T$ représente jusqu'à $2^k$ affectations totales sur l'ensemble complet des atomes (où $k$ est le nombre d'atomes booléens), réduisant significativement l'utilisation de la mémoire et la taille des clauses de blocage.

2.4 Amélioration 3 : Partitionnement Piloté par la Théorie

Si l'ensemble des atomes dans $\phi$ peut être partitionné en ensembles disjoints ($\alpha_1, \dots, \alpha_n$) tels qu'aucun atome dans un ensemble ne partage de variables ou de symboles non interprétés avec des atomes dans un autre, le problème peut être décomposé davantage (Algorithme 5).

• Méthode : Basé sur la Propriété 1 et le Théorème 2, les T-lemmes peuvent être énumérés indépendamment pour chaque partition. L'algorithme partitionne itérativement les atomes, énumère les lemmes pour chaque partition projetée sur les atomes de cette partition, et accumule les résultats.
• Avantage : Cela permet de décomposer une unique énumération totale en $n$ énumérations projetées indépendantes, offrant des accélérations potentielles exponentielles pour les problèmes avec des composants disjoints.

3. Contributions Clés

1. Cadre Indépendant de la Théorie : La première présentation explicite de méthodes pour énumérer des ensembles complets de T-lemmes pour des théories arbitraires, dépassant les encodages éager spécifiques à une théorie.
2. Techniques d'Évolutivité : L'introduction de trois techniques orthogonales :
   • Diviser pour Régner : Parallélise la recherche en décomposant l'espace booléen.
   • Énumération Projetée : Réduit la dimensionalité de recherche en se concentrant sur les atomes T.
   • Partitionnement : Exploite la disjonction structurelle dans la formule pour résoudre des sous-problèmes indépendamment.
3. Garanties Théoriques : Des preuves formelles (Théorèmes 1 et 2) démontrant que ces optimisations préservent la complétude de l'ensemble des T-lemmes nécessaire pour éliminer toutes les affectations T-incohérentes.
4. Intégration avec la Compilation de Connaissances : Ce travail sert de technique habilitante pour relever les méthodes de Compilation de Connaissances (spécifiquement les Diagrammes de Décision comme les OBDD et les SDD) au niveau SMT, adressant le goulot d'étranglement précédent de l'énumération des T-lemmes.

4. Résultats Expérimentaux

Les techniques ont été évaluées sur deux ensembles de benchmarks :

• Instances SMT(LRA) synthétiques : 450 problèmes générés aléatoirement issus de [16].
• Instances de Planification Temporelle : 90 encodages SMT de problèmes de planification du domaine « Peintre ».

Métriques de Performance :

• Efficacité Temporelle :
  • Sur les benchmarks synthétiques, D&C a amélioré les performances jusqu'à 2 ordres de grandeur par rapport à la base, résolvant 17 problèmes de plus dans le délai imparti.
  • L'ajout de la Projection a encore amélioré les résultats, résolvant 30 problèmes de plus que D&C seul et réduisant drastiquement le temps pour les instances précédemment résolues.
  • Le Partitionnement n'a montré aucune amélioration sur les données synthétiques (car peu de problèmes avaient des partitions disjointes) mais s'est révélé hautement efficace sur les problèmes de planification.
  • Sur les problèmes de planification, le Partitionnement a été le facteur dominant, permettant la résolution de problèmes avec un horizon de 5 qui étaient auparavant intraitables, atteignant des accélérations de plusieurs ordres de grandeur.
• Nombre de Lemmes :
  • D&C a tendance à produire légèrement plus de lemmes en raison de la redondance parallèle.
  • La Projection et le Partitionnement ont généralement réduit le nombre de lemmes énumérés en atténuant l'exploration redondante et en générant des lemmes plus forts et plus petits.
• Taille des Lemmes :
  • Le Partitionnement sur les problèmes de planification a résulté en des T-lemmes significativement plus petits (moins de littéraux), probablement dû à l'élagage précoce des branches T-incohérentes impliquant uniquement des partitions spécifiques.

5. Signification et Revendications

L'article revendique que ces techniques améliorent drastiquement l'efficacité et l'évolutivité de l'énumération des T-lemmes par rapport à l'approche AllSMT de base.

• Rôle Habilitant : La signification principale est de permettre l'application pratique de la Compilation de Connaissances au SMT. Les auteurs notent que dans leur travail précédent [16], l'énumération des T-lemmes était le « principal goulot d'étranglement » pour compiler les Diagrammes de Décision. En résolvant ce goulot d'étranglement, les méthodes proposées ouvrent la voie à la mise à l'échelle de ces techniques de compilation vers des instances complexes et réelles.
• Modestie : Les auteurs notent avec prudence que les améliorations dépendent du contexte. Par exemple, la projection n'a pas aidé pour les problèmes de planification car les affectations d'atomes T étaient des conséquences déterministes des affectations booléennes dans ces encodages spécifiques. De même, le partitionnement n'a apporté des bénéfices que lorsque la structure du problème permettait naturellement des partitions disjointes.

En résumé, l'article fournit une boîte à outils robuste et indépendante de la théorie pour l'énumération éager des T-lemmes, transformant une étape auparavant intraitable en un processus évolutif, facilitant ainsi des applications SMT avancées comme MaxSMT et la Compilation de Connaissances.