💻 computer science

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses

Cet article présente deux nouveaux solveurs, tabularAllSAT et tabularAllSMT, qui utilisent l'apprentissage de clauses guidé par les conflits avec retour chronologique et un algorithme agressif de réduction des implicants pour énumérer efficacement des affectations satisfaisantes disjointes pour des problèmes SAT et SMT sans recourir à des clauses de blocage.

Auteurs originaux : Giuseppe Spallitta, Roberto Sebastiani, Armin Biere

Publié 2026-05-11

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Giuseppe Spallitta, Roberto Sebastiani, Armin Biere

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous soyez un détective cherchant à trouver chaque combinaison possible d'indices qui résout un mystère massif et complexe. Dans le monde de l'informatique, ce « mystère » est une formule logique, et les « indices » sont des paramètres vrai/faux pour diverses variables. Cette tâche s'appelle AllSAT (trouver toutes les solutions) ou AllSMT (trouver toutes les solutions lorsque les indices impliquent des mathématiques ou d'autres règles complexes).

Le document que vous avez fourni présente deux nouveaux outils, TabularAllSAT et TabularAllSMT, conçus pour résoudre ce travail de détective beaucoup plus rapidement et efficacement que les méthodes précédentes. Voici comment ils fonctionnent, expliqués par de simples analogies.

Le Problème : Le Goulot d'Étranglement du « Blocage »

Traditionnellement, lorsqu'un ordinateur trouve une solution à une énigme, il doit s'assurer de ne pas retrouver exactement la même solution.

L'Ancienne Méthode (Clauses de Blocage) : Imaginez que le détective trouve une solution, la note, puis place un gigantesque panneau « INTERDICTION D'ENTRER » (une clause de blocage) sur ce chemin spécifique. Il revient ensuite au début et réessaie.
- Le Défaut : S'il existe des millions de solutions, le détective finit par recouvrir toute la carte de millions de panneaux « INTERDICTION D'ENTRER ». Finalement, la carte devient si encombrée de panneaux que le détective se perd, ralentit et manque d'espace pour tous les écrire. C'est l'« explosion de la mémoire » mentionnée dans le document.

La Solution : La Marche « Chronologique »

Les auteurs proposent une manière plus intelligente de parcourir l'énigme sans avoir besoin de ces panneaux « INTERDICTION D'ENTRER ».

La Nouvelle Méthode (Retour Arrière Chronologique) : Au lieu de placer des panneaux, le détective parcourt l'énigme systématiquement. Lorsqu'il atteint une impasse ou trouve une solution, il fait simplement un pas en arrière jusqu'à la dernière décision qu'il a prise, inverse cette décision (comme passer un interrupteur de « Marche » à « Arrêt »), et continue d'avancer.
- L'Avantage : Parce qu'il avance dans une ligne stricte et ordonnée (comme lire un livre page par page), il ne visite naturellement jamais le même endroit deux fois. Aucun panneau n'est nécessaire, la carte reste donc propre, et le détective n'est jamais submergé par l'encombrement.

L'Astuce du « Rétrécissement » : Trouver le Cœur

Une fois que le détective trouve une solution complète (où chaque indice a une valeur), il réalise qu'il n'a pas besoin de tous les indices pour prouver que la solution fonctionne. Peut-être que seulement 3 indices sur 10 étaient essentiels ; les 7 autres pourraient être n'importe quoi.

L'Ancien Rétrécissement : Les méthodes précédentes étaient prudentes. Elles ne supprimaient des indices que si elles étaient absolument sûres que c'était sans danger, laissant souvent du « poids mort » supplémentaire dans la solution.
Le Nouveau Rétrécissement « Agressif » : Les auteurs ont créé un nouvel algorithme qui agit comme un éditeur impitoyable. Il examine la solution et demande : « Puis-je supprimer cet indice sans briser la logique ? » Si oui, il le coupe immédiatement.
- Le Résultat : Au lieu de renvoyer une longue et désordonnée liste de 10 indices, l'ordinateur renvoie une petite liste compacte contenant uniquement les 3 indices essentiels. Cela réduit considérablement la quantité de données que l'ordinateur doit traiter et stocker.

