Résumé technique : Augmentation de données consciente de la cible pour la prédiction de SAT

1. Énoncé du problème

L'application de l'apprentissage automatique, en particulier des réseaux de neurones à graphes (GNN), à des problèmes NP-difficiles comme la satisfaisabilité booléenne (SAT) est fondamentalement limitée par le coût élevé de la génération de données d'entraînement étiquetées. Les pipelines standards reposent sur une approche « solveur dans la boucle », où des formules aléatoires sont générées puis résolues par des solveurs SAT complets (par exemple CaDiCaL) pour déterminer leurs étiquettes (SAT ou NON-SAT). À mesure que la taille des problèmes augmente, en particulier près de la transition de phase de la satisfaisabilité, ce processus d'étiquetage devient exponentiellement coûteux, limitant sévèrement l'échelle des supervisions utilisables. Ce goulot d'étranglement entrave la capacité d'exploiter des données à grande échelle pour capturer les propriétés structurelles des problèmes combinatoires difficiles, une condition préalable au succès des paradigmes modernes d'apprentissage profond.

2. Méthodologie

Les auteurs proposent une approche à double volet : un cadre de génération de données sans solveur, conscient de la cible, et une architecture de GNN consciente de l'optimisation.

2.1 Génération de données sans solveur, consciente de la cible

