G-RRM: Guiding Symbolic Solvers with Recurrent Reasoning Models

Symbolic solver have to branch to check different choices – recurrent reasoning models ( not LLMs!) can help them to speed up solving.

BTW: Frontier AIs fail here!

P: https://t.co/kAEoEmp2S7 https://t.co/uZAPqkrTgR

G-RRM: Guiding Symbolic Solvers with Recurrent Reasoning Models

Source: https://arxiv.org/html/2607.02491 \DeclareMathOperator

*\argmaxarg max\DeclareMathOperator*\argsortarg sort\theorembodyfont\theoremheaderfont\theorempostheader:\theoremsep

\NameTimo Bertram\nametag1 \NameSidhant Bhavnani\nametag2 \NameRichard Freinschlag\nametag1 \NameErich Kobler\nametag1,3 \NameAndreas Mayr\nametag1 \NameGünter Klambauer\nametag1,3 \addr1ELLIS Unit LinzJohannes Kepler University LinzAustria 2Institute for Symbolic Artificial IntelligenceJohannes Kepler University LinzAustria 3Clinical Research Institute for Medical AIJohannes Kepler University LinzAustria

Abstract

Looped Transformers have recently gained significant attention in machine learning as a powerful attention-based architectural paradigm integrating iterative refinement with recurrent parameter sharing. Variants of this architecture have shown promising results on ARC-AGI and Sudoku, both of which are considered to require multi-step reasoning. Looped transformers give rise to recurrent reasoning models (RRMs), such as the Hierarchical Reasoning Model (HRM) and the Tiny Recursive Model (TRM). Despite their success, RRMs provide no guarantees of correctness: each iteration predicts a complete problem assignment and greedy decoding can yield constraint-violating solutions. In this work, we focus on SE-RRMs, a symbol-equivariant instantiation of RRMs that exhibits improved extrapolation to larger problem sizes. We propose a neuro-symbolic approach, “Guiding with Recurrent Reasoning Models” (G-RRM), which integrates SE-RRMs with symbolic solvers for constraint satisfaction problems. SE-RRMs act as neural solvers that generate full solution proposals and guide classical symbolic solvers, such as backtracking or SAT-based methods like Glucose 4.1 and CaDiCaL 3.0.0, that produce globally correct solutions. Centrally, we investigate when neural guidance with G-RRM improves the search efficiency of symbolic solvers. Our experiments show that the efficacy of G-RRM depends on two conditions: first, the problem instances must have an expansive combinatorial search space to expose potential gains, and second, the solver architecture must be capable of dynamically overwriting its branching choices to recover when neural hints are imperfect. When these conditions hold, guidance drives median conflict counts to zero and yields significant wall-clock speedups: on9×99\times 9Sudoku, where the SE-RRM correctly solves91.1%91.1\%of instances, backtracking accelerates by33.3×33.3\timesand Glucose 4.1 by1.70×1.70\times(median,p<0.001p<0.001), with Glucose 4.1 retaining a1.17×1.17\timesspeedup on perfect-hint25×2525\times 25grids. In contrast, CaDiCaL 3.0.0, whose runtime is overhead-dominated and which always respects the injected branching hints rather than overwriting them, shows no significant speedup (median1.02×1.02\times, n.s.) and even a small significant mean slowdown (0.90×0.90\times) on9×99\times 9. These results delineate the regimes in which neural guidance translates into practical speedups.

\floatconts

fig:comparison_NBRRM

Figure 1:Comparison of a naive search approach (left) to G-RRM (right). Naive search follows a heuristic order of digits, while guided search uses a neural network to order symbol assignments based on confidence.## 1Introduction

Looped Transformers/Recurrent Reasoning Models to Solve Combinatorial Problems.

Due to their parameter efficiency and inherent capability to execute iterative algorithmic procedures through recursive state updates, looped transformers(Liu2024)offer a promising framework for solving complex combinatorial problems. However, they lack the capacity for rigorous logical verification(Renkhoff2024), raising the question of how to effectively pair their predictive strength with the exact constraints of symbolic methods. At this interface, Recurrent Reasoning Models (RRMs), such as Hierarchical Reasoning Models (HRMs)(wang2025hierarchical)and Tiny Recursive Models (TRMs)(jolicoeur2025less), have emerged as specialized looped transformers. Despite being called reasoning models, these models do not alter the inherently inductive nature of machine learning, as they perform no deductive logic. Rather, they apply a learned operator to iteratively update an internal state. Nevertheless, they exhibit remarkable predictive performance on heavily constrained tasks. This high accuracy is unlocked by a scalable training methodology that leverages intermediate supervision and stop-gradient operations between individual loop iterations to efficiently optimize deeply looped structures. Consequently, this training paradigm has allowed RRMs to achieve strong empirical results across combinatorial domains, such as Sudoku puzzles and abstract visual reasoning tasks from the ARC-AGI benchmark(chollet2025arc).

Boolean Satisfiability and Modern SAT Solvers.

Combinatorial problems are traditionally encoded as instances of the Boolean Satisfiability (SAT) problem, the foundational NP-complete problem in theoretical computer science, to provide logical guarantees of correctness. Over the past decades, practical SAT solving has evolved from a purely theoretical challenge into an industrial-grade methodology driven by various advancements in algorithms, heuristics and data structures that can solve large instances.

Sudoku as an Established Combinatorial Benchmark.

Sudoku puzzles serve as an ideal and widely adopted combinatorial benchmark. Despite their conceptual simplicity, a Sudoku puzzle embodies a rigorous Constraint Satisfaction Problem (CSP) governed by strict, non-local rules. Given a grid partially filled with digits, the task is to assign symbols to all remaining cells while ensuring that each row, column, and subgrid contains every symbol exactly once. The generalized decision problem is NP-complete(yato2003complexity), highlighting its intrinsic computational difficulty. Despite its simple rules, Sudoku poses significant challenges for neural networks. Purely neural approaches often generate locally plausible but globally inconsistent assignments and struggle to extrapolate to unseen grid sizes or symbol sets(long2023large;seely2025sudoku;giannoulis2026teachingtransformers;vamsi2021deep). Our approach aims to solve this problem by combining neural approaches with exact solvers, which prevents inconsistent assignments and guarantees correctness.

