🤖 AI

Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts

Cet article présente CEGARBox++, une implémentation en C++ qui intègre la résolution modale (KSP) sous forme de raccourcis SAT dans les tableaux CEGAR, démontrant une performance supérieure tant par rapport au KSP autonome qu'aux tableaux CEGAR améliorés par RECAR, particulièrement sur les grands problèmes modaux satisfaisables.

Auteurs originaux : Rajeev Goré (Faculty of Information Technology, Monash University, Australia), Cormac Kikkert (Cormac Kikkert Research)

Publié 2026-07-01

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Rajeev Goré (Faculty of Information Technology, Monash University, Australia), Cormac Kikkert (Cormac Kikkert Research)

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 êtes un détective tentant de résoudre un mystère complexe : un casse-tête logique spécifique est-il possible à résoudre, ou est-ce une contradiction ? Dans le monde de l'informatique, on appelle cela la « satisfiabilité modale ». Le casse-tête implique des règles sur ce qui doit arriver, ce qui pourrait arriver et la manière dont différents scénarios sont connectés les uns aux autres.

Pendant longtemps, les détectives (algorithmes informatiques) utilisaient trois boîtes à outils différentes et concurrentes pour résoudre ces énigmes :

Les solveurs SAT : Excellents pour vérifier si une liste simple de faits s'assemble correctement.
Les Tableaux : Une méthode qui construit un « arbre » de possibilités, se ramifiant pour voir si une histoire valide peut être racontée.
La Résolution : Une méthode qui combine agressivement les règles pour trouver des contradictions, comme un bulldozer dégageant un chemin.

Les auteurs de ce document, Rajeev Goré et Cormac Kikkert, voulaient construire un « Super Détective » capable d'utiliser les meilleures parties de ces trois boîtes à outils. Ils ont créé un système appelé CEGARBox++ et ont testé deux nouvelles façons de le rendre plus rapide.

Le Problème : Le Piège de la « Construction de Modèle »

Leur détective original, CEGARBox, était déjà très bon pour résoudre les casse-têtes « insolubles » (prouver qu'une histoire est un mensonge). Cependant, il peinait avec les casse-têtes « solubles » (prouver qu'une histoire est vraie).

Pourquoi ? Parce que pour prouver qu'une histoire est vraie, CEGARBox devait construire toute l'histoire à partir de zéro.

L'analogie : Imaginez essayer de prouver qu'un labyrinthe possède une sortie. CEGARBox essaierait de dessiner chaque chemin possible à travers le labyrinthe. Si le labyrinthe est immense et possède de nombreuses ramifications, le dessin prend un temps infini, et le détective tombe en panne de temps (un « timeout ») avant d'avoir fini le dessin, même si la sortie existe.

Ils avaient besoin d'un moyen de dire : « Nous n'avons pas besoin de dessiner tout le labyrinthe ; nous avons juste besoin de savoir qu'une sortie existe ». C'est ce qu'on appelle un raccourci ESAT.

Tentative 1 : L'« Architecte Optimiste » (RECAR)

La première nouvelle approche qu'ils ont testée s'appelle RECAR.

L'analogie : Cette approche ressemble à un architecte optimiste qui dit : « Au lieu de construire deux pièces séparées pour deux idées différentes, essayons de construire une seule grande pièce qui convient aux deux. » Si cela fonctionne, nous économisons de l'espace. Si cela échoue, nous les séparons et essayons à nouveau.
Le résultat : Les auteurs ont constaté que cela ne fonctionnait pas bien. L'« optimisme » menait souvent à un effort gaspillé. Le système passait trop de temps à essayer de forcer les choses à s'assembler, pour réaliser plus tard qu'elles ne pouvaient pas l'être, et devait ensuite tout recommencer. C'était plus lent que la méthode originale.

Tentative 2 : L'« Oracle Bulldozer » (KSP)

La seconde approche a changé la donne. Ils se sont associés à un autre détective très agressif appelé KSP (un solveur basé sur la Résolution).

L'analogie : Imaginez que CEGARBox construit une maison pièce par pièce. KSP est un bulldozer qui court devant, abattant les murs et vérifiant les fondations de tout le quartier à la fois.
Comment ils travaillaient ensemble :
1. CEGARBox commence à construire la maison (le modèle logique).
2. KSP tourne en parallèle, vérifiant agressivement si les règles de la maison sont cohérentes.
3. Le moment magique : Si KSP termine la vérification d'une section et dit : « Cette section est solide ; aucune contradiction trouvée », il envoie un signal à CEGARBox.
4. CEGARBox entend cela et dit : « Génial ! Je n'ai pas besoin de construire le reste de cette pièce. Je sais qu'une maison valide existe ici. » Il saute l'étape du travail lourd et passe à la suite.
Le résultat : Ce fut un immense succès. En laissant le « bulldozer » (KSP) faire le gros du travail de vérification de la cohérence, CEGARBox pouvait éviter l'étape coûteuse de la construction de modèles gigantesques. Sur les casse-têtes solubles de grande taille, cette nouvelle équipe (CEGARBox++(KSP)) était beaucoup plus rapide que chaque détective travaillant seul.

