Learning from Algorithm Feedback: One-Shot SAT Solver Guidance with GNNs
Authors: Jan Tönshoff
Martin Grohe
Venue: ICLR 2026 Poster (2026)
Keywords: Reinforcement Learning
Graph Neural Networks
Combinatorial Optimization
SAT Solving
GNNs
Graph Learning
GRPO
Primary area: reinforcement learning
TL;DR: GNNs + guided SAT solvers + GRPO = faster, data-driven SAT solvers

Abstract: Boolean Satisfiability (SAT) solvers are foundational to computer science, yet their performance typically hinges on hand-crafted heuristics. This work introduces Reinforcement Learning from Algorithm Feedback (RLAF) as a paradigm for learning to guide SAT solver branching heuristics with Graph Neural Networks (GNNs). Central to our approach is a novel and generic mechanism for injecting inferred variable weights and polarities into the branching heuristics of existing SAT solvers. In a single forward pass, a GNN assigns these parameters to all variables. Casting this one-shot guidance as a reinforcement learning problem lets us train the GNN with off-the-shelf policy-gradient methods, such as GRPO, directly using the solver's computational cost as the sole reward signal. Extensive evaluations demonstrate that RLAF-trained policies significantly reduce the mean solve times of different base solvers across diverse SAT problem distributions, achieving more than a 2x speedup in some cases, while generalizing effectively to larger and harder problems after training. Notably, these policies consistently outperform expert-supervised approaches based on learning handcrafted weighting heuristics, offering a promising path towards data-driven heuristic design in combinatorial optimization.

Published as a conference paper at ICLR 2026
LEARNING FROM ALGORITHM FEEDBACK: ONE-SHOT SAT SOLVER GUIDANCE WITH GNNS
Jan Tönshoff RWTH Aachen University
Martin Grohe RWTH Aachen University
ABSTRACT
Boolean Satisfiability (SAT) solvers are foundational to computer science, yet their performance typically hinges on hand-crafted heuristics. This work introduces Reinforcement Learning from Algorithm Feedback (RLAF) as a paradigm for learning to guide SAT solver branching heuristics with Graph Neural Networks (GNNs). Central to our approach is novel and generic mechanism for injecting inferred variable weights and polarities into the branching heuristics of existing SAT solvers. In a single forward pass, a GNN assigns these parameters to all variables. Casting this one-shot guidance as a reinforcement learning problem lets us train the GNN with off-the-shed policy-gradient methods, such GRPO, directly using the solver's ' computational cost as the sole reward signal. Extensive evaluations demonstrate that RLAF-traine'' policies significantly reduce the mean solve times of different base solvers across diverse SAT problem distributions, achieving more than 2x speedup in some cases, while generalizing effectively to larger and harder problems after training. Notably, these policies consistently outperform expert-supervised approaches based on learning handcrafted weighting heuristics, offering a promising path towards data-driven heuristic design in combinatorial optimization.
INTRODUCTION
Solving computationally hard combinatorial problems, such as Boolean satisfiability (SAT), remains a cornerstone of computer science and critical to diverse domains such as verification, planning. and cryptography (Biere et al. 202T). Complete search algorithms are of particular importance, as they are guaranteed to find a solution if one exists or prove unsatisfiability otherwise. The runtime of these classical algorithms heavily depends hand-crafted heuristics navigate the solution space, for example, by determining variable assignments during the search. Such heuristics are often rigid and hard to adapt to specific instance distributions without extensive expert knowledge and tuning. Machine learning offers a compelling alternative: Augmenting the heuristic components of classical search algorithms with trainable functions allows us to construct adaptable solvers. Specifically, reinforcement learning (RL) can train these extended solvers to learn improved, distribution-sspclie specific heuristies in data-driven manner without direct expert supervision.
In this work, we study how to leverage RL-trained Graph Neural Network (GNNs) to improve branching heuristics of SAT solvers. Our main contributions are as follows: First, we introduce novel and generic method for integrating variable-wise weights into the branching heuristics of existing SAT solvers. Secondly, we construct a GNN-based policy that assigns a weight and polarity to each variable in one forward pass. This one-shot setting enables single GNN pass influence every branching decision, avoiding costly repeat passes. Thirdly, we phrase the task of inferring weights and polarities that reduce the solver's cost an RL problem. The reward signal is directly obtained from the observed computational cost of the guided SAT solver, requiring no expert supervision. We refer to this training paradigm as Reinforcement Learning from Algorithm Feedback (RLAF). Finally, demonstrate empirically that modern RL techniques, such as GRPO (Shao et al. 2024). are capable of training effective RLAF policies for different base solvers. The learned policies substantially reduce solver runtimes, generalize to harder problems after training. outperform supervised baselines, and appear to capture solver agnossic structural properties of SAT problems.
"Correspondence toenshof F normatii wwthhaachen.de

---

