CaDiCaL 3.0.0

G-RRM: Neuro-symbolic approach guides SAT solvers with recurrent neural reasoning models

Researchers introduce G-RRM (Guiding with Recurrent Reasoning Models), a neuro-symbolic framework that uses symbol-equivariant recurrent neural networks (SE-RRMs) to guide classical symbolic solvers—including backtracking and SAT solvers Glucose 4.1 and CaDiCaL 3.0.0—for constraint satisfaction problems. On 9×9 Sudoku, the approach achieves 33.3× speedup for backtracking and 1.70× for Glucose 4.1, but shows no significant gain for CaDiCaL due to its overhead-dominated runtime and inability to overwrite injected hints. The paper identifies two conditions for neural guidance to be effective: a large combinatorial search space and a solver architecture capable of dynamically overriding imperfect neural hints.