Neurosymbolic Integration.

To formalize the interplay between these empirical neural approximations and exact deductive logic, we contextualize our approach within Kautz’s taxonomy of neural-symbolic integration(kautz2022third). Architecturally, a pipeline that feeds the predictive outputs of a recurrent reasoning model (RRM) into a downstream symbolic SAT solver most closely aligns with aNeuro | Symbolicsystem (Type 3). While Kautz frames a fully integratedNeuro[Symbolic]architecture (Type 6), where symbolic constraints are natively embedded within the neural execution graph, as the ultimate paradigm for combinatorial reasoning, achieving this state with 100% correctness remains open.

Existing neuro-symbolic frameworks highlight these limitations when applied to hard constraint tasks. For instance, the neuro-symbolic solver ofhathidara2023neuroremains restricted to Sudoku puzzles with at most eight missing entries, while oscillatory neural network approaches fail when more than roughly half of the cells are unfilled(haverkort2025solving). Even more general neuro-symbolic learning frameworks, such as semantic constraint strengthening, achieve only modest solve rates of around 28% and do not reliably solve full, high-difficulty instances(ahmed2023semantic;wang2019satnet).

In contrast, recent architectural innovations have closed this empirical performance gap. Recurrent reasoning models have substantially advanced pure neural Sudoku solving, achieving solve rates of roughly 70% on extremely difficult9×99\times 9puzzles with more than half of the digits missing. Building on this progress, symbol-equivariant RRMs (SE-RRMs) further raise this fully solved rate to over 90%, while remaining exceptionally compact and trainable from small instances(freinschlag2026symbol).

A recurrent reasoning model can propose a full solution to a puzzle in a single forward pass, but it cannot certify it satisfies all constraints. A symbolic solver offers the counterpart: it guarantees correctness without prior knowledge of promising solutions. Coupling the sub-symbolic and symbolic components lets the RRM serve as a prior for the solver’s search. When the network is correct, the solver verifies an assignment with no extra search; when it is wrong, the solver falls back on its own completeness guarantees and potentially takes advantage of promising subareas of the search space.

We show that the benefit of this combination is dependent on two factors: (i) the problem’s expansive search space dominates the solver’s runtime for an instance, and (ii) the ability of the solver to dynamically overwrite its branching choices to exploit the hints of the neural model. Consequently, the accuracy of the hints also determines the benefit.

Overview.

In this work, we introduce Guiding with Recurrent Reasoning Models (G-RRM), a neuro-symbolic framework in which symbolic solvers are guided by the predictive symbol probabilities of a trained Symbol-Equivariant RRM. The paper is organized as follows. Section 2 formalizes the problem setting and defines the search-guidance mechanism for backtracking and CDCL solvers. Section 3 presents our experimental evaluation across Sudoku grids of varying sizes, benchmarking G-RRM against naive backtracking and the modern SAT solvers Glucose 4.1 and CaDiCaL 3.0.0. Section 4 concludes our findings and identifies the conditions under which neural guidance improves solver efficiency. Finally, Section 5 outlines limitations of our work and Section 6 describes future work.

2Problem Setting and Methodological Background

2.1Recurrent Reasoning Models

We briefly review recurrent reasoning models (RRMs), including HRM(wang2025hierarchical), TRM(jolicoeur2025less), and SE‑RRM(freinschlag2026symbol). Throughout, we follow the notation offreinschlag2026symbol. For a more in-depth explanation, please refer to\appendixrefapp:rrm.

Problem Setting and Notation.

RRMs have been developed for structured problem‑solving tasks, such as Sudoku solving or maze navigation, where both the input and the possible solutions consist of assignments of discrete values to grid cells. A task instance is represented as a tuple of discrete symbols𝑿=(x1,…,xI),xi∈Σ,\bm{X}=(x_{1},\dots,x_{I}),\;x_{i}\in\Sigma,whereIIis the number of grid cells andΣ\Sigmais a symbol alphabet withK:=|Σ|K:=|\Sigma|symbols (e.g., digits and an additional mask symbol). A solution is represented analogously as𝒀=(y1,…,yI)\bm{Y}=(y_{1},\dots,y_{I})withyi∈Σy_{i}\in\Sigma.

Operational Principle.

RRMs are specialized looped transformer architectures proposed for multi-step reasoning, where the same Transformer-based computational block is repeatedly reused to iteratively refine an internal latent representation (see (2) in\appendixrefapp:rrm). As looped transformers, RRMs are highly parameter-efficient due to extensive parameter sharing across recurrent iterations. Their practical success is largely attributed to a scalable training methodology based on deep supervision and stop-gradient operations. HRM and TRM mainly differ in how they architecturally realize recurrent computation.

Symbol-Equivariant RRMs (SE-RRMs).

SE-RRMs modify the standard RRM formulation to achieve symbol equivariance. They introduce an explicit symbol axis into the latent representation, yielding rank-3 tensors of shapeD×I×KD\times I\times Kinstead of the standard rank-2 representations of shapeD×ID\times I, whereDDis the feature dimension. This change is reflected in corresponding adaptations of both the input encoding and the recurrent update, in particular through the inclusion of attention over the symbol dimension.

SE-RRM provides per-cell symbol distributions that remain meaningful even when the symbol set changes, making it a natural candidate as a learned policy for symbolic search, e.g., for variable ordering in backtracking. This is the key interface for guiding symbolic methods.

2.2Symbolic Search and Verification

2.2.1Backtracking Search

Backtracking uses depth-first search to explore possible solutions in a search tree while continuously checking constraints and undoing choices when violations occur. For Sudoku, it starts from a partially filled puzzle and repeatedly selects empty cells to fill. Nodes in the search tree correspond to partially filled puzzles, while edges represent valid digit assignments to a previously empty cell.

Whenever the algorithm reaches a state in which an empty cell has no valid digit available, the current partial solution cannot be extended to a complete solution. In this case, the algorithm backtracks by undoing the most recent assignment and exploring alternative edges. This process is repeated until either a complete valid Sudoku solution is found or all possible assignments have been exhausted.

