La satisfaisabilité booléenne, le problème SAT, est le moteur d’un vaste éventail de tâches informatiques, de la vérification de puces à la cybersécurité en passant par la vérification formelle de preuves. Les algorithmes qui le résolvent ont été affinés par des experts humains pendant des décennies, améliorant progressivement les performances grâce à des heuristiques ingénieuses pour la sélection des variables, la réduction des clauses et le déclenchement des redémarrages.
Une étude publiée dans Nature Communications le 17 juillet montre que les grands modèles de langage peuvent désormais générer des heuristiques de solveur SAT surpassant celles conçues par des humains, avec une amélioration de 40 % du temps d’exécution par rapport à un solveur de référence et en battant les meilleures versions paramétrées des systèmes les plus avancés sur 8 des 11 ensembles de données de référence.
Ce qu’ont fait les chercheurs
L’équipe, dirigée par Ke Wei de l’Université Fudan et Shaowei Cai de l’Académie chinoise des sciences, a développé un cadre appelé AutoModSAT. La découverte clé était que les bases de code des solveurs SAT sont massives et complexes — le solveur populaire Kissat atteint 250 000 tokens. Demander à un LLM de modifier directement une telle base de code serait vain. Au lieu de cela, les chercheurs ont modularisé un solveur CDCL (apprentissage de clauses guidé par les conflits), exposant exactement sept fonctions heuristiques, le déclenchement des redémarrages, la réduction des clauses, l’activation des variables et d’autres, comme un espace de recherche propre.
Avec le solveur modularisé, le système alterne entre trois agents LLM : un Codeur génère un nouveau code heuristique en C++, un Évaluateur filtre les codes sémantiquement identiques aux heuristiques existantes, et un Réparateur corrige les erreurs de compilation. Les heuristiques les plus performantes sont conservées dans une boucle évolutive. L’ensemble du processus utilise 50 appels LLM par domaine problématique et repose sur DeepSeek-V3, choisi pour ses performances compétitives à faible coût.
Ce qu’il a découvert
Sur 11 ensembles de données de référence couvrant des problèmes de concours SAT, de vérification d’automatisation de conception électronique (EDA) et de puzzles combinatoires, AutoModSAT a généré des heuristiques optimisées qui ont offert une amélioration moyenne de 40 % du score PAR-2 (une métrique standard qui pénalise les instances non résolues) par rapport au solveur modulaire de base.
Comparé aux versions paramétrées des solveurs les plus avancés Kissat et CaDiCaL, AutoModSAT a gagné sur 8 des 11 ensembles de données avec une accélération moyenne d’environ 20 %. Sur le problème d’allocation de registres, l’heuristique découverte par LLM a résolu 18 des 20 instances tandis que la référence en a résolu moins de 6. Sur le problème de vérification de sécurité des tables de hachage, avec 11,7 millions de variables et 53,6 millions de clauses, AutoModSAT a produit un score PAR-2 de 3 302 contre 7 322 pour le meilleur concurrent.
Le LLM a également inventé des heuristiques qui n’avaient pas été décrites auparavant dans la littérature. Pour la stratégie de redémarrage, il a généré une méthode dynamique utilisant des moyennes mobiles des scores de qualité des clauses, une approche inédite qui ne faisait partie d’aucun solveur existant.
Pourquoi c’est important
Ceci est qualitativement différent du réglage automatique des hyperparamètres, qui ajuste des paramètres existants. AutoModSAT génère un nouveau code algorithmique, des heuristiques que les experts humains n’avaient pas conçues. Le coût total est de quelques dollars en frais d’API par exécution d’optimisation, ce qui le rend pratique pour un déploiement industriel réel.
L’approche de modularisation elle-même est la revendication la plus forte de l’article : rendre le code du solveur compatible avec les LLM n’est pas facultatif mais fondamental. Cette approche pourrait s’étendre à d’autres solveurs complexes pour la programmation linéaire en nombres mixtes, la satisfaction de contraintes et la démonstration de théorèmes.
Limites
Le solveur de base (ModSAT) est plus simple que les systèmes les plus avancés comme Kissat, qui bénéficient de décennies d’optimisation. Certains gains reflètent la faiblesse relative de la base. Le cadre n’expose que sept fonctions heuristiques et ne peut pas toucher les paramètres de prétraitement de haut niveau, qui sont critiques sur certains ensembles de données. Sur l’ensemble de données Zamkeller, Kissat paramétré a battu AutoModSAT d’un facteur quatre parce que l’écart se trouvait dans un composant que le système ne pouvait pas modifier.
L’article est publié dans Nature Communications (DOI : 10.1038/s41467-026-74949-2) par Y. Sun, F. Ye, Z. Chen, K. Wei et S. Cai.
Sources
1. Y. Sun, F. Ye, Z. Chen, K. Wei, S. Cai, « Discovering Heuristics in a Complex SAT Solver with Large Language Models », Nature Communications (2026). DOI : 10.1038/s41467-026-74949-2
Traduit par Lydie