G-RRM guide les solveurs symboliques avec des modèles de raisonnement récurrent pour la satisfaction de contraintes

Les auteurs proposent G-RRM, une approche neuro-symbolique qui intègre des modèles de raisonnement récurrent équivariants aux symboles (SE-RRMs) avec des solveurs symboliques classiques pour améliorer l'efficacité de la recherche pour les problèmes de satisfaction de contraintes. Les SE-RRMs agissent comme des solveurs neuronaux générant des propositions de solution pour guider le backtracking ou des méthodes basées sur SAT comme Glucose 4.1 et CaDiCaL 3.0.0.

• L'efficacité de G-RRM nécessite des espaces de recherche combinatoire vastes et des architectures de solveurs capables d'écraser dynamiquement les choix de branching.
• Sur le Sudoku $9\times9$, où les SE-RRMs résolvent 91,1 % des instances, le backtracking est accéléré par un facteur 33,3x et Glucose 4.1 par 1,70x.
• Glucose 4.1 conserve une accélération de 1,17x sur les grilles $25\times25$ avec des indices parfaits.
• CaDiCaL 3.0.0 ne montre aucune accélération significative car il respecte toujours les indices injectés au lieu de les écraser.

Ces résultats délimitent les régimes spécifiques où le guidage neuronal se traduit par des accélérations pratiques en temps réel pour les solveurs symboliques.