This strategy guarantees completeness: if a valid Sudoku solution exists, backtracking will eventually find it by systematically exploring all feasible assignments.

2.2.2Sudoku as a SAT Problem

To solve Sudoku using highly optimized modern SAT solvers, the puzzle must be encoded as a formula in Conjunctive Normal Form (CNF). We introduce Boolean variablesxr,c,vx_{r,c,v}indicating that cell(r,c)(r,c)contains valuevv, wherer,c,v∈{1,…,N}r,c,v\in\{1,\dots,N\}for anN×NN\times Ngrid. Every Sudoku rule constrains a given region (a cell, row, column, orN×N\sqrt{N}\times\sqrt{N}box) to contain exactly one instance of a value. We enforce this using a standard structural encoding where anAt-Least-One(ALO) clause⋁v=1Nxr,c,v\bigvee_{v=1}^{N}x_{r,c,v}ensures that every cell is assigned at least one digit, while pairwiseAt-Most-One(AMO) clauses(¬xr,c,v∨¬xr,c,w)(\lnot x_{r,c,v}\lor\lnot x_{r,c,w})forv≠wv\neq wforbid duplicate assignments so no cell contains multiple values. This identical ALO/AMO pattern is applied across all rows, columns, and boxes to enforce global constraint satisfaction. Prefilled cells are permanently fixed to true via unit clausesxr,c,vx_{r,c,v}.

The resulting CNF formula is satisfiable if and only if a valid Sudoku completion exists. The full encoding requiresN3N^{3}variables and yields11,98811{,}988base clauses for9×99\times 9,123,904123{,}904for16×1616\times 16, and752,500752{,}500for25×2525\times 25grids.

2.2.3SAT Solving

Modern Conflict-Driven Clause Learning (CDCL) SAT solvers, like Glucose 4.1 (glucose4)(glucose)and CaDiCaL 3.0.0 (cadical3)(cadical), evaluate propositional formulas in CNF by combining systematic search with logical deduction and dynamic clause database management. Rather than traversing the search space chronologically, a CDCL solver relies on three key foundational features, which we discuss below.

Heuristic Selection (Variables and Phases).

The solver dynamically selects unassigned variables using scoring metrics like Variable State Independent Decaying Sum (VSIDS)(chaff). For each chosen variable, the solver must also select a literal polarity (phase) to determine which truth value to explore first.

Conflict-Driven Learning and Backjumping.

When an assignment triggers a logical contradiction, the solver analyzes the root cause via an implication graph to derive a globally validlearned clause. It then executes a non-chronologicalbackjumpto the deepest decision level where the learned clause becomes a unit, permanently pruning the invalid search space.

Restarts and Database Management.

To escape local minima and heavy-tailed runtime distributions, the solver periodically flushes its active assignment stack (the trail) and returns to the root level. Crucially, it preserves its cached variable phases, heuristic scores, and highly active learned clauses during a restart. To prevent memory bloat, it concurrently purges low-utility learned clauses.

2.3G-RRM: Guiding Symbolic Solvers with Recurrent Reasoning Models

2.3.1General Strategy

We propose G-RRM, a framework that couples recurrent reasoning models with symbolic solvers through search guidance (FigureLABEL:fig:comparison_NBRRM). We instantiate the recurrent model as an SE-RRM, trained on pairs of partially filled Sudoku grids and their corresponding solutions.

At inference time, SE-RRM assigns a score to each variable–value pair, yielding a matrix𝐘^∈ℝI×K\hat{\mathbf{Y}}\in\mathbb{R}^{I\times K}, where𝐘^i,d\hat{\mathbf{Y}}_{i,d}reflects the model’s preference for assigning valueddto variableii. For each variableii, these scores define a permutation

πi=\argsortd∈{1,…,K}​𝐘^i,d,\pi_{i}=\argsort_{d\in\{{1,\dots,K}\}}\hat{\mathbf{Y}}_{i,d},(1)where\argsort\argsortreturns indices in ascending order of the scores, i.e., from lowest to highest value. The most preferred value for a variableiiis therefore given by the last element of the permutation,di∗=πi​(K)d_{i}^{*}=\pi_{i}(K).

The resulting ordering guides a downstream symbolic solver during search by prioritizing candidate values in decreasing order of their SE-RRM scores, thereby affecting variable selection, branching decisions, or the order of candidate exploration.

When SE-RRM predictions are accurate, the solver can reach a solution with little or no additional search, effectively reducing the process to a sequence of decisions that can be verified efficiently. When predictions are imperfect, they still bias the search towards promising regions of the search space, while the solver explores alternatives as needed.

Importantly, G-RRM does not restrict the search space; it only determines the order of exploration while preserving all feasible assignments. Consequently, correctness and completeness of the underlying symbolic solver remain unchanged, and improvements arise solely from more efficient search ordering.

Because neural guidance influences only the direction of branching decisions, its efficacy depends on both the instance and the solver architecture. G-RRM can yield substantial benefits on search-dominated instances where decision-tree exploration forms the primary bottleneck, such as in backtracking andglucose4. However, these gains can be masked in solvers with high structural or startup overhead, such ascadical3, where initial startup costs persist independently of conflict reduction.

2.3.2G-RRM for Backtracking

The efficiency of backtracking strongly depends on the order in which cells and digits are explored. Good exploration directly reduces the size of the search tree and leads to faster solution times. Our approach combines a classical cell-selection heuristic with neural guidance for digit selection. We use backtracking as the simplest example of G-RRM, making the improvements more pronounced, as the efficiency of backtracking is directly tied to the explored search space.

Cell Selection Heuristic.

At each step, the algorithm must choose one of the remaining empty cells. To reduce the size of the search tree, we select the cell with the fewest valid candidate digits. This is the well-known minimum remaining values heuristic and helps expose contradictions early, often reducing the amount of search required to solve the puzzle.

Digit Selection through Neural Guidance.

After selecting a cell, the algorithm must decide in which order its valid candidate digits should be explored. Classical backtracking implementations typically use a fixed ordering. Instead, we use the predictions of a trained SE-RRM to guide this decision.

2.3.3G-RRM for CDCL SAT Solvers