La Vue d'Ensemble

Le document affirme que c'est la première fois que ces trois méthodes distinctes (SAT, Tableaux et Résolution) sont combinées avec succès dans un seul système qui est plus performant que chacune d'entre elles prise individuellement.

L'ancienne façon : Vous deviez choisir un détective selon le type de casse-tête. Si c'était un casse-tête de type « non », choisissez CEGARBox. Si c'était un casse-tête de type « oui », choisissez KSP.
La nouvelle façon : Ce nouveau système hybride est un détective « Couteau Suisse ». Il utilise la construction méticuleuse, étape par étape, de CEGARBox pour les casse-têtes insolubles complexes, mais il utilise la vérification rapide et agressive de KSP pour confirmer instantanément les casse-têtes solubles sans avoir à tout construire.

Le Bémol

Les auteurs admettent que leur version actuelle n'est pas parfaite. Comme les deux détectives communiquent en écrivant des notes dans des fichiers (comme s'ils se passaient des petits mots en classe), il y a un certain délai. De plus, le « bulldozer » (KSP) crée parfois trop de paperasse (clauses) pour les casse-têtes très grands et complexes, ce qui ralentit les choses.

Cependant, l'idée centrale — utiliser une méthode pour détecter des « points fixes » (zones de sécurité) afin que l'autre méthode n'ait pas à perdre de temps à les construire — est une avancée majeure. Elle prouve que la combinaison de ces différentes stratégies logiques crée un super-outil qui est supérieur à la somme de ses parties.

Résumé technique : Tableaux CEGAR modaux avec RECAR et raccourcis de résolution par SAT

Énoncé du problème

L'article traite du défi consistant à décider efficacement la satisfaisabilité dans la logique multimodale $K_n$ (également connue sous le nom de ALC). Bien que les tableaux CEGAR (Counter-Example Guided Abstraction Refinement) se soient révélés très efficaces pour les problèmes insatisfaisables et de nombreux problèmes satisfaisables, ils éprouvent des difficultés avec les instances satisfaisables de grande taille. Plus précisément, l'implémentation précédente des auteurs, CEGARBox, surpassait les autres solveurs sur les bancs d'essai standards mais perdait face au prouveur de résolution modale KSP sur l'ensemble de tests MQBF. Le problème central identifié est que les tableaux CEGAR construisent explicitement des modèles satisfaisants ; pour les problèmes présentant des facteurs de branchement élevés, cela peut conduire à la génération de modèles exponentiellement grands, provoquant des dépassements de délai (timeouts). Contrairement aux méthodes basées sur la résolution (comme KSP) qui peuvent déterminer la satisfaisabilité via la saturation sans construire explicitement un modèle complet, les tableaux CEGAR manquent d'un « raccourci ESAT » efficace (un mécanisme pour confirmer rapidement la satisfaisabilité sans construction complète du modèle).

Méthodologie

Les auteurs étudient deux approches distinctes pour intégrer des raccourcis ESAT dans les tableaux CEGAR, implémentées dans un nouveau système C++ appelé CEGARBox++. Les deux approches utilisent une structure de données Trie pour stocker les clauses modales en Forme Normale Clausale Séparée (SNFmc).

1. L'approche RECAR (RECARTAB)

Cette méthode adapte le cadre RECAR (Recursive Explore and Check Abstraction Refinement), initialement proposé par Lagniez et al. pour le CEGAR général.

Mécanisme : Au lieu de créer un monde séparé pour chaque clause diamant déclenchée (ce qui entraîne un branchement exponentiel), RECARTAB tente de regrouper plusieurs clauses diamant dans un seul monde successeur en utilisant une sur-approximation. Elle annote les clauses diamant avec des étiquettes et tente de satisfaire une conjonction de leurs cibles dans un seul monde.
Raffinement : Si un conflit survient impliquant plusieurs diamants, l'algorithme les sépare en assignant des étiquettes fraîches et redémarre la recherche.
Objectif : Trouver un modèle plus petit (moins de mondes) que l'approche CEGAR standard, évitant ainsi l'explosion exponentielle de la génération de mondes.

2. L'approche par Oracle basée sur la Résolution (CEGARBox++(KSP))

Cette approche novatrice intègre le prouveur de résolution modale KSP comme un oracle pour détecter les « points fixes » dans la recherche CEGAR.