Published as a conference paper at ICLR 2026
Algorithm 1 DPLL Solver
Algorithm 2 Decision Hcuristic
1: Input: Formula &
1: Input: Formula &
2:
function SOLVE(Ø)
2: function (ICK-LITERAL(O)
3:
# Simplify formula
3: 2 < argmax, SCORE(2)
4:
UNIE-PROPAAATION))))
4: return 2 if PICK-SIGN(E else -u
5: end function
6:
7:
if ④- = 0: return SAT
Algorithm 3 Guided Decision Heuristic
8:
if 0 d: return UNSAT
Input: Formula & Parameters W= (10, 2: function SICC-LLTTRAA-GLDDDDDE W)
10:
Decide next branching variable & PICK-L.TERAI...)
11:
3: 5. + argmax, an (c)
12:
return (OLVE(ÁA V SOLVE(ÓA
4: return è if (()) 1 else -
13:
end function
5: end function
Figure 1: DPLL SAT solver and branching heuristics. Algorithm A DPLL SAT solver performs backtracking search to solve a given CNF formula ø. At each search step, the formula is simplified through unit propagation and pure literal elimination before selecting the next branching literal. Algorithm 2 Branching heuristics are often implemented by choosing the variable that maximizes some hand-crafted scoring function. Algorithm We propose to extend existing branching heuristics by incorporating given variable weights into the branching decisions that scale the associated score of each variable. We additionally choose the sign of each literal according to provided polarity.
1.1 BACKGROUND
SAT Solving A Boolean formula in Conjunctive Normal Form (CNF) is a conjunction of clauses
==C1 A.... A Cm. each clause being disjunction of one more literals C (f,,1 V... fz,k). We denote by Var(ő) = = {.1..... In, the set of Boolean variables of ø. The Boolean SAT problem is to decide whether not there exists a satisfying assignment a Var(ø) + {0, 1} that satisfies all clauses of a given formula ø. This problem is well-known to be NP-complete and naturally arises in wide range of applications (Biere al. 202T). Modern SAT solvers predominantly stem from the (DPLL) algorithm, a backtracking search approach enhanced by unit propagation and pure literal climination. Algorithm [ provides pseudocode description of a DPLL SAT solver. Many extensions of this general idea have been proposed to scale SAT solvers larger, industrial instances. In particular, Conflict-Driven Clause Learning (CDCL) solvers significantly extend the DPLL framework by introducing clause learning and non -onnoooonllli backtracking. A common property DPLL-derived solvers is the importance of the branching heuristic that picks the next branching literal in each search step (line 11 in Algorithm [. Various branching heuristics have been proposed, and which heuristic performs best often depends on the structure of the given SAT formula (Kullmann] (02II. Customizing branching heuristics towards specific distribution of inputs generally requires expert knowledge and significant trial and error.
Reinforcement Learning Reinforcement learning (RL) aims to learn policies for sequential decision-making problems where an agent interacts with an environment to learn through trial and error. An RL problem is usually formalized defined as tuple (S, A, P, Rt), where S is the set of states, A is the set of possible actions, P denotes the transition probabilities between states and policies π are stochastic mappings from states to distributions over actions, i.c., π ((a)s) indicates the probability of selecting action a in state s. More generally, for continuous action spaces, i.e. A = IR, π {a]s) is the probability density that policy assigns to an action The primary objective in RL is to determine an optimal policy π that maximizes the expected cumulative discounted reward EE, -2: 7 R(ss, az)], where [0, 1) represents discount factor that emphasizes earlier rewards. This formulation is the basis for various RL algorithms. Recently, RL algorithms based on policy gradients, such PPO (Schulman et al., 2017) and GRPO (Shao et al.)
Markov Decision Process (MDP), which is
the reward function. In probabilistic settings,
2024) have been used (2017); Ouyang et al.
extensively to fine-tune LLMs from human feedback (RLHF, Christiano et al.
(2022)) and from verifiable rewards (RLVR, Lambert et al. (2024) Guo al.
2025
2

---

Published as a conference paper at ICLR 2026
1.2 RELATED WORK
Leveraging deep learning in the context of combinatorial optimization (CO) problems has emerged as major area of research (Cappart et al.] 2021] and has been applied to wide range of problems such as combinatorial graph problems (Khalil et al. 2017). SAT solving (Selsam et al. 2019). Mixed- Integer Programming (Khalil et al. 2022). and Constraint Satisfaction Problems Tönshoff's al.) 2023). Here. we primarily focus on work that aims to enhance SAT solvers with (graph) neural networks. One line of work suggests using predictions of predefined variable properties to guide SAT solver branching heuristics. [Selsam & Bjömerr (2019) train GNN to predict whether variables belong to an ANSAT core. The branching heuristic then guided by periodically resetting the solver's VSIDS scores to the GNN's s predictions, thus making the guidance specific to VSIDS- based CDCL solvers and dependent on careful tuning of the reset frequency. Wang et al. (2024) predict whether literals occur in the backbone of satisfiable formulas and use these predictions to set the polarity of variables. Another line of work explores purely RL-based training for enhancing branching heuristics, eliminating the need for expert supervision. [Kurin et al. (2020) uses Q- Q-learning train GNNs end-to-end as branching policies to minimize solver runtime, and Cameron et al. (2024) propose Monte Carlo Forest Search for guiding early branching decisions in SAT Solvers UNSAT problems. Both methods require one GNN forward pass per guided branching decision, which creates a significant bottleneck as the GNN usually requires orders of magnitude more runtime than classical branching heuristics. As consequence, both methods only leverage the learned guidance in a few early solver decisions. Further related work is proposed by Han (2020), who accelerate cube-and-congee solvers with supervised learning, [Li et al. (2024), who suggest improving clause deletion heuristics CDCL SAT solvers with GNNs, and Zhai & Ge (2025), who use RL to speed up parallelized divide-and-conquee solvers.
RLAF-GUIDED SAT SOLVERS
2.1 GUIDED BRANCHING HEURISTICS
We modify existing SAT solvers to incorporate external variable weights into their branching heuristic. Let some base SAT solver be given. We assume that this solver is a DPLL-derived backtracking search algorithm. We further assume that the branching hcuristic is implemented by first selecting variable å = argmax, Score(x) that maximizes some variable scoring function Score before picking a literal sign according to some secondary heuristic, as illustrated in Algorithm 2 existing branching heuristics, such VSIDS and look-ahead heuristics, fit the generic algorithm pattern while relying on different definitions of variable scores. Note that these scores usually depend on the current partial assignment of the search as well as information extracted in previous search steps, such as encountered conflicts. We can modify this decision heuristic to incorporate additional variable weights : Var(ø) - R>o for the given input formula Φb.
Many
t argmax w(x)- Sccore()
These weights are passed to the modified solver as additional input and modulate its branching heuristic by scaling the variable-wise scores. In this manner, we can inject prior knowledge of variable importance into the solver's branching decisions without sacrificing its original heuristic. Naturally, choosing useful variable weighting w by hand is difficult. Instead, our focus is on learning to infer effective variable weights from the imput formula's structure using deep neural network.
In addition to these weights, we may also specify a mapping p Var(ø) - {0, 1] that assigns a polarity p(x) to each variable x. When is chosen decision variable, the polarity determines which value is assigned to x first. Specifying polarities for variables is a common function for modern SAT solvers, and well-chosen values can have a significant impact on run time, especially on satisfiable instances. In this work, we will infer variable-win wise polarities alongside the variable weights with learned GNN model. Overall, the modified solver Solve(d) W) takes as input CNF formula & as well as a variable parameterization W (w, p) that assigns a weight w(x) e Ry0 and polarity p(x) {0, 1} each variable E Var(ø).
3

---

Published as a conference paper at ICLR 2026
a) Graph G(a)
by GNN
c) Policy ns
d) Weights & Polarities W (w.p)
Guided SAT Solver SOlvE(O. W)
31
U
argiaa SCORE(s)
No
8.5
1
2.4 U
w(x)
p(z)
Figure 2: a) The imput formula 6 is modeled as a graph G(ő). b) The graph is processed by trainable GNN and outputs parameterization policy Te(Ø). e) The policy Te( consists of independent variable-wise weight (LogNormal) and polarity (Bernoull)) distributions. d) A variable parameterization W (w.p) p) is sampled from (o))), mapping each variable æ in to weight w(x)) E l2 and polarity p(x) E {0, 1}. e) A guided SAT solver incorporates the parameterization W to guide its branching heuristic.
2.2 GRAPH REPRESENTATION AND ARCHITECTURE
Our goal is to map instance & to advantageous variable weights and polarities with neural network. A natural approach is to map & to suitable graph representation G(Ø) = (V()), E()) that captures the instance's 's structure. This graph can then be processed by GNN that extracts structural information in a trainable manner. We represent Ø as a standard "Literal-Clate
Graph" " proposed in prior work [Selsam et al. (019). Note that this choice is modular, other graph representations have also been suggested in the literature and could also be used. We process this graph with a trainable GNN model No that performs message passing to extract latent structural embeddings for every vertex. Here, 0 represents the vector that contains all trainable model parameters. The output of Na a mapping y Var(ø) - 2 that assigns two real numbers each variable in the input formula ø. The full model details are provided in Section A
2.3 GUIDANCE POLICY
For a given input formula d, we map the output of the GNN No to a policy To()) from which a variable parameterization W W (Ø) can be sampled. Recall that for given SAT instance the GNN No outputs a mapping y Var(ø) + R2 that associates every variable x Var(ø) with two real numbers p(x), p(x) E IR, [u(x), p(x)] y(xx). These outputs are used to parameterize variable-wise weight and polarity distributions, respectively. Concretely, for each variable x in á we define its weight policy Ty (z) as a Log-Normar distribution over positive real weights:
T (x) LogNormal(u(z).. o")
Here, the inferred parameter (=x) E IR is used as the log-mean of the distribution, and xx E Ro is a hyperparameter. We employ the Log-Normal distribution because it naturally models unimodal distributions over strietly positive real numbers, ensuring that the sampled weights remain valid multiplicative scaling factors without requiring artificial clipping or constraints. While we observed reasonable training convergence with alternative parameterizations, such as Truncated Normal and Poisson distributions, the Log-Normal formulation proved simpler and more robust.
Analogously, we define a variable's polarity policy (x) probability is obtained by applying a sigmoid function to p(r):
Bernoulli distribution where the
The (x) Bernoulli Bernoulli(Sigmoid (p(x)))
(3)
The complete variable parameterization policy कe is then defined as the joint distribution of TT' (a) and 7h (wr) over all variables:
To( 5 (x1) mi (x11
n. (x T (Ix))
We sample variable parameterization W (w,p) To from this distribution in one shot by independently sampling a weight w(xx) ~ x (x)) and polarity p(x) ~ =f(()) for each variable x in parallel. The probability density To (W)))) of W can then be factorized as
no (W)o)
II TH (w(x))0) ())))))))
(5)
4

---