Gérer les Variables « Importantes » vs « Peu Importantes » (Projection)

Parfois, le détective ne se soucie que d'indices spécifiques (par exemple : « Qui a volé le biscuit ? ») et ne se soucie pas d'autres (par exemple : « De quelle couleur était le ciel ? »).

Le Défi : Si l'ordinateur résout toute l'énigme, y compris la couleur du ciel, il perd du temps.
La Correction : Les nouveaux outils sont entraînés à prioriser les indices « Importants ». Ils résolvent l'énigme mais ignorent complètement les indices « Peu Importants ». C'est comme résoudre un labyrinthe mais ne se soucier que du chemin vers la sortie, pas des décorations sur les murs. Cela rend la recherche beaucoup plus rapide.

Gérer les Mathématiques et les Règles Complexes (SMT)

Jusqu'ici, nous avons parlé de simples interrupteurs Vrai/Faux. Mais les problèmes du monde réel impliquent souvent des mathématiques (comme « x + y > 10 »).

L'Extension : Les auteurs ont amélioré leur détective pour gérer ces règles mathématiques. Ils ont ajouté un « Consultant en Mathématiques » (un solveur de théorie) à l'équipe.
- Lorsque le détective fait une hypothèse, il demande au Consultant en Mathématiques : « Est-ce que cela a du sens avec les règles mathématiques ? »
- Si les mathématiques disent « Non », le détective recule immédiatement et essaie un chemin différent, plutôt que de perdre du temps à emprunter un chemin mathématiquement impossible.

La Conclusion

Le document affirme qu'en combinant un style de marche strict et ordonné (Retour Arrière Chronologique) avec un style d'édition impitoyable (Rétrécissement Agressif), leurs nouveaux outils (TabularAllSAT et TabularAllSMT) sont significativement plus rapides et utilisent moins de mémoire que les meilleurs outils actuels.

Ils ne s'encombrent pas de panneaux « Interdiction d'Entrer ».
Ils renvoient des réponses plus petites et plus claires en éliminant les détails inutiles.
Ils gèrent les mathématiques complexes sans se bloquer.

Les auteurs ont testé ces outils contre les meilleurs concurrents et ont constaté que leur approche résolvait plus de problèmes, plus rapidement, en particulier lorsque les problèmes étaient énormes ou impliquaient des mathématiques complexes.

Résumé Technique : Énumération Projetée Disjointe pour SAT et SMT sans Clauses de Blocage

Énoncé du Problème

L'article aborde les défis computationnels inhérents à la Satisfiabilité de Toutes les Solutions (AllSAT) et à son extension, la Satisfiabilité Modulo Théories de Toutes les Solutions (AllSMT). L'objectif est d'énumérer toutes les affectations satisfaisantes d'une formule. Alors que la résolution SAT traditionnelle se termine dès qu'une seule solution est trouvée, l'énumération nécessite d'explorer l'ensemble de l'espace de recherche.

Deux difficultés principales sont identifiées :

Espace de Recherche Exponentiel : Pour une formule avec $n$ variables, il existe $2^n$ affectations totales possibles. L'énumération explicite est irréalisable pour de grandes valeurs de $n$ . L'article préconise l'utilisation d'affectations partielles (implicants) pour représenter des ensembles d'affectations totales, comprimant ainsi l'espace des solutions.
Clauses de Blocage et Mémoire : Les solveurs AllSAT traditionnels basés sur l'Apprentissage de Clauses par Conflit (CDCL) et le Retour Arrière Non Chronologique (NCB) reposent sur l'ajout de clauses de blocage pour empêcher la redécouverte du même modèle. À mesure que le nombre de modèles augmente, le nombre de clauses de blocage peut devenir exponentiel, entraînant des explosions mémoire et une dégradation des performances de la propagation unitaire.
Projection : Dans de nombreuses applications (par exemple, la conversion de formules non-CNF via la transformation de Tseitin), il est nécessaire d'énumérer les solutions uniquement pour un sous-ensemble de variables « importantes » ( $V_r$ ), en ignorant les variables auxiliaires « non pertinentes » ( $V_i$ ).

