Learning to Rank the Initial Branching Order of SAT Solvers

Cette étude propose d'utiliser des réseaux de neurones à graphes pour prédire un ordre de branchement initial efficace afin d'accélérer les solveurs SAT de type CDCL sur des instances aléatoires et pseudo-industrielles, tout en constatant que cette approche perd de son efficacité sur des instances industrielles complexes où les heuristiques dynamiques du solveur annulent rapidement l'initialisation.

L'essentiel

Voici une explication simple de ce papier de recherche, imagée comme si l'on racontait une histoire.

🧠 Le Problème : Perdu dans une forêt de décisions

Imaginez que vous devez résoudre un immense casse-tête logique (un problème SAT). C'est comme essayer de trouver la sortie d'un labyrinthe gigantesque où chaque intersection vous oblige à choisir entre deux chemins : "Gauche" ou "Droite".

Les ordinateurs actuels (les "solveurs SAT") sont très forts, mais ils sont un peu comme des randonneurs qui avancent au hasard. À chaque carrefour, ils choisissent une direction en se basant sur des règles fixes et un peu rigides (par exemple : "Choisis toujours la porte la plus proche"). Parfois, ces règles fonctionnent bien, mais souvent, elles les font faire des milliers de boucles inutiles avant de trouver la sortie.

Le problème, c'est que le tout premier choix que l'on fait au début du labyrinthe est crucial. Si on commence par la mauvaise porte, on peut passer des heures à errer. Si on commence par la bonne, on sort en quelques minutes.

💡 L'Idée : Un guide qui connaît le chemin avant de partir

Les auteurs de ce papier se sont dit : "Et si on entraînait un petit assistant intelligent (une Intelligence Artificielle) pour qu'il nous dise quelle porte choisir en premier, avant même que le randonneur ne commence à marcher ?"

C'est là qu'intervient le Réseau de Neurones Graphique (GNN). Imaginez ce réseau comme un expert cartographe qui a étudié des milliers de labyrinthes. Il ne résout pas le labyrinthe lui-même (ce serait trop lent), mais il regarde la carte et vous dit : "Hé, pour ce type de labyrinthe, commence toujours par la porte bleue, c'est là que se trouve la sortie !"