Published as a conference paper at ICLR 2026
Sample Parameterizations
b) Run Solver
c) Cost & Advantage
d) Optimize Lroo
Cost
A
W1
Solve( W1)
150
- 1.39
(W [ +
Φ TT(Ø)
W2 Solve( W2)
128
0.91
(o 6) f
W3 solve(o, W3)
132
0.49
To (VWa f
Figure 3: Learning to accelerate a SAT solver with GRPO: a) For given training formula e sample multiple variable parameterizations i.idd from the current policy (e( b) Run the SAT solver on ø with each parameterization. Map the cost of each solver run (i.c. the number of decisions) to the normalized group-relative advantage Á(ó, W). d) Optimize the model weights to maximize Crro to shift the policy towards faster parameterizations.
Note that all trainable weights of the GNN model have a partial derivative with respect to Te (W()) for given W, which enables to train with policy-gradient methods such GRPO. During training, we sample multiple W i...d. from To (Ø) and use the variance of the observed solver runtimes to compute our training signal, as explained in Section 2.4 At test time, we do not sample randomly from No (1b) but simply use the mode W. which deterministically chooses the most probable weight and polarity for each variable This eliminates source of variance when testing and, average, yields better results than sampling at random from the learned policy.
2.4 POLICY OPTIMIZATION
Our aim is to learn a policy GNN that guides the SAT solver towards lower computational costs on given distribution SAT instances. Formally, let Q2 be some training distribution of SAT problems. The objective is to learn model weights 0 that minimize the expected solver cost when applying the learned policy to instances sampled from ft:
= arg min
E an W~ro(d)
[Cost (W))..
(6)
Here, Cost((, W) is defined as the number of decisions required when rumning Solve(ø, W), which is the primary target metric we aim to minimize. We can view this objective as an RL problem by modeling the process of choosing W single-step Markov Decision Process (MDP) where the input formula øi is viewed as the state, and single-step episode unfolds by choosing a variable parameterization W as the action. Once the action taken, the environment transitions immediately to terminal state, yielding reward R(ó, W) -Cost(e (Ø, W) that is the negative of the solver's s cost (e.g., number of decisions). Note that we also experimented with directly using CPU time as cost measure, but found this to yield less stable training due to the performance variance caused by noisy CPU utilization.
We leverage Group Relative Policy Optimization (GRPO) (Shao et al., 2024 to learn a policy for this RL problem. GRPO is a simplification Proximal Policy Optimization (PPO) (Schulman et al. 2017) that eliminates the need for learning additional value network. The initial model weights 6, are sampled at random. GRPO updates these model weights in iterations E {l,..., K}. In iteration k, first sample batch of training instances from J {Ø)..... AN3 ~ Ω2 from the given training distribution. For each such formula Φi we sample M variable parameterizations W W......, W.M ( i.i.d. from the current policy. We then Solve Wa,) for all i E [N] x [M] and measure the corresponding cost and reward. The group-relative advantage is then defined
R(o,, Wa,) mean (R,)
A.
std(R.)
where R, (R. 1j fl....,
(.I...,)) is the of all rewards collected for the same instance 6, The main objective is to maximize the clipped policy update function for each training instance ds:
(P (0.)=
1 Σ M
min (0)
-- (.,,--,,,+e)A... e.1+))
(8)
5

---

Published as a conference paper at ICLR 2026
Here, E (0,1) is a hyperparameter, and (f) is defined as the probability ratio of the new policy and the policy learned in the previous GRPO iteration:
To ( 1o,)
Ti. (0)
(9)
TH (Wa, (bx)
This objective aims to adjust the policy such that actions (e.g.. variable parameterizations) with high advantage become more likely while avoiding excessively large distribution shifts by clipping the objective at probability ratio determined by The full training objective combines Lpoo with
an additional term that penalizes the KL divergence relative to the previous model weights 0z-1 to
stabilize training further:
L( Φ.) = Lrro( (x)) - BB. KL
(10)
Here, the weight 3 2 0 is an additional hyperparameter. Starting from the previous model weights 8x-1, we learn updated model weights 0₂ by performing stochastic gradient ascent for fixed number of steps to maximize this objective function for all training instances. This overall process repeats in the next round of GRPO. In the appendix, Algorithm| provides complete formal specification of our training.
2.5 TRAINING SETUP
We are utilizing GRPO as an online RL algorithm to learn the parameters of our policy GNN directly from observed solver costs. As consequence, we train with the SAT solver in-the-loop and make M-N calls to the solver per GRPO iteration. With our default parameters (N= = 100, .M = 40) we make 4000 SAT solver calls in each iteration. This imposes the practical constraint to train distribution Ω of SAT problems where this number of solver calls is possible in an acceptable time on the underlying hardware. The work presented here intends to be a small-scale demonstration of RLAF as a training paradigm, and all training is performed on machines with one (multi-core) CPU and one GPU, Therefore, the training data in our experiments is chosen so that each instance solvable by the given base solvers within a fraction of second. In future work, the hardness and size of the training problems can be scaled up substantially by leveraging a distributed compute cluster for collecting the SAT solver feedback. Crucially, we demonstrate in Section 3 that after training. the learned policies do generalize to significantly harder and larger problems. The reliance on comparatively easy training problems is therefore not significant limitation for learning effective GNN-guidance with RLAF.
EXPERIMENTS
In our experiments, we aim to answer two primary research questions: (i) Can RLAF train GNN- based guidance policies that shorten solver runtimes and generalize to harder formulas? (ii) How do RLAF-trained policies fare against guidance based learning predefined notions of variable importance in a supervised manner? Furthermore, we want to understand whether the learned policies capture known variable properties after training and whether the policies learned with different solvers are related or solver-specific.
Solvers We conduct experiments with two distinct base solvers: The well-known CDCL solver Glucose (Audemard & Simon| (017) and the DPLL solver March (Heule et al. 2005). Glucose uses the EVSIDS branching heuristic and is comparatively strong on structured problems, while March uses look-ahead branching heuristic and is among the best-known solvers for random instances. Full details on the extended solvers are provided in Section[A.3 As our focus is prototype-scale demonstration of RLAF training paradigm, we leave integration with state-of-the-art CDCL solvers for future work aimed at large-scale industrial settings.
Data We consider three well-known classes of SAT problems with significantly different structures to study how well RLAF can adapt the base solvers each of them. In Section B. we provide full details on the data generation and dataset statistics. Random 3SAT: We define AT))(n) as the distribution of uniformly random 3SAT instances with variables and tauuee-tovvaritte which is approximately the critical density where the instances transition from SAT to UNSAT. The training data consists of 20K instances sampled from AS (200). We test on larger instances with
ratio of 4.26,

---

Published as a conference paper at ICLR 2026
Table Results on test instances. All metrics are averaged across the respective test sets. The mean number of decisions is rounded to the nearest whole number. For results with RLAP, we include the time required for the GNN forward pass in the total runtime. We highlight numbers in bold when they are the best value achieved for the respective base solver.
Data
Glucose
Glucose RLAF
March
March RLAF
Distribution
Result
Count
Decisions
Time (8)
Decisions
Time (s)
Decisions
Time (s)
Decisions
Time (s)
SAT
103
341,418
121,184
1.85
2,893
0.25
2,389
0.23
3SA7(300)
UNSAT
97
725,812
15.49
508,676
8.21
11,783
1.01
11,757
1.04
SAT
108
1,568,289
48.76
805,035
18.88
16,546
1.64
11,702
3SAT(350)
UNSAT
92
3.628.268
132.28
3,136,552
82.84
52.287
5.14
51,846
5.16
3SAT(400)
SAT
89
9,638.668
598.35
4,447,304
186.70
64,296
7.27
47,992
5,51
UNSAT
111
22.130.692
1,895.62
20,808,043
1,112.71
245,064
27.49
242,499
27.51
3Cor)
SAT
77
15,519
0.36
6,988
0.22
926
0.22
598
0.21
UNSAT
123
70,692
1.99
34,920
0.81
10,563
2.61
5,954
(S00)
SAT
91
82,758
2.61
35,901
1.05
7,689
2.55
4,754
1.68
UNSAT
108
460,881
17.47
363,2778
12.24
100,811
33.34
60,321
20.52
3COL(600)
SAT
87
606,599
25.03
339,378
11.59
63,512
27.16
42,862
18.71
UNSAT
113
3,092,344
193.96
2,811,133
155.23
754,720
313.57
461,639
197.12
CRYPTO(20)
UNSAT
100
51,294
1.16
3,541
0.15
1,203
0.82
390
0.41
CRYPTO(15)
UNSAT
100
225,447
5.74
64,150
1.40
52,282
34.56
8,257
6.40
CRYPTO(10)
UNSAT
100
3,753,850
162.45
1,520,075
64.95
679,864
467.38
230,905
169.22
n E {300, 350, 400), where we sample 200 instances for each size n. Graph Coloring: We consider the distribution (C) of SAT problems that decide 3-colorability for random Erdös-Rényi graphs with n vertices. We set the edge probability such that the expected vertex degree is 4.67, which is approximately the critical density for 3-colorability where hard instances are common (Zdeborová Krzakala| (207). We train on 20K instances sampled from (301(300) on 200 larger problems each for n [400, 500, 6003. Cryptographic: We further include highly structured instances arising from SAT-based decryption attacks (Soos et al. 2009). We define CRYPTO(1) (n) as the distribution of SAT instances generated for decrypting the Hilla22 cipher (Courtois et al. (009) with n given help bits. Note that these instances are harder for smaller values of n and are mostly UNSAT. We train on 20K instances from CRYPTO((2)) and test on harder problems with n E {20, 15, 10).
Hyperparameters We train different model for each solver and each SAT problem class. We configure the GNN with 10 layers with embedding dimension GRPO iterations, each consisting of 50 training steps of SGD. In every iteration, we use N = 100 training formulas and collect feedback for M 40 variable parameterizations for each formula.
256. We train for K 2000
3.1
MAIN RESULTS
Table provides the main results for both Glucose and March on our test sets. We observe that GNN- guided training with RLAF consistently accelerates the given base solver. The margin of improvement depends on the base solver and the class of problem instances. For 3SAT(400) problems, RLAFF guidance reduces the mean runtime of Glucose by 69% and 41 % for satisfiable and unsatisfiable instances, respectively. Similar improvements are observed for satisfiable 3-coloring problems as well as cryptographic instances. For unsatisfiable coloring instances with 600 vertices, the runtime of Glucose is reduced by around 24%. The smallest margin of improvement is observed for the March solver on unsatisfiable 3SAT instances. While March+RLAF does need fewer decisions on average to solve this class of problems, the runtime is worse, the small improvement does not compensate for the additional runtime overhead of the GNN forward pass. It is known that lookahead DPLL sol like March are very strong baselines for unsatisfiable random instances, so this result is not surprising. For more structured problem classes, RLAF is able to accelcrate the March solver substantially on both satisfiable and unsatisfiable instances. We emphasize that the wall-clock runtime of the GNN forward pass is included in the runtime measurements with RLAF-guidance. For the instances used here, this runtime is generally around 0. seconds or less, which is negligible compared to the solver runtimes harder problems. We refer to Section B.4 in the appendix for extended results that report the GNN overhead in detail and plot the cumulative number of solved instances over time. Overall, these results demonstrate that RLAF is able to train GNN-based solver guidance and that relying on comparatively easy problems for efficient training does not prevent the learned policy from generalizing to more complex problems at test time.
7

---

Published as a conference paper at ICLR 2026
UNSATERIABLE
SATEEFIBBLE
Relativ Runtine to Gluooe
Gurmee-Core
80
00
40
300
250
400
200
350
400
400
500
600
400
500
600
10
Figure 4: Runtimes relative to the base solver Glucose for RLAF and supervised approaches based on Backbones and UNSAT cores. Less is better.
3.2 COMPARISON TO SUPERVISED APPROACHE
Prior work suggests predicting predefined variable properties, such UNSAT core Selsam & Bjørner (2019) or backbone Wang et al. (2024) membership, in a supervised manner, and then transforming model predictions into variable weights and polarities for solver guidance. Here, we aim compare how guidance learned with RLAF compares to this approach. Note that the notions of UNSAT cores and backbones are only sensible training targets for some instance distributions. Backbones can only be non-empty on satisfiable instances, and even for satisfiable graph coloring problems, all backbones are empty due the permutation symmetry of the vertex colors. Furthermore, on our UNSAT ASA training instances, we observed that the UNSAT core extracted by SAT solvers contained all variables on almost all instances, yielding a training target that effectively constant. Due to these limitations, we use the AT instances to evaluate the effectiveness of predicting the backbone, while we use the graph coloring and cryptographic instances to compare RLAF to core-based solver guidance. For a use the same GNN architecture used to train with RLAF and train a separate model for each instance distribution. The transformation that maps the backbone/core predictions to variable weights is tuned separately for each instance distribution set. Full details about the setup of this comparison are provided in Section B.5 We also provide an additional comparison of RLAF to Graph-Q-SAT Kurin et al. (020), unsupervised baseline using Q-Learning. in Section B.6
fair comparison,
the corresponding validation
Figure SegureAcoome compares the results for Glucose in terms of the relative wall-clock runtime compared to the base solver. Overall, the policy learned with RLAF significantly outperforms solver guidance based on both UNSAT core and backbone predictions by achieving a smaller relative runtime. The backbone-basse heuristic outperforms RLAF only on satisfiable 3SAT instances with 300 variables, but not on larger problems. On unsatisfiable AS problems, the backbone- -eedddde-guided heuristic performs substantially worse. RLAF also outperforms core-based guidance for both graph coloring and cryptographic SAT problems. Overall, these results demonstrate that pure RL-based learning with RLAF can yield more effective solver guidance than predicting handerafted notions of variable importance in a supervised manner.
3.3 EXPLORING LEARNED VARIABLE WEIGHTS
We further aim to gain insights into the weight distributions learned through RLAF In particular, we investigate whether the policies learned with different base solvers are related and whether they capture predefined variable properties, such as backbone and UNSAT core membership. To this end, Figure compares the weights for 5000 randomly selected variables from the corresponding validation sets. Specifically, we plot the expected variable weight [[((x)) for the Glucose-trainel policy on the x-axis and plot the corresponding value for the March-trained policy on the y-axis. We also report the Pearson correlation coefficient (r) for these weights to quantify their correlation. For AS, we only plot variables from satisfiable instances and additionally indicate whether each variable belongs its instance's backbone. Likewise, we focus unsatisfiable instances for 3CoL and CRYPTO and indicate a variable occurs in the UNSAT core extracted for the experiment in Section 3.2
8

---

Published as a conference paper at ICLR 2026
73350
Coloring (n-0.8456)
Crysto (rwO 8478)
Bacidtine
Com
Merch March--Htaa SLLAY E.,0000
March RLAT Eleboll
1:35
0.13
Glucose RLAF Elwoo1
Gluosse+RLA E[WEN)
Gluoose+RLAF EtwEx)
Figure 5: Weight correlation between policies learned with different solvers. For each instance distribution, we randomly sample 5, 000 variables æ from the corresponding validation set and plot the expected variable weight E [[][))] for the policies learned with either base solver. The color further indicates the backbone or UNSAT core membership of each variable.
We observe that the variable weights of the two policies are generally correlated, with a Pearson correlation coefficient between 0.73 and 0.85. This indicates that the learned weightings capture structural properties that are inherent to the variables and accelerate the search across different solvers. We further observe that for the 3COL and CRYPTO instances, the variables with high weights are predominantly members of the UNSAT core. For these problem instances, the RLAF-based training therefore self-discovered weight policies that correlate to existing handerafted heuristics while performing better, as demonstrated in Section For the 3SAT instances, we do not observe a clear correlation between the learned weight policies and backbone membership, showing that in this case, the trained models express functions that, while effective, do not resemble this particular handcrafted heuristic.
4 DISCUSSION
We introduced RLAF as a paradigm for training GNN-based policies that guide the branching heuristics of SAT solvers. Our work contributes (i) a generic mechanism for injecting variable weights into branching heuristics, (ii) a formulation weight selection as a one-shot RL problem, (iii) a way to leverage GNNs trainable policies in this setting, and (iv) experimental evidence that GRPO can learn policies that reduce the computational cost different base solvers. In our empirical studies, the learned policies generalize larger and harder instances, and consistently surpass supervised baselines that rely on handcrafted variable properties. Moreover, policies trained with different base solvers converge toward similar structural signals, suggesting that RLAF is capturing inherent information about SAT instance structure that is not specific to the underlying base solver.
The current implementation is designed small-scale prototype optimized for training on relatively simple formulas using moderate hardware. This constraint allows for only comparatively simple problems to be solved quickly enough to collect sufficient solver feedback on local CPU cores in each GRPO iteration. Expanding the system to leverage distributed computing resources would enable the incorporation of larger and harder SAT problems during training, potentially leading to better guidance policies. GNN scalability also remains bottleneck, particularly during training, as processing large industrial instances imposes significant memory and computational demands. At the same time, the expressive power of our network, standard message-passien GNN, is bounded by color refinement (Morris et al. 2019, Xu et al. 2019). Combining higher expressivity and scalability remains critical challenge for applying GNNs to large, structured problem instances.
Finally, the proposed methodology is not strictly limited to SAT solvers. Branching heuristics are critical components not only in SAT solving but also for Mixed Mixed-Integer Programming (MIPs) and Constraint Satisfaction Problems (CSPs). More broadly, implementing any kind of selection heuristic as the argmax of some scoring function is generic pattern of algorithm design found across many domains. For any such algorithm, one can introduce external multiplicative weights that guide the heuristic and then phrase the task of inferring effective weights as RL problem. In this work, we have demonstrated that this general methodology can be leveraged in the context of SAT solving. Translating other domains and algorithms remains as future work.

---

Published as a conference paper at ICLR 2026
REPRODUCIBILITY STATEMENT
All experimental code is included in the supplementary material (https://github com/ Ecenshoff E RLAF), E/LAF) including scripts for data generation and preprocessing. We also provide detailed information on the hyperparameters required to reproduce our results in Section B in the appendix.
ACKNOWLEDGMENTS
The project was funded by the European Union (ERC, SymSim, 101054974). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.
REFERENCES
Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern sat solvers. In IJCAI, volume 9, pp. 399-404. Citeseer, 2009.
Gilles Audemard and Laurent Simon. Glucose and syrup in the sat' 17. Proceedings of SAT Competition, pp. 16-17, 17, 2017.
Armin Biere, Marijn Heule, and Hans van Maaren (eds.). Handbook of satisfiability, volume 185. IOS press, 2nd edition, 2021.
Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL 2.0. In Arie Gurfinkel and Vijay Ganesh (eds.), Computer Aided Verification 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of Lecture Notes in Computer Science, pp. 133-152, Springer, 2024. doi: 10.10077978-3-000
Chris Cameron, Jason Hartford, Taylor Lundy, Tuan Truong, Alan Milligan, Rex Chen, and Kevin Soyton-Brownn Unsat solver synthesis via monte carlo forest search. In International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research, pp. 170-189. Springer, 2024.
Quentin Cappart, Didier Chételat, Elias B. Khalil, Andrea Lodi, Christopher Morris, and Petar Veličković. Combinatorial optimization and reasoning with graph neural networks. In Zhi-Hua Zhou (ed.), Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21, pp. 4348 4355. International Joint Conferences on Artificial Intelligence Organization, 8 httpsttts::///t http:///..oorr....../oo 24963/ /iceaaca.cca..... 2021/ or.//0.24/33333333
2021. doi: (0.24963/jcaii.222155555 Survey Track.
595
Paul F Christiano, Jan Leike, Tom Brown, Miljan Martic, Shane Legg, and Dario Amodei. Deep reinforcement learning from human preferences. In I. Guyon, U. Von Luxburg, S. Bengio. H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett (eds.), Ad- vances in Neural Information Processing Systems, volume 30. Curran Associates, Inc.. 2017. URL https::/ppocceedinneeee//// www.eiinnnnnnueuueeeee www.nnnuriinccm cwtppppp.cppppp....eeppppp fi ftl.ss/ppper//2117 File/ http://ccccaabbosssaaaaaaoddeeee
Nicolas Courtois, Sean O'Neil, and Jean-Jacques Quisquater. Practical algebraic attacks on hitag2 stream cipher. volume 5735, pp. 167-176, 09 2009. ISBN 178-3-642-04473-1. doi:
0000077788-3-42-4447777
James M Crawford and Larry D Auton. Experimental results on the crossover point in random 3-sat. Artificial intelligence, 81(1-2):31-57, 1996.
Niklas Eén and Niklas Sörensson. An extensible sat-solver. In International conference on theory and applications of satisfiability testing, pp. 502-518. Springer, 2003.
Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. Deepseck-rl: Incentivizing reasoning capability in Ilms via reinforcement learning. arXiv preprint arXiv:2501. /2948 2025.
10

---

Published as a conference paper at ICLR 2026
Jesse Michael Han. Learning cubing heuristics for sat from drat proofs. 2020.
Marijn Heule, Mark Dufour, Joris Van Zwieten, and Hans Van Maaren. March eq: Implementing additional reasoning into an efficient look-ahead sat solver. In Theory and Applications of Satisfia- bility Testing: 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10-13, 2004, Revised Selected Papers 7, pp. 345-359. Springer, 2005.
Marijn JH Heule and Hans Van Maaren. March_ dl: Adding adaptive heuristics and a new branching strategy. Journal on Satisfiability, Boolean Modelling and Computation, 2(1-4):47-59 2006.
Elias Khalil, Hanjun Dai, Yuyu Zhang, Bistra Dilkina, and Le Song. Learning combinatorial optimization algorithms over graphs. Advances in neural information processing systems, 30, 2017.
Elias B Khalil, Christopher Morris, and Andrea Lodi. Mip-gnn: A data-driven framework for guiding combinatorial solvers. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 36, pp. 10219-10227, 2022.
Oliver Kullmann. Fundaments of branching heuristics. In Handbook of Satisfiability, pp. 351-390. IOS Press, 2021.
Vitaly Kurin, Saad Godil, Shimon Whiteson, and Bryan Catanzaro. Can q-learning with graph networks learn generalizable branching heuristic for
solver? In H. Larochelle, M. Ranzato, R. Hadsell, M.F. Balcan, and H. Lin (eds.), Advances in Neu- ral Information Processing Systems, volume 33, pp. 9608-9621. Curran Associates, Inc.. Files/paper/2022
http://ccceeciio......eeee.e..aa file/ Bllc//80065555522777666666627222
2020. URL
Nathan Lambert, Jacob Morrison, Valentina Pyatkin, Shengyi Huang, Hamish Ivison, Faeze Brahman, Lester James V Miranda, Alisa Liu, Nouha Dziri, Shane Lyu, et al. Tulu 3: Pushing frontiers in open language model post-training arXiv preprint arXiv2241..55124 2024.
Hongduo Liu, Peng Xu, Yuan Pu, Lihao Yin, Hui-Ling Zhen, Mingxuan Yuan, Tsung-Yi Yi Ho, and Bei Yu. Neuroselect: Learning select clauses in sat solvers. In Proceedings of the 61 ACM/EEE Design Automation Conference, DAC '24, New York, NY, USA, 2024. Association for Computing Machinery. ISBN 9798400706011. doi: 10.1145/3649329.3666222
URL
bttts:://oi..rgg 1tte///....1113343..2.1
Christopher Morris, Martin Ritzert, Matthias Fey, William I.. Hamilton, Jan Eric Lenssen, Gaurav Rattan, and Martin Grohe Weisfeiler and Leman go neural: Higher- graph neural networks. In Proceedings of the Thirty-Third AAAI Conference Artificial Intelligence (AAAI), pp. 4602-4609, 2019.
Long Ouyang, Jeffrey Wu, Xu Jiang, Diogo Almeida, Carroll Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, al. Training language models to follow instructions with human feedback. Advances in neural information processing systems, 35:27730- 27744, 2022.
Rafael Rafailov, Archit Sharma, Eric Mitchell, Christopher Manning, Stefano Ermon, and Chelsea Finn. Direct preference optimization: Your language model is secretly reward model. In A. Oh, T. Naumann, A. Globerson, K. Saenko, M. Hardt, and S. Levine (eds.), Advances in Neural Information Processing Systems, volume 36, pp. 13728-53744 Curran Associates, Inc., 2023.
John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. Proximal policy optimization algorithms. arXiv preprint arXiv:1707.00347, 2017.
Daniel Selsam and Nikolaj Bjømer. Guiding high performeffe sat solvers with unsat-core predictions. In Theory and Applications of Satisfiability Testing-SA7 20/9: 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings 22, pp. 336-353. Springer, 2019.
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning a SAT solver from single-bit supervision. In International Conference on Learning Representations, 2019. URL httthhttts:://peeeeee

---

Published as a conference paper at ICLR 2026
Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, YK Li, Y Wu, et al. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXtv:2402.03300 2024.
M. Soos. Grain of salt an automated way to stream ciphers through sat solvers. 2010. URL https://apl semant icscholes ar. org/ wwwg//ooooooooooooooooooooo Ctap/Corppp Corpus ID: 61 (1822222
Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending sat solvers to cryptographic problems. In Oliver Kullmann (ed.), Theory and Applications of Satisfiability Testing SAT 2009, pp. 244 257, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. ISBN 978-3-642-02777-22
Jan Tönshoff, Berke Kisin, Jakob Lindner, and Martin Grohe. One model, any esp: Graph neural networks as fast global search heuristics for constraint satisfaction. In Proceedings of the Thirty- Second International Joint Conference Artificial Intelligence, IJCAI-23, pp. 4280 4288, 8 2023. 2023/442222444
doi: 21444963//jcai2222377777 ULL/ttpss//ooo...r///222222
Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth McMillan, and Risto Miikku- lainen. Neuroback: Improving CDCL SAT solving using graph neural networks. In The Twelfth International Conference on Learning Representations, 2024.
Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. How powerful graph neural networks? Proceedings of the Seventh International Conference on Learning Representations (ICLR), 2019.
Lenka Zdeborová and Florent Krzękata. Phase transitions in the coloring of random graphs. Phys. Rev. E, 76:031131, Sep 2007, doi: 10. 10.10331hyRR11..000313.1 URL https::///iiie aps
76. 031131
Shumao Zhai and Ning Ge. Learning splitting heuristies in divide-and-conquer SAT solvers with reinforcement learning. In The Thirteenth International Conference on Learning Representations, 2025. URL hattts:///peaaeeee http://ppwweeeeeeeeeeeeeeeeeeeee net httt//foummmiieo wtw.ooummmddduaooBBB......
uUsL07BsL
12

---

Published as a conference paper at ICLR 2026
A
METHOD DETAILS
A.1 GRAPH REPRESENTATION AND ARCHITECTURE
We represent formula e as graph G( (V))), F(ø)). This is standard "Literal-Clause Graph" used in prior work, such as NeuroS AT [Selsam et al. (2019). Formally, the vertices of this graph (Ø) (o) U (l) are the literals and clauses of ø. The edges E(Φ) ELo(Ø) ELL (o)
connect literals with the clauses they occur in and with the opposing literal of the same variable:
(Ø) = {az, -x) 2 E {())
(11)
ELC(Ø)= U ((C,))&EC) CECI(()
(12)
A.2 MESSAGE-PASSING NEURAL NETWORK
For each vertex e E Lit(o) U Cls(e) we obtain an initial embedding / (v) E RR:
(e) Enc(log(deg(v) + 1)).
(13)
Here d the latent embedding dimension of the model, and Enc is trainable 2-layer MLP that is applied to the log-normalized degree of
The GNN model then stacks I. E N message passing layers. For t E (1,.... : I.), the 1-th layer takes as input the previous embedding h²-1 and outputs a refined embedding ht' by performing a message pass. This message pass is split into two phases. First, each clause E Cls aggregates information from its associated literals:
A (c) = Ucls ('((), θ (N(O)
(14)
REC
Here, Ucis is a trainable MIP, and + is order-invariant aggregation. Throughout all experiments, we use element-wise mean for aggregation. In the second phase, each literal E Lit aggregates the updated embeddings from the clauses it occurs in:
h (2) = ULa ((()), θ (ct
(15)
c,FEc
Here, Ura is another trainable MLP that additionally also takes the embedding of the opposing literal -f as input. This model architecture is conceptually similar to that of NeuroSAT. One major difference is that we use more standard fixed-depth feed-forward GNN instead of recurrent model. Note that all MLPs used in our model have two layers, and the hidden layer is always SiLU-activated and has hidden dimension 2d. The final output is a variable embedding y Var(ø) - RR,, which obtained by concatenating the two literal embeddings associated with each variable x and then applying final 2-layer MLP Dec:
v(x) (x),
(16)
Note that we choose Dec as a 2-layer MLP with input dimension 2d, hidden dimension 2d, and output dimension 2. No activation is applied to the output, and the weights and biases the final layer of Dec are initialized as zeros. This ensures that at the beginning of training, the initial GNN No, assigns μ(r) = 0 and p(xx) = to all variables. We found this to be a stable configuration for initializing training. In particular, µu(x) 0 ensures that the log- rognoolyllly distributed weight policy Th (x) has a mode of approximately for all variables while p(z) = 0 ensures that the polarity of each variable is initially distributed uniformly.
A.3 SAT SOLVER DETAILS
GLUCOSE
Glucose (Audemard & Simon 2009) is popular CDCL solver based on Minisat (Eén & Sörensson
2003). Our modification is based on Glucose 4.2.1 (Audemard & Simon 2017 Like many other
https://gi
13

---

Published as a conference paper at ICLR 2026
CDCL solvers, Glucose uses the Variable State Independent Decaying Sum (VSIDS) heuristic for branching. Each variable z is assigned an activity score (etivity(z) that reflects its involvement in conflicts. When a conflict occurs, the activity scores of variables involved are increased by constant A, i.e.,
activity(x)) activity(x)) + A.
(17)
Periodically, all activity scores multiplied by decay factor 3 (where 0 < 8 < 1):
activity(a)) < B activity(x).
(18)
The activity then effectively serves as the SCORE function from Algorithm 2 Note that in practice, CDCL solvers commonly exponential VSIDS (EVSIDS), which is variation that yields identical decisions but avoids a costly loop over all variables to compute Equation (18). Rather than decaying the activity, the increment A is instead scaled up:
(19)
The cumulative values of the activity scores then yield the same decisions. To incorporate our variable weights w into this process, we simply modify Equation (17) by scaling the increment with the variable weight:
activity(x)) + activity(x)) w(x) A.
(20)
This ensures that the total activity score of each variable is scaled by a factor of w(z) at each step of the search while still preventing loops over all variables. We found that the runtime overhead of the additional multiplication in Equation (20) is negligible. We use the provided polarities p(x) to initialize the polarity (or phase) of each variable. Note that we leave phase saving on, so this initial polarity may be overwritten by the solver in later search steps. We run all experiments without randomized decisions (rnd-freq = 0). We further set the parameter K = 0.1 to minimize solver restarts, which found to improve performance on the three instance distributions considered in our experiments. Apart from this, we use the default parameters of Glucose.
MARCH
March (Heule et al. 2005; Heule & Van Maaren 2006) a DPLL-based solver that uses a branching heuristic based on look-ahead (Biere et 20.1) It is among the best-known solvers for purely random SAT instances. Look-ahead branching heuristics estimate how each variable's 's selection as a branching variable would affect the instance. In March, the scoring function SCORE(x) essentially quantifies how many new binary clauses would occur if a is picked for branching in the current search step. Computing this score is relatively expensive when compared to activity-basee approaches, and look-ahead solvers usually make fewer decisions per time. To decrease the cost of each branching step, March first applies pre-selection step before each branching decision, where a reduced set of candidate variables is selected according to a second scoring function PEEER---REEEEETTT This score aims approximate the expected look-ahead score but cheaper to compute. In the modified solver, we also apply the variable weight in pre-selection, i.e. the weighted scores w(xx) P
are used to select candidate variables. The ratio of selecele candidates is fixed at 10%. The same weights w are then applied again to the actual look-ahead scores obtain the branching variable. Afterwards, we use the given polarities p in each branching to determine the sign of the branching literal. Aside from these changes, run March in its default configuration.
ver
14

---

Published as a conference paper at ICLR 2026
Algorithm 4 GRPO Training for SAT Solver Guidance
1: Input:
2: Training formulas F = (0,,..., AN}
3: Number of GRPO iterations E IV
4: Number of samples per instance M E E
5: Number of optimizer steps per GRPO iteration S E N
6: Clip ratio (0, 1), KL penalty weight 3 2 0, learning rate 0
7: Initialize: Random weights 0o
8: for .......: K do
9:
for = 1,,...., N do
10:
for j = 1.2..... M do
WA To. (0i) Ot, + Cost(os, Was) Wis) + -Ci end for
12:
13:
14:
R;
(R(bi, Wai)) j tl,..., M}}
16:
for j = 1,2, ...,,... M do
Aij + Wa -mean(R.)
17:
Rtd
18:
end for
19:
end for
20:
+- 0k-1
21:
for
1,2, do
22:
for i = 1,2,.... N do
23:
for j 1,2, ..... M do
(l: (0) + _ (o.) end for
24:
25:
26:
(p (.)) t 1 Σn min
1.e))..))
M
27:
L(O (b:) +- L (b)) - B KI. (To(())) To (0:))
28:
end for
29:
0 v E, L( (:)
30:
end for
31:
0g + 0.
32:
end for
33: Output: Final model weights 0x-
15

---

Published as a conference paper at ICLR 2026
B EXPERIMENT DETAILS
B.1 DATA
Table provides full dataset statisties for all data distributions and splits. In the following, we provide further details on how each instance distribution is generated.
Random 3SAT Uniformly random 3SAT instances are commonly used to benchmark SAT solvers.
Here, each clause is sampled by choosing three distinct variables uniformly random and negating each with a probability is around m = 4.258m + 58. 58.26n where n is the number of variables (Crawford & Auton 1996). This is approximately the critical density where the instances transition from SAT ATSAT. We define (T) as the distribution of uniformly random 3SAT instances with n variables and [4.258n + 58.26m 31 clauses. For training, we use 20K instances sampled from (200), which are filtered such that exactly 10K instances are SAT and UNSAT, respectively. Our test sets contain larger instances with E {300, 350, 400J, where sample 200 instances for each size
50%. Hard instances are known to occur when the number of clauses
Graph Coloring Combinatorial problems on graphs are commonly solved by reducing them to Boolean SAT instances. Here, consider the problem of finding 3-colloing for Erdös-Rényl graphs We define 3COL(n) as the distribution of SAT problems that are obtained by sampling an Erdös- Rénós-Rééní graph with vertices and then encoding the problem of deciding 3-colorability as SAT instance. We set the edge probability such that the expected vertex degree is 4.67, which is approximately the critical density for 3-colorability where hard instances commonly occur (Zdeborová & Krzakała 2007). We train 20K instances sampled from (300. Again, these are filtered such that exactly 10K instances are SAT and UNSAT, respectively. Our test sets consist of larger problems with {400, 500, 600).
Cryptographic Hard, structured SAT problems commonly arise the context of cryptoanalysis, for example, for SAT-based decryption attacks (Soos et al. 2009). To generate data in this domain, we use Grain-of-Salt (Soos) 2010) to generate SAT instances for decrypting stream ciphers. We define CRYPTO(n) as the distribution of SAT instances generated for decrypting the HiTag2 cipher (Courtois) et al. 2009) with given help bits. We use the recommended generation parameters (-outputs bbase-shiie
-karnaugh 8). Note that these instances are harder for smaller values of and are mostly UNSAT. We train on 20K instances from CRYPTO(22) and test on harder problems with n E (20, 15, 10}.
For each of these three instance classes we formally define the corresponding training distribution Ω from Equation (6) as the uniform distribution over the set training instances.
Table 2: Dataset Statistics
Distribution
Split
Number
#SAT
#UNSAT
|Var [)] min
[Cls(())
mean
max
mean
min
max
0
3SAT(200)
Train
20.000
10,000
10,000
200.00
200
200
853.00
853
853
3SAT(200)
Val
200
100
100
200.00
200
200
853.00
853
853
3SAT(300))
Test
200
103
97
300.00
300
300
1,278.00
1.278
1.278
3SAT(350)
Test
200
108
92
350.00
350
350
1,491.00
1,491
1,491
3SAT(400)
400.00
1,704.00
1,704
1.704
3Col(300)
Train
20,000
10,000
10,000
900.00
900
3,284.75
3,009
3,618
3Col(300)
Val
200
100
100
900.00
900
900
3,288.63
3,042
3,489
3Col(400)
Test
200
77
123
1.200.00
1,200
1,200
4,392.31
4.144
4,603
8
3Col(500)
Test
200
91
108
1,500.00
1,500
1,500
5,488.56
5,216
5,750
3Co)
Test
200
87
113
1 1,800.00
1,800
1,800
6.597.24
6,306
6,861
Crypto(22)
Train
20,000
0
20,000
529.41
518
544
8,420.71
7,669
9,453
Crypto(22)
Val
200
529.24
8,413.41
7,937
9,075
2r))
Test
100
533.43
8,767.57
8.182
9,309
15))
Test
100
100
542.89
537
552
9,622.04
9,129
10,321
14
Crypto( 10)
Test
100
100
550.99
544
568
10,497.63
9,947
11,528
16

