arXiv:2607.02491cs.AI2026-07

用神经推理模型指导符号求解器,显著加速约束满足问题求解。

G-RRM: Guiding Symbolic Solvers with Recurrent Reasoning Models

  • 将符号等变神经模型与传统求解器结合,由神经模型生成解的初步建议。
  • 在9×9数独上使回溯法提速33.3倍,葡萄糖求解器提速1.70倍(中位数)。
  • 适用于搜索空间大且支持动态修正分支策略的问题,适合优化求解场景。

本文聚焦于符号等变的递归推理模型(SE-RRMs),其在更大规模问题上表现出更强的外推能力。我们提出一种神经符号方法——‘引导式递归推理模型’(G-RRM),将SE-RRMs与符号求解器(如回溯法、Glucose 4.1、CaDiCaL 3.0.0)结合,由神经模型生成完整解提案并引导经典求解器获得全局正确解。实验表明,当问题具有广阔的组合搜索空间,且求解器可动态覆盖分支选择时,神经引导能显著提升效率:在9×9数独上,SE-RRM正确解出91.1%实例,回溯法中位冲突数降为零,提速33.3倍;Glucose 4.1提速1.70倍(中位数,p<0.001),在完美提示的25×25网格仍保持1.17倍加速。而始终遵循提示且运行时开销主导的CaDiCaL 3.0.0未见显著加速(中位数1.02倍,不显著),甚至在9×9上出现显著平均减速(0.90倍)。结果明确了神经引导实现实际加速的条件边界。

原文摘要 · Abstract (English)

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: on $9\times9$ Sudoku, where the SE-RRM correctly solves $91.1\%$ of instances, backtracking accelerates by $33.3\times$ and Glucose 4.1 by $1.70\times$ (median, $p<0.001$), with Glucose 4.1 retaining a $1.17\times$ speedup on perfect-hint $25\times25$ grids. 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 (median $1.02\times$, n.s.) and even a small significant mean slowdown ($0.90\times$) on $9\times9$. These results delineate the regimes in which neural guidance translates into practical speedups.

神经符号求解器加速约束满足

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。