🛠️ Comment ils ont fait ? (Les trois méthodes d'entraînement)

Pour apprendre à cet expert cartographe, il faut lui montrer des exemples de "bons premiers pas". Mais comment savoir quel est le "bon" premier pas ? Les chercheurs ont testé trois méthodes pour étiqueter ces bons choix :

1. La méthode du "Conflit" (Le détective) : On laisse le randonneur résoudre le labyrinthe une fois. On regarde quelles portes ont causé le plus de problèmes (des impasses). On dit au GNN : "Voilà, ces portes sont les plus importantes, commence par elles !". C'est comme apprendre en regardant où les autres ont échoué.
2. La méthode du "Premier Pas" (L'expérimentateur) : On force le randonneur à commencer par la porte A, puis la porte B, puis la porte C, des milliers de fois. On mesure quelle porte a permis de sortir le plus vite. C'est long à faire, mais très précis.
3. La méthode "Génétique" (L'évolution) : On crée des milliers de listes de portes au hasard, on garde les meilleures, on les mélange un peu, et on recommence jusqu'à trouver la liste parfaite. C'est comme l'évolution naturelle pour trouver le meilleur chemin.

🚀 Les Résultats : Une victoire (mais avec des limites)

Une fois l'expert cartographe entraîné, ils l'ont mis à l'épreuve :

• Sur les petits et moyens labyrinthes (problèmes générés aléatoirement) : C'est une révolution ! Le GNN a permis de résoudre les problèmes jusqu'à 50 % plus vite. Il a su généraliser son apprentissage : même sur des labyrinthes beaucoup plus grands que ceux qu'il avait vus à l'entraînement, il a continué à donner de bons conseils.
• Sur les labyrinthes géants et complexes (problèmes industriels réels) : Là, ça coince un peu. Les gains de vitesse sont faibles, voire nuls.

🤔 Pourquoi ça ne marche pas toujours ?

Les chercheurs ont trouvé deux raisons principales à cet échec sur les gros problèmes :

1. Le randonneur oublie le guide : Une fois que le randonneur a fait son premier pas, il se met à utiliser ses propres règles très rapides pour décider des pas suivants. Il oublie vite le conseil initial du GNN. C'est comme si vous donniez une carte à un guide, mais qu'il la jette dès la première minute pour suivre son instinct.
2. La complexité est trop grande : Pour les problèmes énormes, le labyrinthe est si compliqué que même l'expert cartographe a du mal à deviner le meilleur premier pas. Le bruit dans les données est trop fort.

🎯 En résumé

Ce papier nous dit que l'IA peut aider les ordinateurs à résoudre des problèmes logiques beaucoup plus vite, à condition de leur donner un bon point de départ.

C'est comme si on apprenait à un coureur de fond à bien s'élancer au départ d'une course. Sur des courses moyennes, un bon départ change tout. Mais sur des courses ultra-marathons très techniques, le départ ne suffit plus à garantir la victoire, car le reste de la course devient trop complexe pour que le conseil initial reste utile.

C'est une belle première étape vers des "solveurs hybrides" qui combinent la puissance de calcul brute des ordinateurs et l'intuition de l'IA.

Résumé technique

Voici un résumé technique détaillé de l'article « Learning to Rank the Initial Branching Order of SAT Solvers », publié lors du VerifAI-2.

1. Problématique

Le problème de la satisfiabilité booléenne (SAT) est un problème NP-complet fondamental pour la vérification formelle et la preuve automatique. Les solveurs SAT modernes, basés sur l'apprentissage de clauses par conflit (CDCL), reposent sur des heuristiques fixes et manuelles pour guider la recherche (choix de la variable à brancher). Bien que performants en moyenne, ces heuristiques échouent souvent sur des instances complexes ou industrielles.

L'objectif de cet article est d'améliorer l'efficacité des solveurs SAT existants en prédisant un ordre de branchement initial optimal à l'aide de réseaux de neurones graphiques (GNN), avant d'engager la résolution. L'hypothèse centrale est que le choix de la première variable (et de l'ordre initial) a un impact disproportionné sur le temps de résolution, et qu'un GNN peut apprendre à identifier ces variables critiques à partir de la structure du graphe du problème.

2. Méthodologie

L'approche proposée consiste en un pipeline de prétraitement où un GNN prédit un ordre de variables, qui est ensuite injecté dans un solveur SAT standard (MiniSat ou CaDiCaL).

A. Représentation du graphe

Les instances SAT sont converties en graphes tripartites :

• Nœuds : Variables et clauses.
• Arêtes : Indiquent la présence d'une variable dans une clause, avec un poids indiquant si la variable est négée ou non.
• Nœud méta : Un nœud central connecté à toutes les clauses pour faciliter le passage de messages.
• Features : Encodages one-hot basés sur les quartiles du degré des nœuds pour améliorer la performance.

B. Méthodes d'étiquetage (Labeling)

Pour entraîner le GNN, il faut déterminer un "ordre idéal" (label) pour chaque instance. Les auteurs proposent trois méthodes :

1. Étiquetage par conflit (Conflict Labeling) : Classe les variables selon le nombre total de conflits auxquels elles ont participé durant une résolution. Hypothèse : les variables à fort conflit sont des "backdoor variables" dont la résolution précoce simplifie le problème.
2. Étiquetage par première variable (First Variable Labeling) : Calcule la moyenne des propagations obtenues lorsque chaque variable est forcée en premier sur plusieurs exécutions (avec le reste de l'ordre aléatoire). Cela isole la contribution individuelle de chaque variable.
3. Étiquetage génétique (Genetic Labeling) : Formule le problème comme une optimisation pour trouver l'ordre minimisant les propagations, en utilisant un algorithme génétique (hill-climbing) sur des permutations.

C. Architecture du GNN et Fonction de Perte

• Architecture : Basée sur NeuroBack, utilisant des mécanismes d'attention avec une complexité mémoire linéaire.
• Sortie : Un score pour chaque variable.
• Fonction de perte : Utilisation de LambdaRank (Learning to Rank). La pertinence d'une variable est définie par $1/\log_2(Rank)$, accordant une importance cruciale au placement correct des variables en haut de la liste (les premières décisions étant les plus critiques).

D. Intégration au Solveur

Pour injecter l'ordre prédit sans modifier profondément le solveur, les auteurs initialisent les niveaux d'activité des variables utilisés par les heuristiques VSIDS (MiniSat) et VMTF (CaDiCaL). Cela force le solveur à sélectionner les variables prédites en priorité au début de la recherche.

3. Contributions Clés

1. Validation empirique de l'impact du branchement initial : L'article démontre que le choix de la première variable peut réduire le temps de résolution de manière significative (jusqu'à 2200% sur des instances aléatoires de 100 variables), confirmant l'existence d'un classement hiérarchique des variables.
2. Proposition de trois méthodes d'étiquetage : Comparaison de stratégies pour générer des labels d'entraînement, montrant que l'étiquetage par conflit est le plus robuste et le plus facile à apprendre pour le GNN.
3. Pipeline GNN-SAT hybride : Démonstration qu'un GNN peut prédire un ordre de branchement qui accélère la résolution sur des instances aléatoires et pseudo-industrielles, avec une capacité de généralisation à des instances beaucoup plus grandes que celles utilisées pour l'entraînement.

4. Résultats

Les expériences ont été menées sur MiniSat et CaDiCaL avec trois types de distributions :

• Instances aléatoires 3-CNF :

  • Des gains significatifs sont observés, réduisant le temps de résolution de plus de 50 % pour des instances de 200 variables ou moins.
  • Le modèle, entraîné sur de petites instances (20-40 variables), généralise bien jusqu'à 5-10 fois la taille des données d'entraînement.
  • L'étiquetage par conflit donne de meilleures corrélations (Spearman ~0.37) que les autres méthodes.

• Instances G4SATBench (Pseudo-industrielles) :

  • Sur les instances "faciles", une réduction de 10-20 % des propagations est observée.
  • Sur les instances "difficiles" (> $10^5$ propagations), les gains disparaissent et les performances se rapprochent des solveurs de base.

• Instances Industrielles (SAT Competition 2024) :

  • Aucun gain significatif n'est observé par rapport aux solveurs de base.
  • Les auteurs attribuent cet échec à deux facteurs :
    1. Écrasement dynamique : Les heuristiques dynamiques du solveur (VSIDS/VMTF) écrasent rapidement l'initialisation statique fournie par le GNN lors de résolutions longues.
    2. Complexité structurelle : La complexité des instances industrielles rend la prédiction d'un ordre initial optimal trop difficile pour le GNN.

5. Signification et Conclusion

Ce travail identifie l'ordre de branchement initial comme un point de rencontre sous-exploité mais prometteur entre les réseaux de neurones et les solveurs SAT de pointe.

• Points forts : La méthode offre une accélération notable sur des problèmes générés et semi-industriels sans modifier l'architecture interne complexe du solveur, agissant comme un "warm start" intelligent.
• Limites : L'approche actuelle est limitée par la nature dynamique des solveurs modernes qui annulent les initialisations statiques sur les problèmes très difficiles.
• Perspectives futures : L'article suggère que pour être efficace sur des problèmes industriels complexes, les approches hybrides devront peut-être évoluer vers des mécanismes de rappel périodique de l'ordre suggéré ou des architectures capables de s'adapter dynamiquement, plutôt que de se limiter à une initialisation unique.

En résumé, bien que la prédiction d'un ordre initial ne résolve pas encore les défis des instances industrielles les plus dures, elle prouve que les GNN peuvent apprendre la structure sous-jacente des problèmes SAT pour optimiser les étapes critiques de la recherche.