---

Published as a conference paper at ICLR 2026
B.2 HYPERPARAMETERS
Table B provides an overview of all RLAF training runs from our main experiments. We tuned the learning rate in 7) E {0.0001, 0.00005, 0.00001}: } and schedule warm up over the first 5 GRPO iterations. After warm up the the learning rate stays constant throughout training. The clip ratio was tuned in {0.1, 0.2) and the KL-penalty constant default values, which we found to be stable based on preliminary experiments, Each training run uses machine equipped with a single H100 GPU, an Intel Xeon 8468 CPU with 48 cores, and 128GB of RAM. The total runtime of all training runs is between 24h and 48h.
{0.1, 1.0). All other hyperparameters were given
Table 3: Hyperparameters
Glucose 3COL
March 3COL
3SAT
CRYPTO
3SAT
CRYPTO
K
2000
2000
2000
2000
2000
2000
M
40
40
N
100
100
100
100
100
100
S
50
50
50
50
50
50
0.1
0.1
0.1
0.1
0.1
0.1
clip ratio
0.2
0.2
0.2
0.1
0.2
0.2
KL--penatty &
0.1
1.0
0.1
1.0
0.1
0.1
batch size
20
20
20
20
20
20
learning rate ?
0.0001
0.00005
0.00005
0.00005
0.00001
0.0001
weight decay
0.0
0.0
0.0
0.0
hidden dim d
256
256
256
256
256
256
model depth L
10
10
10
B.3 TRAINING
Figure provides the learning curves for the RLAF-trained models in our main experiments. For all models, the cost decreases throughout training. We found that training with the March base solver tends to yield noisier training, particularly on 3SAT instances, where the policy does not improve further after 700 GRPO iterations. Exploring effective strategies for reducing this noise remains future work. Nonetheless, we can learn guidance policies that reduce the solver cost of both base solvers across all three problem instances.
We further note that, in principle, any RL method based on policy gradients can be applied to learn a GNN policy for MDP formulation. During development we briefly experimented with using DPO Rafailov et al. (2023) instead of GRPO and observed that training with DPO also converges effectively. However, the learned policies where less effective on test problems compared GRPO-learned policies, which is we we opted for GRPO as our default training methodology.
B.4 EXTENDED RESULTS
In Table we provide the results from our main experiments and additionally report the mean wall- clock runtime of the GNN forward pass. For all instance distributions, this GNN overhead is between 0.02 and 0.1 seconds, which negligible when compared to SAT solver runtimes on non-trivial instances. However, we note that classical SAT solvers commonly perform over 10d branching decisions per second. In setting where every guided branching decision requires separate forward pass, as in prior RL-based work (Kurin al.) 20200 Cameron et al.) 2024). is therefore not possible to guide every branching decision without incurring a massive runtime overhead. Our one-shot setup incorporates multiplicative weights obtained in a single GNN pass in every
avoids this problem branching decision with minimal runtime overhead.
Figure further provides survival plots that plot the cumulative number of solved problems against the wall-clock runtime on each instance distribution. With the exception of March on UNSAT 3SAT instances, RLAF constantly improves the speed of the guided base solver.
17