Neural guidance in CDCL solvers attaches to the phase selection: at each decision point, the solver chooses an unassigned variable together with a polarity (True or False) to try first. This choice determines which region of the search space the solver explores before any conflict is encountered. Correct phase assignment eliminates backtracking entirely; wrong assignment forces the solver to discover and escape an infeasible subspace before recovering. We exploit solver control over this heuristic by initializing phases from SE-RRM predictions before search begins by setting variable phases from the highest-scored digitdi∗d_{i}^{*}. The Boolean variablexri,ci,di∗x_{r_{i},c_{i},d_{i}^{*}}is initialized to 1, and the variablesxri,ci,dx_{r_{i},c_{i},d}are initialized as 0 for alld≠di∗d\neq d_{i}^{*}. Because SE-RRM suggests full solution proposals over all grid cells simultaneously, we map the network’s high-confidence predictions directly onto the initial Boolean polarities (phases) of the CNF variables. When the model’s hints are highly accurate, the solver can traverse a valid path to the solution with zero or minimal conflicts. The normal configuration omits this step, relying solely on the solver’s built-in heuristics.

We leverage two popular CDCL solvers to evaluate how they interact with this neural phase guidance:glucose4andcadical3. Crucially, these solvers manage phase initialization and internal recovery differently when external hints conflict with the underlying logic:

• •cadical3: This solver strictly honors externally set literal phases. Provided phases persist across restarts, forcing the solver to consistently prioritize the externally injected search direction unless explicitly overridden by hard learned clause constraints.
• •glucose4: This solver adopts a more fluid approach and may override initial external phases on restart via its native VSIDS-driven reinitialization mechanism. This design yields a significantly faster self-correction loop, allowing the solver to rapidly recover and diverge from faulty hints directing the search into an infeasible subspace.

3Experimental Evaluation

In this section, we evaluate G-RRM by benchmarking different solvers’ default configurations against their SE-RRM–guided variants to quantify the impact of neural guidance on solver efficiency for Sudoku puzzles of different sizes. For training details of the SE-RRM, see\appendixrefapp:trDetails. Additional CP-SAT experiments are located in\appendixrefapp:cpsat.

Because reduced conflicts directly lead to runtime savings for search‑dominated solvers, we quantify the efficiency of G-RRM via changes in conflict counts alongside wall‑clock time (see\tablereftab:sat_conflicts_full and\tablereftab:sat_timing_full). In addition, we report the fully‑solved rate (FSR), which denotes the fraction of Sudoku instances that SE-RRM immediately predicts correctly, for each benchmarked grid size.

For the SAT solvers, we interface withglucose4andcadical3via thePySATPython library(pysat2018;pysat2024), integrating the neural outputs directly into the solver via phase initialization. For the wall‑clock time experiments, we separately evaluate the advantage of neural guidance for cases with perfect neural predictions and for cases where the predictions contain errors. We do not aim to directly compare the performance of backtracking and the CDCL solvers, as we use a custom Python implementation of backtracking. Rather, we compare thenormalandguidedversion of each solver.

Conflict Counts (Table1).

Table 1:Conflict count percentiles (Normal vs. Guided) across grid sizes and solvers. Bold marks the best value at each percentile. Backtracking conflicts denote DFS search dead-ends and are not directly comparable in magnitude to CDCL conflicts.- aStandard backtracking is too inefficient to solve puzzles larger than9×99\times 9.

• bIn this work, we use a different set of9×99\times 9puzzles than the authors of SE-RRM, which explains the slightly lower fully-solved rate on9×99\times 9Sudokus compared tofreinschlag2026symbol.

Neural guidance tends to reduce conflict counts most consistently at the median: on9×99\times 9, it drives the median (and p90) to zero across solvers, reflecting the instances perfectly solved by the SE-RRM. On16×1616\times 16and25×2525\times 25, it collapses or markedly lowers the median (e.g.,−53.2%-53.2\%for glucose4 and−22.1%-22.1\%for cadical3 at16×1616\times 16; zero median at25×2525\times 25), with smaller or mixed effects in the upper tail. These conflict reductions do not necessarily translate into significant wall-clock speedups, presumably because runtime is not search-dominated.

Wall-Clock Time (Table2).

Table 2:Wall-clock solve times (ms) of normal and guided SAT solvers across all grid sizes. Speedup > 1 indicates that neural guidance reduces solve time. Significance of each speedup is from a paired test on per-instance solve times across the test set (Wilcoxon signed-rank for Median rows; paired t-test for Mean rows): *** p<0.001, ** p<0.01, * p<0.05, n.s. = not significant. Seeds were collapsed per instance (mean over 3 runs) before aggregation. Note that the significance for the Median rows is more relevant, as the t-test on Mean rows is less informative due to the heavy-tailed distributions.- aStandard backtracking is too inefficient to solve puzzles larger than9×99\times 9.

Backtracking shows large, statistically significant speedups on all puzzles and perfect puzzles (33.251×\mathbf{33.251}\!\timesand30.101×\mathbf{30.101}\!\timesrespectively) in9×99\times 9, as reduced conflicts directly lead to faster runtime. On imperfect solutions, the results are mixed and not significant.

glucose4consistently converts conflict savings into statistically significant wall-clock speedups:1.699×\mathbf{1.699}\!\timesoverall and1.666×\mathbf{1.666}\!\timeson perfect-hint instances at9×99{\times}9, with perfect-hint speedups of2.204×\mathbf{2.204}\!\timesand1.169×\mathbf{1.169}\!\timesat16×1616{\times}16and25×2525{\times}25, respectively. Speedups on all puzzles and imperfect hints for16×1616\times 16and25×2525\times 25are mostly non-significant, only reaching moderate significance on all puzzles for25×2525\times 25. The diminishing returns at larger scales reflect a growing share of solve time spent outside the search.