L'article se concentre sur l'énumération disjointe, où les affectations répétées sont strictement interdites, une exigence pour des applications telles que l'Intégration de Modèles Pondérés (WMI) et l'inférence probabiliste.

Méthodologie

Les auteurs proposent deux nouveaux solveurs : TabularAllSAT (pour la logique propositionnelle) et TabularAllSMT (pour SMT). Tous deux intègrent le CDCL avec un Retour Arrière Chronologique (CB) pour éliminer le besoin de clauses de blocage tout en maintenant la disjointure.

1. Algorithme de Recherche Principal (CDCL + CB)

La boucle de recherche combine les forces du CDCL (échapper aux régions insatisfaisables via l'analyse de conflits) et du CB (exploration systématique sans clauses de blocage redondantes).

Gestion des Conflits : Lorsqu'un conflit est détecté, le solveur effectue une analyse de conflit standard pour dériver une clause de conflit. Cependant, au lieu de revenir en arrière de manière non chronologique au niveau de la clause de conflit (comme dans le CDCL standard), le solveur remonter chronologiquement jusqu'à la dernière littérale de décision assignée et inverse sa valeur.
Blocage Implicite : Pour assurer la disjointure sans stocker de clauses de blocage explicites, le solveur utilise des clauses de raison de retour virtuelles. Lorsqu'un modèle est trouvé et qu'une littérale de décision est inversée, la raison de l'inversion est enregistrée sous la forme de Backtrue. Cela définit implicitement une clause de blocage composée de la négation de toutes les littérales de décision jusqu'à ce point.
Terminaison : La recherche se termine lorsque le solveur revient au niveau de décision 0, garantissant que l'ensemble de l'espace a été balayé systématiquement sans répétition.

2. Réduction Chronologique des Implicants

Un composant critique est la réduction des affectations totales en affectations partielles compactes (implicants). L'article introduit deux algorithmes :

Réduction Conservatrice (Référence) : Basée sur la surveillance de 2 littéraux, cet algorithme vérifie si une littérale est nécessaire pour que l'affectation partielle courante satisfasse la formule. Elle respecte l'ordre de décision et les drapeaux Backtrue pour garantir la disjointure.
Réduction Agressive (Nouvelle) : Cet algorithme simule un ordre de décision optimal. Il identifie les littérales « nécessaires » (celles requises pour satisfaire des clauses spécifiques) et les littérales « inutiles ». Il permet la suppression des littérales inutiles indépendamment de leur niveau de décision, à condition qu'elles ne soient pas marquées Backtrue ou impliquées dans une analyse de conflit. Cela est réalisé en :
1. Comptant combien de littérales dans chaque clause sont actuellement dans la trace.
2. Supprimant itérativement les littérales qui ne sont pas le seul satisfacteur d'aucune clause.
3. Reconstruisant la trace avec uniquement les littérales nécessaires, reportant efficacement l'assignation des variables inutiles à la fin de la boucle de recherche.

3. Extensions à la Projection et SMT

Énumération Projetée : L'algorithme est adapté pour gérer un sous-ensemble de variables pertinentes ( $V_r$ ). L'heuristique de décision privilégie $V_r$ par rapport aux variables non pertinentes ( $V_i$ ). Lors de la réduction d'implicants, les littérales correspondant à $V_i$ sont automatiquement écartées, garantissant que la sortie ne contient que des affectations pour $V_r$ .
Intégration AllSMT : Le cadre intègre un solveur de théorie (MathSAT5). La boucle de recherche inclut une vérification de cohérence T après la propagation unitaire. Si un conflit de théorie survient, il est analysé de manière similaire à un conflit booléen, et le solveur revient en arrière chronologiquement. Les atomes de théorie générés lors de la résolution sont traités comme des variables non pertinentes aux fins de projection.

Contributions Clés

L'article expose cinq contributions principales :

Énumération Partielle Disjointe : Une procédure combinant CDCL et Retour Arrière Chronologique pour énumérer des modèles partiels disjoints sans introduire de clauses de blocage.
Algorithmes de Réduction d'Implicants : Deux algorithmes (conservateur et agressif) conçus pour minimiser les affectations partielles tout en adhérant strictement aux contraintes de disjointure du calcul sous-jacent.
Extension à l'Énumération Projetée : Adaptation du solveur pour énumérer uniquement un sous-ensemble de variables importantes, gérant les variables auxiliaires introduites lors de la transformation CNF.
Extension SMT : Intégration du raisonnement théorique dans le cadre d'énumération, permettant la résolution AllSMT avec énumération partielle disjointe.
Évaluation Expérimentale : Un benchmarking complet contre des solveurs de l'état de l'art.

Résultats Expérimentaux

Les auteurs ont évalué TabularAllSAT et TabularAllSMT sur divers benchmarks (3-SAT aléatoire, SATLIB, SMT synthétique et formules non-CNF) par rapport à des solveurs incluant MathSAT5, Dualiza, des solveurs basés sur BDD, et D4+ModelGraph.

Réduction d'Implicants : Le nouvel algorithme de réduction agressive a considérablement réduit le nombre d'affectations partielles générées par rapport à la référence conservatrice, en particulier sur les instances comportant un grand nombre de solutions totales. Bien qu'il ait entraîné une légère surcharge sur les très petites instances, il a amélioré le temps d'exécution global sur les problèmes plus vastes.
Performance AllSAT : TabularAllSAT a performé de manière compétitive ou supérieure à la plupart des solveurs (BC, NBC, MathSAT5). Il a été surpassé par des outils de compilation de connaissances (BDD, D4+ModelGraph) sur des benchmarks spécifiques avec peu de clauses où la surcharge de compilation était faible. Cependant, TabularAllSAT a démontré une empreinte mémoire plus faible et n'a pas subi de dépassement de temps dû à l'épuisement de la mémoire.
AllSAT Projeté : Sur les benchmarks non-CNF nécessitant une projection, TabularAllSAT a nettement surpassé MathSAT5 et Dualiza tant en vitesse qu'en nombre d'instances résolues. Il a également dépassé D4+ModelGraph sur des benchmarks synthétiques plus difficiles.
Performance AllSMT : TabularAllSMT a surpassé MathSAT5 (le seul autre solveur AllSMT projeté disponible publiquement) dans les tâches d'énumération totale et d'énumération partielle. L'absence de clauses de blocage dans TabularAllSMT a empêché la dégradation des performances observée dans MathSAT5 à mesure que la complexité du problème augmentait.

Signification et Revendications

L'article revendique que l'approche proposée offre une alternative supérieure à l'énumération traditionnelle basée sur les clauses de blocage, en particulier dans les scénarios nécessitant une projection et un raisonnement SMT.

Efficacité : En évitant la croissance exponentielle des clauses de blocage, le solveur maintient des performances de propagation unitaire stables et évite les explosions mémoire.
Compacité : L'algorithme de réduction agressive d'implicants produit des affectations partielles plus compactes, réduisant la taille de la sortie et l'espace de recherche pour les étapes d'énumération ultérieures.
Généralité : Le cadre unifie avec succès le CDCL et le Retour Arrière Chronologique pour l'énumération propositionnelle et basée sur des théories, étendant l'applicabilité de l'énumération disjointe à des domaines complexes tels que l'inférence probabiliste et le comptage de modèles sur des théories du premier ordre.

Les auteurs positionnent leur travail comme une réalisation pratique du calcul formel présenté dans [17], fournissant la première implémentation qui gère efficacement la projection et SMT sans la surcharge des clauses de blocage.