---

Published as a conference paper at ICLR 2026
3547
Coloring
Crypts
2400
3008
1108
1000
www
Figure 6: GRPO training curves of the RLAF models from our main experiment. We plot the mean number of decisions on the validation set against the GRPO iteration.
Table 4: Full results on test instances, including the main time spent for the GNN forward pass. All
metries are averaged across the respective test sets. The mean number of decisions is rounded the nearest whole number. For results with RLAF, we include the time required for the GNN forward pass in the total runtime.
Time
Decisions
Time
time
Time (5)
Time
(5)
38AT(300))
SAT
341,418
6.67
121,184
1.85
0.0210
2,893
0.25
2,389
0.23
0.0205
3SAT(300)
UNSAr
725,812
15.49
508,676
8.21
0.0209
11,783
1.01
11,757
1.04
0.0206
3SAT(350)
1,568,289
48.76
805,035
18.58
0.0238
16.546
1.64
11,702
1.19
0.0233
38AT(350)
3.136.552
3SAT(400)
4,447,304
5.51
3SAT(400)
UNSAT
22,130,692
1,895.62
20,808,043
1.112.71
0.0265
245.064
27.49
242,499
27.51
0.0270
3Gal(100)
SAT
15,519
0.36
6,988
0.22
0.0662
926
0.22
$98
0.21
0.0661
3Cul-400)
UNSAT
70.692
1.59
34,920
0.81
0,0662
10.563
2.61
5,954
1.57
0.0661
3Col(500)
82,758
7,689
460,881
363,278
100,811
3Cul6600)
SAT
606.598
25.03
339,378
11.59
0.0984
63.512
27.16
12,862
18.71
0.0888
3Cal6600)
UNSAT
3,092,344
193.96
2,811,133
155.23
0.9984
754,720
313.57
461.639
197.12
0.0990
Crypec20)
UNSAT
51,294
1.16
3,541
0.15
0.0974
1,203
0.82
390
0.41
0.0933
UNSAT
225,467
5.74
61,150
1.40
0,1075
$2.282
34.56
8,257
6.10
0.1073
Crypto(10)
162.45
1,520,075
230,905
Figure 7: Survival plots of our main results for different instance distributions.
18