cadical3shows no consistent wall-clock benefit and provides the only statistically significant slowdown using G-RRM. The solver is overhead-dominated: its internal bookkeeping is largely independent of conflict count, so eliminating conflicts does not proportionally reduce runtime. On9×99{\times}9, phase initialization adds∼1.7{\sim}1.7ms on instancescadical3would have solved trivially, producing a0.896×0.896\!\timesaggregate mean. On the more reliable median,cadical3shows no significant change (1.021×1.021\!\times, n.s.); the only significant effect is a small mean slowdown attributable to fixed phase-initialization overhead. On16×1616\times 16and25×2525{\times}25, search accounts for a tiny fraction of the solve budget, leaving guidance as a non-significant, near-zero impact.

4Conclusion

We propose G-RRM, a neuro-symbolic framework in which a symbol-equivariant recurrent reasoning model (SE-RRM) guides the search of exact symbolic solvers. The neural model provides probabilistic preferences over candidate assignments from a single forward pass, while a symbolic solver enforces global constraints and guarantees correctness. This combination reduces the effective search space compared to only using a solver and still retains the completeness of the symbolic algorithm; improvements arise from more efficient search. In essence, G-RRM converts a high-accuracy but unverified neural solver into one with guaranteed correctness.

The central question of this work is under what conditions G-RRM reduces search cost. Our results show that reductions in search cost are strongly tied to the solver architecture and the instance-level correctness of the neural model. On perfect-hint instances, guidance resolves puzzles with zero conflicts across all grid sizes and solvers. For the search-dominated backtracking andglucose4, this translates into statistically significant wall-clock speedups in all cases. For the overhead-dominatedcadical3it does not, as its runtime is largely independent of conflict count. On imperfect-hint instances, the outcome depends on solver architecture and hint quality. Although we see slight speedups in some instances, e.g., a1.069×1.069\!\timesspeedup in mean time for backtracking on9×99\times 9, no result is statistically significant. This can be explained by the confidence of the SE-RRM: independent of being correct in its assignments, the majority of predictions strongly favor one option. When the model is confidently incorrect, it leads the search towards incorrect paths, which cancel the speedup of promising directions.

5Limitations

Our evaluation isolates the effect of neural guidance, which introduces some limitations to the results.

First, all reported wall‑clock times refer to the symbolic solver. Inference time for SE‑RRM is not included, as it was precomputed separately. Incorporating inference time would entangle batch size, GPU hardware, and implementation‑specific optimizations, making comparisons difficult. Our objective in this work is to isolate the impact of neural guidance itself, rather than to maximize engineering performance. Accordingly, our SE‑RRM implementation is a straightforward research prototype and does not exploit the full range of possible performance optimizations.

Second, our study is confined to Sudoku. While Sudoku is an established combinatorial benchmark, we do not confirm our results on other domains.

6Future Work

Beyond Sudoku, G-RRM suggests a general strategy for combinatorial problems whose symbolic search cost grows exponentially with size. We call itSolve–Learn–Extrapolate (SLE): (i)solvesmall instances exactly with a symbolic solver, (ii)learnan SE-RRM on these valid solutions, and (iii)extrapolateto larger instances, where SE-RRM hints guide the solver through the search space. Since G-RRM preserves completeness, new solutions are valid and can be fed back to re-train the SE-RRM before advancing to the next size, lifting the frontier of tractable sizes using only valid data. Our experiments realize a first step of this loop: the SE-RRM trained on9×99\times 9Sudokus and fine-tuned on a small number of larger grids (AppendixB) produces hints that guide solvers on16×1616\times 16and25×2525\times 25instances, demonstrating SLE in miniature. Assessing SLE on harder problem families is a promising direction for future work.

Acknowledgements

The ELLIS Unit Linz, the LIT AI Lab, the Institute for Machine Learning, are supported by the Federal State Upper Austria. We thank the projects FWF AIRI FG 9-N (10.55776/FG9), AI4GreenHeatingGrids (FFG-899943), Stars4Waters (HORIZON-CL6-2021-CLIMATE-01-01), FWF Bilateral Artificial Intelligence (10.55776/COE12). We thank NXAI GmbH, Audi AG, Merck Healthcare KGaA, GLS (Univ. Waterloo), TÜV Holding GmbH, Software Competence Center Hagenberg GmbH, dSPACE GmbH, TRUMPF SE + Co. KG.

References

Appendix ARecurrent Reasoning Models

\floatconts

fig:rrm

Figure 2:Principle designs of Recurrent Reasoning Models (Source:freinschlag2026symbol).Left:HRM/TRM compared to SE-RRM which introduces an explicit symbol dimension that enables permutation equivariance over symbols and allows for problem size extrapolation.Right:Permutation equivariance explained.### A.1Recurrent Reasoning Models: Fixed-Point Iteration with Deep Supervision

Recurrent reasoning models (RRMs) perform iterative refinement via a fixed-point iteration on a recurrent state. An overview of our notation is shown in Table3. Let𝒁t∈ℝD×I\bm{Z}^{t}\in\mathbb{R}^{D\times I}denote the recurrent state at iterationtt, whereDDis the feature dimension. An input embeddingEℋE^{\mathcal{H}}maps the symbolic instance into the same shape,Eℋ​(𝑿)∈ℝD×I,E^{\mathcal{H}}(\bm{X})\in\mathbb{R}^{D\times I},typically as a sum of a symbol embedding and a positional encoding.

AnRRM blockℋ\mathcal{H}is a mappingℋ:ℝD×I×ℝD×I→ℝD×I,\mathcal{H}:\mathbb{R}^{D\times I}\times\mathbb{R}^{D\times I}\to\mathbb{R}^{D\times I},which updates the state𝒁\bm{Z}as

𝒁t+1=ℋ​(Eℋ​(𝑿),𝒁t),\displaystyle\bm{Z}^{t+1}=\mathcal{H}\left(E^{\mathcal{H}}(\bm{X}),\bm{Z}^{t}\right),(2)where𝒁0\bm{Z}^{0}is a learned initial state.

Variants of the RRM block may omit the input embedding at some steps or inject a previous recurrent state𝒁t−rp​r​e​v\bm{Z}^{t-r_{prev}}(withrp​r​e​vr_{prev}being a hyperparameter). We capture this by