Mécanisme : Le système exécute CEGARBox++ et KSP en parallèle (multithread). KSP opère sur un Trie linéaire (SNFml) et effectue la résolution de la couche modale la plus profonde vers la racine.
Détection de point fixe : Lorsque KSP sature complètement une couche modale spécifique $l$ par rapport à la couche $l+1$ , il produit des clauses classiques apprises. CEGARBox++ importe ces clauses. Si une couche est saturée (un « point fixe » est atteint), CEGARBox++ déduit qu'aucun raffinement supplémentaire (apprentissage de nouvelles clauses) n'est possible pour cette couche.
Raccourci : Lors de la détection d'un point fixe, CEGARBox++ saute le processus coûteux de génération de mondes successeurs (la règle de « saut ») pour cette couche et retourne immédiatement Satisfaisable, en s'appuyant sur le lemme selon lequel si la sous-approximation est un point fixe, la formule modale complète est satisfaisable.

Contributions clés

Implémentation de CEGARBox++ : Une nouvelle implémentation C++ de tableaux CEGAR servant de base de référence pour les expériences.
Algorithme RECARTAB : Une extension saine et complète des tableaux CEGAR incorporant des raccourcis ESAT de type RECAR pour tenter la minimisation de modèle.
Intégration CEGARBox++(KSP) : La première intégration efficace de SAT, de tableaux et de méthodes de résolution pour la satisfaisabilité modale. Elle utilise KSP non pas seulement comme un partenaire de portfolio, mais comme un oracle interne pour détecter les points fixes et déclencher une terminaison anticipée pour les problèmes satisfaisables.
Analyse théorique : Preuves formelles de correction, de complétude et de terminaison pour les deux approches basées sur RECAR et sur la résolution.

Résultats expérimentaux

Les auteurs ont évalué leurs approches sur les bancs d'essai K standards (LWB-K, 3CNF et MQBF) en utilisant un processeur Intel i7-11700F.

Performance de RECAR : L'approche RECARTAB (RECARBox) s'est avérée non compétitive. Elle a généralement moins bien performé que le CEGARBox++ standard. Les auteurs attribuent cela à la surcharge liée à la recherche de modèles plus petits ; si un modèle plus petit n'existe pas ou est difficile à trouver, le calcul supplémentaire est gaspillé.
Performance basée sur la résolution : CEGARBox++(KSP) a démontré une performance supérieure :
- Il a nettement surpassé à la fois le CEGARBox++ autonome et le KSP autonome sur les benchmarks MQBF (qui sont dominés par des problèmes satisfaisables).
- Il a obtenu des accélérations allant jusqu'à 100x sur certaines instances satisfaisables par rapport à KSP seul.
- Sur les benchmarks 3CNF, il a performé de manière équivalente à CEGARBox++.
- Sur les benchmarks LWB-K, il a été légèrement surpassé par CEGARBox++ seul, probablement en raison de la surcharge de la génération de la forme normale de KSP produisant plus de clauses pour les formules massives.
Synergie vs Parallélisme : Les auteurs ont écarté la possibilité que les gains de performance soient simplement dus au parallélisme (doublement des ressources). CEGARBox++(KSP) a résolu des problèmes satisfaisables que KSP seul ne pouvait pas résoudre, prouvant que la composante CEGAR a activement contribué à la solution en fournissant le contexte nécessaire au prouveur de résolution ou en élaguant l'espace de recherche via la détection de point fixe.

Signification et Revendications

L'article affirme que CEGARBox++(KSP) représente la première intégration efficace de SAT, de tableaux et de résolution pour la satisfaisabilité modale qui est plus performante que ses composants individuels.

Surmonter les limitations : Ce travail traite de la faiblesse fondamentale des tableaux CEGAR dans la gestion des grands problèmes satisfaisables en introduisant un mécanisme pour détecter quand un modèle existe sans le construire explicitement.
Forces complémentaires : Les résultats soulignent que, bien que les solveurs basés sur SAT, sur tableaux et sur la résolution soient traditionnellement des méthodes concurrentes avec des forces différentes (ex: tableaux pour l'insatisfaisabilité, résolution pour la satisfaisabilité), leur intégration peut produire un solveur « supérieur à la somme de ses parties ».
Perspectives : Les auteurs notent modestement que leur implémentation actuelle est naïve (utilisant les entrées/sorties de fichiers pour la communication et la forme normale spécifique de KSP). Ils suggèrent qu'une intégration plus polie, utilisant potentiellement la propre génération de forme normale de CEGAR et de meilleurs protocoles de communication, pourrait permettre à cette approche hybride de surpasser les solveurs existants sur tous les bancs d'essais, y compris les benchmarks LWB-K où elle accuse actuellement un léger retard.

L'article conclut que, bien que l'approche RECAR n'ait pas été fructueuse dans ce contexte, la stratégie de détection de point fixe utilisant un oracle de résolution est une direction prometteuse pour les algorithmes CEGAR récursifs, particulièrement ceux impliquant du branchement.