---

Published as a conference paper at ICLR 2026
B.5 SUPERVISED UNSAT-CORE AND BACKBONE PREDICTION
For UNSAT-Core and backbone prediction in Section 3.2 we train supervised GNN models that are identical in architecture and size to the models used for our RLAF-bused policies. The used hyperparameters specified in Table In the following, we provide a detailed description of how these models are trained and evaluated.
UNSAT-CORE
Selsam & Bjömer 2019) propose to train supervised models that predict the UNSAT-core membership of variables and then the model prediction guide branching heuristics. Following their methodology, we phrase the task of predicting whether or not a variable occurs in an UNSAT-core as variable-level binary classification task and train GNN for this problem in a supervised manner using standard cross-entrope loss. The ground -rrut on training and validation instances is computed by extracting the cores from DRAT UNSAT proofs generated by the CaDiCaL (Birre al. (2024) solver. Note that these cores are not minimal, as computing such would not be feasible. As discussed in Section 3.2 the extracted cores on our unsatisfiable AT training instances contain all variables for almost all instances and are therefore not a meaningful training target. We therefore only train UNSAT- core prediction models for 3COL and CRYPTO. We train a separate model for each distribution and restrict training to the unsatisfiable instances.
Note that Selsam & Björner 2019) integrate their prediction by periodically resetting the VSIDS scores of the guided CDCL-solver to prediction logits of the GNN. This requires careful tuning is also specific to solvers based on the VSIDS heuristic and would, for example, not be applicable to the March solver. Furthermore, in later ablation experiments, (Selsam & Björner (2019) report that the performance improvement obtained with a trained GNN is barely distinguishable from when an untrained, randomly initialized model is used, further questioning the effectiveness of guiding solvers with this strategy. To facilitate a direct and fair comparison with RLAF-trained policies, we instead combine the UNSAT-core predictions with our own solver guidance based on multiplicative weights. For variable x, let Peore (æ) be the predicted probability of being in an UNSAT-COrE according to the trained GNN model. Then we transform these probabilities to variable weights through the following transformation:
of the reset frequency.
w (x) + or (eooe(()).
(21)
Here, 2 0 is parameter that determines how the variable weight scales with the raw model predictions. For this experiment, we found weights of w(x) 2 1 to perform better, hence the offset of 1 in Equation (2)). The value of is tuneed the corresponding validation dataset in the range {10 4 10 10 2,10 10
100, 10 102 ,00,, 10*}. We tune a separately for both Glucose and the prediction of UNSAT-core membership has no clear implication for the sign of the branching literal. Using this methodology, we found that the UNSAT-core predictions can significantly accelerate both base solvers, although by smaller margin than RLAF-trained policies.
March. The polarities
simply set p(x)=
BACKBONE
Wang et al. 2024) suggests using the backbone membership of literals as a supervised training target and then setting variable polarities using the model predictions. We follow their methodology and train a GNN on the literal-level binary classification task using cross-entropy loss. As discussed in Section 3.2 we only train model for the 3SAT instances and only use the satisfiable problems for training. The backbone of coloring problems is always empty due to the permutation symmetry of the colors, and some distributions, such as CRYPTO, predominantly consist of UNSAT instances.
When evaluating, we set the polarity of variable x as p(x) = 0 if Phackbone (-x) > Phuckhome (x) and p(x) otherwise. Here, Phackhone (E) is the predicted probability of literal belonging to the back- bone. We further assign variable weights w(x) under the assumption that correctly assigning backbone literals in early search steps positively affects the runtime. To this end, we apply the transformation from Equation (2l) to the mean backbone probability Prackhone (x) (x) 0.5 (Pbscktone (-x:) + Pbackboue (z)) to obtain a weight for each variable. Again, we tune the transformation parameter a for both base solvers on the validation set.
19