𝒁t+1=ℋ​(1emb​Eℋ​(𝑿)+1prev​𝒁t−rp​r​e​v,𝒁t),\displaystyle\bm{Z}^{t+1}=\mathcal{H}\left(1_{\text{emb}}E^{\mathcal{H}}(\bm{X})+1_{\text{prev}}\bm{Z}^{t-r_{prev}},\bm{Z}^{t}\right),(3)for intermediate layers (witht−rp​r​e​v​\geqslant​0t-r_{prev}\geqslant 0), where1emb,1prev∈{0,1}1_{\text{emb}},1_{\text{prev}}\in\{0,1\}denote whether the respective input is used (can be arbitrarily set and therefore define the design of the neural fixed-point architecture).

Transformer-Style RRM Block.

Following HRM/TRM-style designs, one RRM block consists ofLLstacked Transformer-style layers. Let

𝑯0:=1emb​Eℋ​(𝑿)+1prev​𝒁t−rp​r​e​v+𝒁t.\displaystyle\bm{H}_{0}:=1_{\text{emb}}E^{\mathcal{H}}(\bm{X})+1_{\text{prev}}\bm{Z}^{t-r_{prev}}+\bm{Z}^{t}.(4)Forl=0,…,L−1l=0,\dots,L-1, the update is

𝑯l′\displaystyle\bm{H}^{\prime}_{l}=Norm​(𝑯l+TD,I​(𝑯l)),\displaystyle=\text{Norm}\left(\bm{H}_{l}+T^{D,I}(\bm{H}_{l})\right),D¯×I¯\displaystyle\underline{D}\times\underline{I}(5)𝑯l+1\displaystyle\bm{H}_{l+1}=Norm​(𝑯l′+mD​(𝑯l′)),\displaystyle=\text{Norm}\!\left(\bm{H}^{\prime}_{l}+m^{D}(\bm{H}^{\prime}_{l})\right),D¯×I,\displaystyle\underline{D}\times I,(6)and the block output is𝒁t+1=𝑯L\bm{Z}^{t+1}=\bm{H}_{L}. HereTD,IT^{D,I}denotes self-attention along the position dimension andmDm^{D}is a position-wise MLP (e.g., SwiGLU), whileNormdenotes RMSNorm, applied token-wise. In above equations, we tried to indicate the attention axes or axes used as features to neural operations with an underscore, while the neural operation operates independently on the other axes.

Output Mapping and Training with Deep Supervision.

RRMs predict symbol distributions per position by mapping𝒁t\bm{Z}^{t}to logits𝒀^t∈ℝI×K\hat{\bm{Y}}^{t}\in\mathbb{R}^{I\times K}using an output head𝑶\bm{O}(typically linear inDD), followed by a softmax over theKKsymbols. Training uses deep supervision: losses (categorical cross-entropy) are applied to selected intermediate predictions, and gradients are truncated/detached across iteration segments.

A.2Limitation: Lack of Symbol Extrapolation in Vanilla RRMs

Vanilla RRMs encode symbols via a learned embedding tableΣ→ℝD\Sigma\to\mathbb{R}^{D}insideEℋE^{\mathcal{H}}. As a consequence, permuting symbols in the input can lead to differing results in the output. It also disallows the application to instances with unseen symbolsΣ′⊃Σ\Sigma^{\prime}\supset\Sigma(i.e.,|Σ′|>K|\Sigma^{\prime}|>K), because new symbols require new embeddings. This is particularly restrictive for extrapolation across Sudoku sizes, where the alphabet grows with the grid (e.g., from digits1:91:9to1:161:16or1:251:25).

Data Augmentation.

Previous methods combat this issue by augmenting the training data with symbol-permuted samples. While this can diminish performance inconsistencies, it requires additional computation due to the increased training data. Crucially, it still prevents extrapolation to unseen symbols.

Symbol-Axis Embedding.

Conceptually, for each positioniiand each symbolc∈Σc\in\Sigma, SE-RRM stores whetherxi=cx_{i}=calong the symbol axis using a shared embedding vector for all usual symbols plus dedicated embeddings for special tokens such as mask/unknown, and zeros otherwise. This yields a tensorE𝒞​(𝑿)∈ℝD×I×KE^{\mathcal{C}}(\bm{X})\in\mathbb{R}^{D\times I\times K}that can be augmented with positional and (optionally) task-type information,E𝒢:=E𝒞+E𝒫+E𝒯.E^{\mathcal{G}}:=E^{\mathcal{C}}+E^{\mathcal{P}}+E^{\mathcal{T}}.

SE-RRM Fixed-Point Update.

SE-RRM uses the same fixed-point structure but with a block𝒢:ℝD×I×K×ℝD×I×K→ℝD×I×K,\mathcal{G}:\mathbb{R}^{D\times I\times K}\times\mathbb{R}^{D\times I\times K}\to\mathbb{R}^{D\times I\times K},and

𝒁¯t+1=𝒢​(1emb​E𝒢​(𝑿)+1prev​𝒁¯t−rp​r​e​v,𝒁¯t).\displaystyle\bar{\bm{Z}}^{t+1}=\mathcal{G}\left(1_{\text{emb}}E^{\mathcal{G}}(\bm{X})+1_{\text{prev}}\bar{\bm{Z}}^{t-r_{prev}},\,\bar{\bm{Z}}^{t}\right).(7)

SE-RRM Block Architecture with Axial Attention over Positions and Symbols.

Let𝑯0\bm{H}_{0}be defined analogously to (4), but inℝD×I×K\mathbb{R}^{D\times I\times K}. Forl=0,…,L−1l=0,\dots,L-1, SE-RRM applies two attention layers: first along positions, then along symbols, followed by a token-wise MLP:

𝑯l′\displaystyle\bm{H}^{\prime}_{l}=Norm​(𝑯l+TD,I​(𝑯l)),\displaystyle=\text{Norm}\left(\bm{H}_{l}+T^{D,I}(\bm{H}_{l})\right),D¯×I¯×K\displaystyle\underline{D}\times\underline{I}\times K(8)𝑯l′′\displaystyle\bm{H}^{\prime\prime}_{l}=Norm​(𝑯l′+TD,K​(𝑯l′)),\displaystyle=\text{Norm}\left(\bm{H}^{\prime}_{l}+T^{D,K}(\bm{H}^{\prime}_{l})\right),D¯×I×K¯\displaystyle\underline{D}\times I\times\underline{K}(9)𝑯l+1\displaystyle\bm{H}_{l+1}=Norm​(𝑯l′′+mD​(𝑯l′′)),\displaystyle=\text{Norm}\left(\bm{H}^{\prime\prime}_{l}+m^{D}(\bm{H}^{\prime\prime}_{l})\right),\/D¯×I×K,\displaystyle\underline{D}\times I\times K,(10)and𝒁t+1=𝑯L\bm{Z}^{t+1}=\bm{H}_{L}. Attention along the position and the MLP are uniform across the symbol axis and therefore do not break equivariance. Attention along the symbol dimension is itself permutation-equivariant. Therefore, equivariance is preserved, unless it is explicitly broken via task-type embeddings.

Output Head.

SE-RRM projects eachDD-dimensional feature vector of𝒁t\bm{Z}^{t}(for every position–symbol pair(i,k)(i,k)) to a scalar logit, producing an output tensor inℝ1×I×K≅ℝI×K\mathbb{R}^{1\times I\times K}\cong\mathbb{R}^{I\times K}. Categorical probabilities per position are then computed as in vanilla RRMs.

Table 3:Notation used throughout the paper (RRMs/SE-RRMs, SAT solving, and G-RRM).DefinitionSymbolTypeScalars and indicesgrid dimension (Sudoku isN×NN\times N)NNℕ\mathbb{N}feature dimensionDDℕ\mathbb{N}number of positions/cellsIIℕ\mathbb{N}position / cell indexii{1,…,I}\{1,\ldots,I\}number of symbolsKKℕ\mathbb{N}symbol (channel) indexkk{1,…,K}\{1,\ldots,K\}recurrent iteration index (RRM/SE-RRM)ttℕ\mathbb{N}previous-state offset (recurrence hyperparameter)rprevr_{\text{prev}}ℕ\mathbb{N}number of layers per blockLLℕ\mathbb{N}layer index within a blockll{0,…,L−1}\{0,\ldots,L-1\}SATcell row, column, and value indicesr,c,vr,c,v{1,…,N}\{1,\ldots,N\}SAT variable: cell(r,c)(r,c)holds valuevvxr,c,vx_{r,c,v}{0,1}\{0,1\}per-variable value ordering (arg sort of scores)πi\pi_{i}permutation of{1,…,K}\{1,\ldots,K\}value index / most-preferred value for variableiid,di∗d,\,d^{*}_{i}{1,…,K}\{1,\ldots,K\}second value index (At-Most-One clauses)ww{1,…,N}\{1,\ldots,N\}Sets and spacessymbol alphabet (neural sections; may include mask)Σ\Sigmafinite set,|Σ|=K|\Sigma|=Kextended symbol alphabet (unseen symbols)Σ′\Sigma^{\prime}Σ′⊃Σ,|Σ′|>K\Sigma^{\prime}\supset\Sigma,\ |\Sigma^{\prime}|>Kinput/solution space (neural)ΣI\Sigma^{I}tuples of symbolsTasks, solutions, and assignmentsinput task (neural encoding)𝑿=(x1,…,xI)\bm{X}=(x_{1},\ldots,x_{I})ΣI\Sigma^{I}solution task (neural target)𝒀=(y1,…,yI)\bm{Y}=(y_{1},\ldots,y_{I})ΣI\Sigma^{I}symbol at positioniixi,yix_{i},\,y_{i}Σ\SigmaEmbeddings and representations (neural)RRM task embedding matrixEℋ​(𝑿)E^{\mathcal{H}}(\bm{X})ΣI↦ℝD×I\Sigma^{I}\mapsto\mathbb{R}^{D\times I}SE-RRM symbol-axis embedding tensorE𝒞​(𝑿)E^{\mathcal{C}}(\bm{X})ΣI↦ℝD×I×K\Sigma^{I}\mapsto\mathbb{R}^{D\times I\times K}SE-RRM task embedding tensorE𝒢​(𝑿)E^{\mathcal{G}}(\bm{X})ΣI↦ℝD×I×K\Sigma^{I}\mapsto\mathbb{R}^{D\times I\times K}positional embeddingE𝒫E^{\mathcal{P}}ℝD×I×K\mathbb{R}^{D\times I\times K}task-type embeddingE𝒯E^{\mathcal{T}}ℝD×I×K\mathbb{R}^{D\times I\times K}recurrent state at steptt(RRM)𝒁t\bm{Z}^{t}ℝD×I\mathbb{R}^{D\times I}recurrent state at steptt(SE-RRM)𝒁¯t\bar{\bm{Z}}^{t}ℝD×I×K\mathbb{R}^{D\times I\times K}learned initial state𝒁0\bm{Z}^{0}ℝD×I\mathbb{R}^{D\times I}intermediate block states𝑯l,𝑯l′,𝑯l′′\bm{H}_{l},\bm{H}^{\prime}_{l},\bm{H}^{\prime\prime}_{l}ℝD×I\mathbb{R}^{D\times I}orℝD×I×K\mathbb{R}^{D\times I\times K}Models and blocks (neural)RRM block (HRM/TRM)ℋ\mathcal{H}ℝD×I×ℝD×I→ℝD×I\mathbb{R}^{D\times I}\times\mathbb{R}^{D\times I}\to\mathbb{R}^{D\times I}SE-RRM block𝒢\mathcal{G}ℝD×I×K×ℝD×I×K→ℝD×I×K\mathbb{R}^{D\times I\times K}\times\mathbb{R}^{D\times I\times K}\to\mathbb{R}^{D\times I\times K}output head𝒪\mathcal{O}ℝD→ℝK\mathbb{R}^{D}\to\mathbb{R}^{K}embedding inclusion indicator𝟏emb\mathbf{1}_{\text{emb}}{0,1}\{0,1\}previous-state inclusion indicator𝟏prev\mathbf{1}_{\text{prev}}{0,1}\{0,1\}Neural operatorsself-attention over positionsTD,IT^{D,I}ℝD×I→ℝD×I\mathbb{R}^{D\times I}\to\mathbb{R}^{D\times I}self-attention over symbolsTD,KT^{D,K}ℝD×K→ℝD×K\mathbb{R}^{D\times K}\to\mathbb{R}^{D\times K}MLP over features (SwiGLU)mDm^{D}ℝD→ℝD\mathbb{R}^{D}\to\mathbb{R}^{D}normalization (RMSNorm)Norm\mathrm{Norm}ℝD→ℝD\mathbb{R}^{D}\to\mathbb{R}^{D}Predictionlogits produced by the RRM backbone (single forward pass)𝐘^\hat{\mathbf{Y}}ℝI×K\mathbb{R}^{I\times K}logits at RRM iterationtt𝒀^t\hat{\bm{Y}}^{t}ℝI×K\mathbb{R}^{I\times K}score for assigning valueddto variableiiY^i,d\hat{Y}_{i,d}ℝ\mathbb{R}