L'idée centrale réside dans une asymétrie : si trouver une affectation satisfaisante pour une formule donnée est NP-difficile, construire une formule autour d'une affectation (ou d'une contradiction) connue est computationnellement efficace. Les auteurs adoptent un point de vue « solution en premier », construisant des instances par construction plutôt que par échantillonnage et vérification.

• Génération d'instances SAT : La méthode échantillonne une affectation de référence aléatoire $x^*$. Pour chaque clause, elle échantillonne une « marge » (slack) cible $s^*$ à partir de la distribution empirique d'une référence cible (par exemple G4SATBench). La marge représente le nombre de littéraux dans une clause satisfaits au-delà du seul requis pour la faisabilité. Le générateur construit ensuite de manière déterministe des clauses avec des polarités spécifiques de telle sorte que exactement $s^* + 1$ littéraux soient satisfaits par $x^*$. Cela garantit que l'instance est satisfaisable par construction et correspond à la distribution de marges de la référence.
• Génération d'instances NON-SAT : La méthode intègre un petit cœur garanti NON-SAT (un ensemble de clauses couvrant toutes les combinaisons de polarité d'un sous-ensemble de variables) au sein d'un ensemble plus large de clauses « de remplissage ». Les clauses de remplissage sont générées en utilisant la même méthode de plantation de marges que pour les instances SAT, en s'alignant sur la distribution de marges NON-SAT de la référence. L'étiquette est connue par construction (NON-SAT) sans nécessiter de solveur.
• Conscience de la cible : Contrairement aux constructions plantées génériques, ce cadre correspond explicitement aux statistiques structurelles (largeur des clauses, biais d'occurrence et distributions de marges) d'une référence cible afin de minimiser le décalage distributionnel.

2.2 Réseau de neurones à graphes conscient de la programmation linéaire (LPGNN)

Pour exploiter la structure algébrique des données générées, les auteurs introduisent le LPGNN.

• Encodage : Les formules CNF sont mappées à un problème de faisabilité linéaire binaire $Ax \geq b$. Des variables de marge $s$ sont introduites pour convertir les inégalités en égalités : $Ax - s = b$.
• Structure du graphe : Le graphe contient deux types de nœuds : les nœuds de variables ($x$) et les nœuds de marge ($s$). Les arêtes relient les variables aux nœuds de marge des clauses dans lesquelles elles participent.
• Passage de messages avec résidus : L'architecture intègre un mécanisme de résidu de programmation linéaire (LP). À chaque couche, le réseau projette les plongements de nœuds vers un substitut continu $\tilde{z}$. Il calcule un résidu de contrainte $r = \tilde{A}\tilde{z} - b$ dans l'espace des contraintes. Ce résidu est mappé de retour dans l'espace des nœuds via la transposée $\tilde{A}^T r$, fournissant un signal de faisabilité (gradient de la violation de contrainte) qui est injecté dans les mises à jour des nœuds. Cela permet au GNN d'exploiter directement la structure d'optimisation sous-jacente.

3. Contributions clés

1. Cadre de génération sans solveur : Une méthode native CNF pour générer des instances SAT et NON-SAT correctement étiquetées par construction, éliminant le besoin d'appels coûteux à des solveurs lors de la création des données.
2. Alignement conscient de la cible : Une stratégie qui aligne les données synthétiques avec les propriétés structurelles et algébriques (spécifiquement les distributions de marges) des références cibles, rendant les données efficaces pour l'apprentissage en aval.
3. Architecture LPGNN : Une conception novatrice de GNN qui intègre des résidus de violation de contrainte basés sur la programmation linéaire dans le passage de messages, exposant la structure de faisabilité algébrique au modèle.
4. Paradigme centré sur les données : Une démonstration que pour les problèmes NP-difficiles, la génération de données évolutives et alignées sur la tâche est aussi cruciale que la conception de l'architecture du modèle.

4. Résultats expérimentaux

• Efficacité de génération : La méthode proposée atteint des accélérations de plusieurs ordres de grandeur par rapport aux bases de référence « solveur dans la boucle ». Pour les grandes instances (par exemple $n=1000$), la méthode sans solveur est environ $10^{14}$ fois plus rapide que la base de référence CaDiCaL extrapolée.
• Alignement distributionnel : Les instances générées reproduisent fidèlement les distributions de marges de l'ensemble de données cible G4SATBench (Figure 1).
• Comportement d'échelle : L'entraînement du LPGNN sur les données synthétiques générées montre une amélioration constante des performances à mesure que le volume d'entraînement augmente.
  • Prédiction SAT : Le taux de satisfaction des contraintes (CSR) s'améliore d'environ 88 % à environ 99 % lorsque le volume de données passe de 250 à 10 000 instances.
  • Prédiction NON-SAT : La fraction de clauses violées ($k/m$) diminue, indiquant une meilleure qualité d'affectation pour les instances insatisfaisables.
• Généralisation : Les avantages des données conscientes de la cible s'étendent à d'autres architectures (NLocalSAT, QuerySAT) et se généralisent à des ensembles de test hors distribution (niveaux 3-SAT plus difficiles et familles SR).
• Ablation : La suppression du mécanisme de résidu LP du LPGNN entraîne une baisse de la précision et du CSR, confirmant la valeur du signal conscient de l'optimisation.
• Comparaison avec des données génériques : L'entraînement sur des données synthétiques génériques et non alignées produit des performances proches du hasard, soulignant que l'alignement structurel est le facteur clé de succès.

5. Signification et affirmations

L'article affirme que le principal goulot d'étranglement dans les solveurs SAT basés sur l'apprentissage n'est pas la capacité du modèle, mais le coût de l'obtention de données étiquetées. En introduisant un pipeline de génération évolutif et sans solveur produisant des données synthétiques alignées sur les références, les auteurs démontrent qu'il est possible d'entraîner efficacement des GNN sans dépendre de solveurs coûteux pour la supervision.

Les auteurs positionnent ce travail comme un virage vers un paradigme centré sur les données pour les problèmes NP-difficiles. Ils soutiennent que tout comme la prédiction du prochain jeton a permis la mise à l'échelle des modèles de langage, la génération de données évolutives et alignées sur la tâche est le principal catalyseur pour débloquer le potentiel de l'apprentissage automatique dans l'optimisation combinatoire. Le travail ne prétend pas résoudre des instances SAT qui sont intraitables pour les solveurs actuels, mais plutôt fournir un mécanisme pour générer les données d'entraînement à grande échelle et de haute qualité nécessaires pour améliorer la recherche heuristique et la prédiction d'affectation dans les GNN. Les auteurs reconnaissent les limitations concernant l'écart « synthétique-réel », notant que les instances manufacturées peuvent ne pas capturer parfaitement les structures communautaires cachées des problèmes industriels spécialisés, mais soutiennent que l'approche sert de régularisateur puissant pour l'apprentissage en distribution.