---

Published as a conference paper at ICLR 2026
Table 5: Hyperparameters the supervised models.
3SAT
3Cor.
CRYPTO
batch size
50
50
learning rate ry
0.0001
0.0001
0.0001
weight decay
0.1
0.1
0.1
epochs
200
200
200
hidden dim model depth L a Glucose
256
256
256
10
10
10
10a
103
10-2
a March
10
10
10
10
35AT SATISFIABLE
UNSATISFIABLE
Coloring SATIFRIBLEE
UNSATEFIABLE
UNSATISFIABLE
March-RLFF
March-Baciitoee
100
Marth-Core
Delativn to Narch
200
300
350
400
300
250
400
400
500
400
500
600
20
15
Figure 8: Runtimes relative to the base solver March for RLAF and supervised approaches based on Backbones and UNSAT cores. Less better. We include the time required for the GNN forward pass in the runtime.
SUPERVISED COMPARISON WITH MARCH
In Figure 8 we further provide the comparison with supervised baselines from Section 3.2 for the March base solver. On satisfiable 3SAT problems, our RLAF-trained policy and the guidance based on backbone prediction roughly par. However, unsatisfiable 3SAT problems found that backbone-bart guidance increases the solver's runtime be approximately 10%. Backbone predictions therefore not useful guidance signal this instance type when working with strong base solver, such as March. Our RLAF-based policy does not share this problem. On the 3COL and CRYPTO distributions, the RLAF-trained policy consistently outperforms the guidance based on UNSAT core prediction, as for the Glucose base solver.
B.6 COMPARISON TO GRAPH-Q-SAT
central design choice in RLAF is one-shot solver guidance: a single GNN forward pass assigns multiplicative variable weights and polarities that are reused at every branching decision with negligible overhead (Section BB.4). Prior RL/GNN methods, such as Graph-Q-SAT (Kurin et al. 2020), couple the GNN tightly the solver by invoking it each guided decision, which can introduce substantial runtime costs. Graph- Q-ST proposes an RL formulation where every solver decision corresponds to one action of an MDP where GNN is tasked with selecting the next branching variable. The model is then trained with standard Q-learning techniques. Note that Q- learning is not applicable for our formulation, which is based on large, combinatorial, and partially continuous action space that is more suitable for policy-gradient methods such as GRPO.
To facilitate a comparison with RLAF within this landscape, we include an evaluation on 3SAT instances from SATLIB. As the public Graph-Q-SAT codebase did not run in our environment, we compare against the reported Graph-Q-S Q-SAT MRIR from Kurin et al. (2020) on the same SAT instances. The base solver is MiniSAT (Eén & Sörensson 2003). which guidance in a manner identical to the guided Glucose solver used in our main experiments. Training uses 800 satisfiable 50-variable 3SAT instances from SATLIB. Evaluation covers 3SAT problems
extended with RLAF
20

---

Published as a conference paper at ICLR 2026
Table 6: SATLIB comparison with the MiniSAT base solver. We report MRIR metric for the compared models (higher is better). We also provide the mean decision counts of the unguided MiniSAT solver as reference.
Dataset
MiniSAT #Decisions
Graph-Q-San
RLAF-SATLIB
RLAF-Main
SAT 100-430
286
3,94
3,14
3.58
SAT 250-1065
76,120
3.91
11.03
7.33
UNSAT 100-430
596
2.24
1.56
2.03
UNSAT 250-1065
182,799
1.54
1.30
1.94
with 250) variables, including both SAT and UNSAT splits. We report MRIR (Mean Relative Improvement in Runtime) as defined by Kurin et al.] (2020), averaging over five independent also evaluate the policy trained for our
RLAF models (denoted RLAF-SATLIB), As reference, main experiments on mixed SAT/UNS data from 3SAT(250), which we denote as RLAF-Main. Note that this policy was learned with the Glucose solver but also capable of guiding the closely related MiniSAT solver effectively.
All learned policies accelerate MiniSAT. On small 100-variable SAT instances, the reported Graph-Q SAT MRIR exceeds RLAF-SATLIB. On larger 250-variable SAT instances, RLAF-SATL.B attains higher MRIR than the reported Graph-Q-Sae indicating strong size generalization for one-shot guidance. For UNSAT, RLAF-SATLIB underperforms the reported Graph-Q-SAT MRIR, consistent with training solely on SAT instances. The solver guidance from our main experiments (RLAF-Main) achieves the highest MRIR the 250-variable UNSAT set, which aligns with its training on mixed SAT/UNSAT data and the consistent solver guidance on long search trajectorics with > 100K branching decisions.
These results support two observations. First, a one-shot mulliplicative-weiitt interface can provide persistent guidance throughout the search while avoiding per-decision GNN calls, achieving clear gains on larger SAT instances. Second, volicy-gradient training over a joint, partially continuous action space is effective for learning guidance that scales in problem size and can transfer across EVSIDS-based solvers. The incurred wall-clock overhead only single forward pass (Section B.4). enabling guidance of all decisions without prohibitive inference costs.
B.7
IMPACT OF WEIGHTS AND POLARITIES
Our learned policies provide both variable weights and polarities guide the solver. Here, we aim to measure the individual impact of these model outputs. To this end, we evaluate the models from our main experiment
modified setting where only the weights or the polarities are provided to the guided solver. We create setting where only the variable weights are used by setting all polarities to In the inverse setting, we set all variable weights to and only use the predicted polaritics.
1000
Guidence
Reterive Decisions to tlse Salver (S)
Liاh 60
50
20
35AT1300) SATISFWALF
35AT1900) UNSATISTIARL
Colo0oi SATISFIALLE Dataset
Colot0n LNSATISFUALE
Crypto7001 UNSAT STARLE
Figure 9: Relative number of decisions compared to the Glucose base solver. Less is better. We compare 3 guidance settings: Using polarities only (p), using weights only (w), and using both weights and polarities (p+w).
21

---