Appendix BSE-RRM Model Training Details

Data.

We use Sudoku puzzles of differing sizes to compare methods across problem specifications. For standard9×99\times 9Sudokus, we use the same data asfreinschlag2026symbol: 1,000 samples provided bywang2025hierarchicalto train the neural models and 1,000 test samples. The16×1616\times 16and25×2525\times 25data comprises 100 training samples for fine-tuning and 100 and 90 test samples, respectively, which are created withpy-sudoku. The average rate of empty cells differs per dataset,9×99\times 9,16×1616\times 16, and25×2525\times 25Sudokus have68.88%68.88\%,63.49%63.49\%, and50.08%50.08\%empty cells, respectively.

Training Details.

We train an SE-RRM model initially on9×99\times 9Sudokus. We then fine-tuned it further for the16×1616\times 16and25×2525\times 25grids with 100 samples using a decreased learning rate and increased regularization.

Appendix CCP-SAT Experiments

To confirm findings from our main experiments, we provide additional experiments using the state-of-the-art constraint programming solver CP-SAT(perron2023cp).

We compare four configurations designed to evaluate different levels of neural-symbolic coupling:

Table 4:Tested CP-SAT solver configurationsAll four configurations share the same underlying CP-SAT base model, enforcingN×NN\times NSudoku constraints (AllDifferent constraints across all rows, columns, and subgrids). To isolate the impact of search guidance and ensure reproducibility, all configurations are restricted to a single worker thread and a fixed random seed.

The configurations are defined as follows:

• •C1 (Default CP-SAT)functions as the primary symbolic baseline, utilizing the solver’s default configuration.
• •C2 (Naive Fixed)represents a blind symbolic baseline. It enforces a fixed search strategy that branches on the variable with the minimum domain size and selects the minimum value first. This matches the branching heuristics of the naive backtracking analyzed in Section2.2.1, while retaining CP-SAT’s propagation and conflict-driven clause learning.
• •C3 (Soft Hint)warm-starts CP-SAT with the SE-RRM’s argmax predictions viamodel.AddHint. If the hints are globally consistent, the solver completes in the hint phase with zero conflicts; when a conflict arises, it continues following the hints for up to the default budget (hint_conflict_limit = 10), using each conflict to learn which hint values are wrong, before discarding the hints and falling back to automatic search.
• •C4 (Repaired Hint)uses the same hints withrepair_hint = True: rather than discarding on conflict, the solver runs a propagation-based local search that adjusts only the inconsistent cells while preserving the rest. A successful repair yields zero conflict-driven clause learning backtracking; a larger budget (hint_conflict_limit = 100) funds this process.

The performance of these configurations across different grid sizes is presented in Table5.

Table 5:CP-SAT performance across different constraint configurations. Lower values are better.The results are best understood throughhint feasibility: during presolve, CP-SAT classifies the SE-RRM hint set as either feasible—the predictions form a globally consistent assignment, allowing the solver to complete in the hint phase with zero branching—or infeasible, requiring repair or general search. On feasible instances, C3 and C4 are equivalent; they diverge only on infeasible ones.

1. 1.Conflict Reduction at Low Density:For9×99\times 9grids (clue density≈31.3%\approx 31.3\%), conflict counts are right-skewed: propagation resolves most instances, while a hard tail drives the mean. C2’s28.128.1mean conflicts already reflect CP-SAT’s full conflict-driven clause learning—C2 is a blindbranching heuristic, not a blind solver. C4 achieves0.00.0mean conflicts: the91.1%91.1\%feasible instances complete in the hint phase, and all remaining infeasible instances are fully repaired within the 100-conflict budget. C3 reduces mean conflicts by83%83\%(4.74.7vs.28.128.1): on infeasible instances, it follows wrong hints for up to 10 conflicts—building clause knowledge from each failure—before handing off to conflict-driven clause learning.
2. 2.Propagation-Dominated Regimes at Scale:At25×2525\times 25(clue density≈49.9%\approx 49.9\%), propagation resolves92.2%92.2\%of instances under C2 with zero conflicts, leaving little room for any branching heuristic to influence outcomes. Mean conflict counts collapse across all configurations. Notably, C3 performs worse than the blind C2 baseline (6.06.0vs.3.93.9): incorrect hints add overhead to otherwise near-trivial solves. C4 beats C2 by a negligible margin (3.83.8vs.3.93.9). This illustrates a fundamental limit of hint-based guidance: when propagation already resolves most of the search space, the branching heuristic has little opportunity to contribute, and incorrect hints are a net cost.
3. 3.Wall-Clock Time and Overhead:C3 consistently reduces wall-clock time relative to C2:1.9×1.9\timeson9×99\times 9(0.00660.0066s vs.0.01220.0122s),1.2×1.2\timeson16×1616\times 16(0.03120.0312s vs.0.03660.0366s), and1.2×1.2\timeson25×2525\times 25(0.04090.0409s vs.0.04910.0491s). C1’s automatic portfolio heuristics remain faster than C3 at all scales. C4 minimizes conflicts across all grid sizes but incurs substantial overhead at16×1616\times 16(0.09710.0971s vs.0.02370.0237s for C1): with only22.0%22.0\%of hint sets feasible, the repair budget is frequently exhausted before a consistent assignment is found, forcing costly fallback to general search.