Published as a conference paper at ICLR 2026
Figure provides the test results in both settings well as the default setting where both weights and polarities are used. Overall, we observe that variable weights account for most of the performance gains. On satisfiable 3SAT problems, the polarities do play significant role in accelerating the solver, as using both weights and polarities performs significantly better than using either separately. On the remaining instance distributions, guidance with weights only already achieves the same speed-up as using both weights and polarities. Conceptually, well-chosen variable polarities are most impactful on satisfiable problems with non-empty backbones, and our empirical results reflect this. Variable weights, on the other hand, are ubiquitously useful across instance distributions.
B.8 IMPACT OF THE GNN DEPTH
We further study how the depth the underlying GNN affects the quality of the learned guidance. Recall that this depth set to 10 in main experiments, We train two additional policies guide Glucose on AT with GNN depths of and 5, respectively. Figure [ralprovides the mean number of decisions achieved by each policy the 3SAT(300) test set. We observe that deeper GNNs yield more effective guidance. These results demonstrate that the learned policies effectively exploit the model's depth and incorporate non-trivial structural graph features that GNNs. These results also suggest that scaling up the GNN model in the future may further improve performance.
captured by shallow
Solver
Solver
Glucose
Kesn #Deeciors
Decisions
200000
500000
200000
200000
Glucose
10
of 0.05
of=01
=f=05
(a) Effect of the GNN depth.
(b) Effect of
Figure 10: Ablation experiments on the effects of GNN depth and ot parameter. We report the mean number of decisions achieved on the 3SAT(300) (SAT and UNSAT).
B.9
IMPACT OF "
We further provide data on the impact of the T" hyperparameter, which sets the variance of the LogNormal variable weight distributions. By default, we use fixed value of y% 0.1 in our main experiments, which was determined preliminary tuning runs. To probe the effect of using a wider range of values for " we train two additional policies to guide Glucose on 3SAT with ~% 0.05 and R" 0.5. Both of these additional policies converged stably during training. Figure 10b compares the test results of these policies. We observe that the three policies all successfully accelerate the base solver. The policy trained with xt = 0.05 performs nearly identically to our default of T 0.1, while training with higher value of "" 0.5 does cause degradation. This suggests that successfully training a policy with RLAF does not require the specific choice of " 0.1. However, the test-time performance is somewhat sensitive the choice of this hyperparameter, it should be appropriately tuned for given application of RLAF
performance
22


Reviews:
[{"review_id": "0uiVqDNVvr", "reviewer": "Reviewer_CgoS", "summary": "This paper introduces Reinforcement Learning from Algorithm Feedback (RLAF), a novel paradigm for accelerating SAT solvers by training a Graph Neural Network (GNN) to guide their branching heuristics. Departing from traditional approaches that rely on expert-crafted rules or supervised labels, RLAF formulates solver guidance as a one-shot reinforcement learning problem. Instead of intervening at each decision step, the GNN performs a single pass at the beginning of the search to assign an \"importance score\" (weight) and a \"starting guess\" (polarity) to each variable.\nThese predictions are integrated directly into the branching heuristics of existing solvers. The GNN policy is trained end-to-end using policy-gradient methods, such as GRPO, with the objective of minimizing the solver’s computational cost. The solver's own performance serves as the reward signal, creating a self-improving feedback loop that obviates the need for expert supervision. The experimental evaluation demonstrates consistent speedups across random 3-SAT, graph coloring, and cryptographic SAT problems. Notably, models trained on smaller instances generalize effectively to significantly larger and more difficult unseen problems.", "questions": "1.\tHow stable is RLAF training across random seeds? Does GRPO converge consistently?\n\n2.\tDid the authors attempt fine-tuning across mixed problem distributions (e.g., 3SAT + 3COL)? Given the \"solver-agnostic structural properties\" observed, could the authors comment on whether transfer learning (pre-training a GNN policy on a general SAT solver/distribution and then fine-tuning for specific instances or solvers) is a promising avenue for reducing the training cost and improving generalization further?", "limitations": "", "rating": 6, "confidence": 3, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "-\tThe RLAF paradigm is a novel and effective concept. It learns by using the solver's own performance, i.e., its computational cost, as a reward signal. This help in eliminating the need for costly human labelling or hand-curated features (GNN can train itself).\n-\tThe GNN runs just once per problem to generate a set of hints (weights and polarities) that guide the entire search. It resolves the computational bottleneck of prior RL/GNN methods that required per-decision GNN calls, which often made them slower than the original solver .\n-\tThe proposed mechanism for feeding variable weights and polarities into existing branching heuristics is generic, which allows the learned policies to be applied to different base solvers.\n-\tStrong Empirical Results: The experimental evaluation is comprehensive and interesting. The authors demonstrate substantial speedups across 3 distinct SAT problem distributions and two different base solvers. It also generalizes well to larger and harder unseen instances. RLAF-trained policies also consistently outperforms over supervised approaches.\n-\tClarity and Well-Structured Paper: The paper is clearly structured and well-written. Figures (especially Figs. 2–5) effectively convey key ideas. Mathematical formulations (e.g., the RL setup, Eqns. 6–10) are precise. Overall, its easy to follow.\n-\tDetailed appendices include architecture, solver modification details, and training algorithms. Reproducibility is well-handled.", "weaknesses": "The primary limitations of the work, which the authors are commendably upfront about, relate to the scalability of training and the depth of the methodological analysis. The most significant constraint is the computationally intensive nature of the RL training loop. This currently confines the approach to smaller problem instances, leaving its effectiveness on industrial-scale SAT problems as a crucial direction for future work.\n\nFurthermore, the analysis would benefit from comprehensive ablation studies to better understand the sources of the performance gains. For instance, disentangling the separate impacts of weight and polarity guidance would clarify the mechanics of the learned heuristic. \n\nA sensitivity analysis regarding GNN depth and RL hyperparameters would also be a valuable addition, providing a more complete picture of the model's robustness and helping to guide future work in this direction.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "zLei2PJOaN", "reviewer": "Reviewer_KMQK", "summary": "The paper presents a novel method to combine (graph) neural networks and\na SAT solver. They use the network to predict an \"importance\" of each\nvariable, and then combine this value with SAT solver's inner variable\nevaluation. The approach uses curriculum learning to train the NN with\nRL (GRPO) on easy instance in one of three categories, and show time\nimprovement on harder problems, compared to the base solver as well as\nother approaches.", "questions": "-", "limitations": "", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "* The use of a NN once before the solver doesn't slow down the solver,\n   and directly relates to SOTA methods for SAT solving.\n* The article is well written, including discussing the downsides", "weaknesses": "* Using RL forces the network to be trained only on small SAT instances,\n   so it was not attempted on serious problems.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "gFGRHegV5T", "reviewer": "Reviewer_gUdh", "summary": "This work introduces Reinforcement Learning from Algorithm Feedback (RLAF), a paradigm for learning to guide SAT solver branching heuristics using Graph Neural Networks (GNNs). \n\nThe authors demonstrate that RLAF-trained policies can reduce the mean solve time of various base solvers across a diverse set of SAT problems.\n\nMany branching heuristics-based methods are implemented by starting with selecting a variable \n\\hat{x} = argmax_x Score(x) \nthat maximizes some function Score. \n\nThe authors modify this to incorporate additional variable weights w for the given input formula:\n\\hat{x} = argmax_x w(x) · Score(x)\n\nThis way, we can inject prior knowledge of variable importance into the solver’s branching decisions.\nIn addition to the weights w(x), polarity p(x) can also be assigned to each variable x. When x is chosen as a decision variable, the polarity determines which value is assigned to x first.\n\nThe authors map input formula Phi to a graph representation (“Literal-Clause Graph”) that captures the instance’s structure. This graph is processed by a GNN that extracts structural information.\nThe output of the GNN [mu(x), rho(x)] is used to parameterize variable-wise weight and polarity distributions.\nThe models are trained by RL: the input formula Phi is the state, and a variable parameterization is the action. \nOnce the action is taken, the environment transitions immediately to a terminal state, providing a reward R(Phi, W) = −Cost(Phi, W).", "questions": "•\tHow would the results change if other RL methods were used instead of GRPO?\n•\tHow does the training time scale with problem size? How much faster is training on a GPU compared to a CPU?\n•\tWhat are the main challenges (if any) in developing a distributed version?", "limitations": "", "rating": 6, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "•\tThe paper is well written.\n•\tIt investigates how RL-trained Graph Neural Networks (GNNs) can improve the branching heuristics of SAT solvers.\n•\tThe authors modify existing DPLL-based backtracking SAT solvers to incorporate external variable weights into their branching heuristics.\n•\tThe results demonstrate that, after training, the learned policies generalize well to significantly larger and more challenging problems.\n•\tI particularly appreciate the inclusion of the graph coloring and cryptographic experiments.", "weaknesses": "The work is demonstrated only on small-scale examples, with all training performed on machines equipped with a single multi-core CPU and one GPU. I wish the paper included more numerical experiments on larger-scale problems.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "kketwf5JlX", "reviewer": "Reviewer_j7Rf", "summary": "This paper introduces Reinforcement Learning from Algorithm Feedback (RLAF), a paradigm for training Graph Neural Networks to guide SAT solver branching heuristics through a one-shot mechanism where a single GNN forward pass assigns multiplicative variable weights w(x) and polarities p(x) that persistently influence all branching decisions. The approach modifies existing solvers by scaling their native scoring functions with learned weights, formulating weight selection as a single-step MDP trained with GRPO policy-gradient methods using only solver cost as reward, eliminating expert supervision or predefined properties like UNSAT cores. Training on easy instances with 2000 GRPO iterations sampling M=40 parameterizations across N=100 instances, the policies generalize to larger problems, achieving 69% runtime reduction on 400-variable 3SAT, 2× speedup on 600-vertex graph coloring, and 3× improvement on cryptographic instances. The approach consistently outperforms supervised baselines predicting handcrafted variable properties, with learned weights from different solvers showing high correlation (r=0.73-0.85), suggesting solver-agnostic structural understanding. The one-shot design incurs minimal overhead (0.02-0.1s) versus prior RL methods requiring one GNN pass per decision, enabling practical guidance throughout trajectories exceeding 100K decisions.", "questions": "See the weakness part.", "limitations": "", "rating": 6, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The paper is well-written with good illustration and easy to follow. The paper provides clear algorithmic descriptions (Algorithms 1-3) showing precisely how variable weights are injected into branching heuristics, with Figure 2 effectively illustrating the complete pipeline from graph representation through GNN processing to solver guidance. The background section carefully explains both SAT solving fundamentals and RL formulations, making the paper accessible to readers from either community. Experimental setup is thoroughly documented with comprehensive hyperparameter tables and detailed data generation procedures in the appendix.\n2. The learned policies achieve substantial speedups across diverse problem distributions, including 69% runtime reduction on satisfiable 3SAT(400) instances and more than 2× acceleration on graph coloring and cryptographic problems, while generalizing to instances significantly larger than those seen during training. RLAF consistently outperforms supervised baselines that predict handcrafted heuristics like UNSAT cores and backbones, demonstrating that direct RL optimization yields more effective guidance. The one-shot design incurs negligible overhead (0.02-0.1 seconds) compared to solver runtime, making the approach practically viable.", "weaknesses": "This paper is in general a good paper to me, but I am not an expert in this field. Here I point out some suggestions which I hope could strengthen the paper further.\n\nWhile the paper demonstrates strong results on three well-studied problem classes, the evaluation could be strengthened by including more diverse and realistic industrial SAT benchmarks from domains like hardware verification, software testing, or planning problems from SAT competitions. \n\nFor example, the choice of LogNormal distribution for variable weights (Equation 2) with fixed standard deviation σ_w=0.1 is mentioned to perform best in \"preliminary experiments,\" but no systematic comparison with alternative distributions (e.g., Gamma, truncated Normal) or analysis of sensitivity to σ_w is provided.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)