SAT-ACT：从结果导出的动作偏好中学习 CDCL 分支决策

# SAT-ACT: Learning CDCL Branching from Outcome-Derived Action Preferences
Source: [https://arxiv.org/html/2610.41290](https://arxiv.org/html/2610.41290)
###### Abstract

Learning\-based approaches have increasingly been explored for SAT solving, with particular attention to improving branching decisions in conflict\-driven clause learning \(CDCL\) solvers\. These approaches derive branching guidance either from static structural properties of SAT formulas or from dynamic signals obtained through solver feedback and execution traces\. However, these forms of supervision provide limited evidence about state\-dependent branching effects, while different outcome measures may favor different branching choices\. To address these limitations, we proposeSAT\-ACT, an outcome\-derived learning framework for CDCL branching\. We design three complementary outcome comparison criteria to extract action preferences from independent branching action rollouts initiated at the same solver state\. The criteria identify preferences supported by the outcomes and leave comparisons unresolved when the evidence is insufficient or conflicting, instead of forcing an ordering using a predefined scalar metric\. A state\-conditioned network learns branching priorities from the extracted preferences and uses them to guide CDCL search directly without online action rollouts\. We further introduce non\-dominated heuristic action supervision, which retains the solver\-selected action as a training target only when it remains non\-dominated under these preferences\. Solver\-level experiments show thatSAT\-ACTconsistently reduces CDCL search costs on three SAT families and improves PAR\-2 on the SAT Competition benchmarks\.

## 1Introduction

The Boolean satisfiability problem \(SAT\) is a fundamental problem in computer science with broad applications in planning\([Büttner and Rintanen, 2005](https://arxiv.org/html/2610.41290#bib.bib3)\), verification\([Vizel et al\., 2015](https://arxiv.org/html/2610.41290#bib.bib4)\), and security\([Mironov and Zhang, 2006](https://arxiv.org/html/2610.41290#bib.bib5)\)\. As the first problem shown to be NP\-complete\([Cook, 1971](https://arxiv.org/html/2610.41290#bib.bib2)\), SAT has motivated decades of research on efficient solving algorithms\. Modern SAT solvers are largely built upon conflict\-driven clause learning \(CDCL\), which combines branching, Boolean constraint propagation, conflict analysis, clause learning, and restart mechanisms to solve large and complex instances\([Biere et al\., 2021](https://arxiv.org/html/2610.41290#bib.bib1)\)\. Among these components, branching is particularly consequential because each branching action selects an unassigned variable together with its polarity, and this choice can substantially alter the subsequent search trajectory\. Modern CDCL solvers therefore rely on carefully designed branching heuristics to select these actions\.

Recently, many studies have explored learning\-based approaches to solve SAT instances or enhance SAT solving\([Bünz and Lamm, 2017](https://arxiv.org/html/2610.41290#bib.bib14);[Selsam et al\., 2019](https://arxiv.org/html/2610.41290#bib.bib6);[Amizadeh et al\., 2019](https://arxiv.org/html/2610.41290#bib.bib15);[Li et al\., 2023](https://arxiv.org/html/2610.41290#bib.bib16);[Cameron et al\., 2020](https://arxiv.org/html/2610.41290#bib.bib17);[Selsam and Bjørner, 2019](https://arxiv.org/html/2610.41290#bib.bib7);[Shi et al\., 2023](https://arxiv.org/html/2610.41290#bib.bib12);[Wang et al\., 2024](https://arxiv.org/html/2610.41290#bib.bib8);[Sun et al\., 2026](https://arxiv.org/html/2610.41290#bib.bib27)\)\. A representative line of work learns structural signals from SAT formulas to guide CDCL heuristics\. Such methods predict information related to unsatisfiable cores or backbone variables to assist variable selection and phase initialization\([Selsam and Bjørner, 2019](https://arxiv.org/html/2610.41290#bib.bib7);[Shi et al\., 2023](https://arxiv.org/html/2610.41290#bib.bib12);[Wang et al\., 2024](https://arxiv.org/html/2610.41290#bib.bib8);[Sun et al\., 2026](https://arxiv.org/html/2610.41290#bib.bib27)\)\. More recent approaches instead derive supervision from the solving process itself\. Reinforcement\-learning \(RL\) methods learn branching guidance through solver interaction or solver\-level performance feedback\([Kurin et al\., 2020](https://arxiv.org/html/2610.41290#bib.bib19);[Tönshoff and Grohe, 2026](https://arxiv.org/html/2610.41290#bib.bib21)\), while imitation\-based methods learn branching policies from decisions recorded in CDCL execution traces\([Zhang et al\., 2026](https://arxiv.org/html/2610.41290#bib.bib26)\)\. Together, these developments move learning\-based branching from static formula\-level guidance toward supervision that more directly reflects dynamic CDCL search\.

Although existing learning\-based approaches have improved CDCL branching, they construct supervision at different levels of the solving process\. Methods that learn structural signals from SAT formulas guide variable selection and phase initialization, but these signals do not describe the downstream effect of a branching decision at a dynamic solver state\([Selsam and Bjørner, 2019](https://arxiv.org/html/2610.41290#bib.bib7);[Shi et al\., 2023](https://arxiv.org/html/2610.41290#bib.bib12);[Wang et al\., 2024](https://arxiv.org/html/2610.41290#bib.bib8);[Sun et al\., 2026](https://arxiv.org/html/2610.41290#bib.bib27)\)\. RL\-based methods learn from solver feedback\([Kurin et al\., 2020](https://arxiv.org/html/2610.41290#bib.bib19);[Tönshoff and Grohe, 2026](https://arxiv.org/html/2610.41290#bib.bib21)\), while imitation\-based methods learn from decisions recorded during CDCL execution\([Zhang et al\., 2026](https://arxiv.org/html/2610.41290#bib.bib26)\)\. These forms of supervision reflect solver behavior, but they do not necessarily provide matched outcomes for multiple branching decisions at the same dynamic state\. The effect of a branching decision depends on the current assignments, learned clauses, and search history, so evidence collected from different states or trajectories cannot provide matched comparisons at a particular decision point\. Classical SAT lookahead solvers probe candidate branches through propagation\-based effects\([Heule and van Maaren, 2021](https://arxiv.org/html/2610.41290#bib.bib29);[Biere et al\., 2021](https://arxiv.org/html/2610.41290#bib.bib1)\), while strong branching in mixed\-integer linear programming \(MILP\) evaluates candidate variables under a shared branch\-and\-bound context\([Khalil et al\., 2016](https://arxiv.org/html/2610.41290#bib.bib30);[Gasse et al\., 2019](https://arxiv.org/html/2610.41290#bib.bib31)\)\. These precedents demonstrate the value of assessing candidate decisions under a shared search context\. Existing learning\-based CDCL branching methods, however, still provide limited supervision for distinguishing the downstream effects of the branching decisions available at a dynamic solver state\.

A further challenge lies in deriving reliable supervision from solver outcomes at a dynamic solver state\. Solver outcomes report whether solving terminates and how many conflicts, propagations, decisions, and restarts occur during the evaluation\. These measures describe different aspects of the subsequent search and may favor different branching choices\. Reducing them to a single scalar criterion would impose a fixed tradeoff among different outcome measures\. The key question is therefore when the observed outcomes provide sufficient evidence to prefer one branching choice over another\. A suitable supervision scheme should retain only preferences supported by the observed outcomes and leave comparisons with insufficient or conflicting evidence unordered rather than forcing a complete ordering over the available choices\.

To address these limitations, we proposeSAT\-ACT, a framework for learning CDCL branching from outcome\-derived action preferences\. The framework samples candidate branching actions at selected solver states and runs an independent CDCL rollout for each action from its corresponding state\. The rollout outcomes are examined using three complementary outcome comparison criteria to extract supported action preferences\. To learn branching decisions from these preferences, we develop a CDCL branching action network that encodes the active CNF and dynamic assignment features and produces state\-conditioned scores for branching actions\. The extracted preferences supervise the network through a pairwise ranking objective\. During solving, the learned scores guide branching directly without requiring action rollouts\. To incorporate guidance from the solver’s internal branching heuristic, we introduce non\-dominated heuristic action supervision\. Under this mechanism, the heuristic action is used as a training target only when it remains non\-dominated under the extracted preferences\.

Our main contributions are summarized below\.

- •We introduce an outcome\-derived learning framework for CDCL branching\. The framework uses a state\-conditioned model to score branching actions, while outcome\-derived action preferences supervise the model through a pairwise ranking objective\. During solving, the trained model guides branching directly without online action rollouts\.
- •We design three complementary outcome comparison criteria for extracting supported preferences between branching actions\. These criteria leave action pairs without sufficient evidence unordered and avoid collapsing the observed outcomes into a predefined metric\.
- •We additionally propose non\-dominated heuristic action supervision for the action selected by the solver’s internal branching heuristic\. The heuristic action is retained as a training target only when it remains non\-dominated under the outcome\-derived preferences\.

## 2Preliminaries

#### Boolean Satisfiability Problem \(SAT\)\.

We consider a Boolean formulaϕ\\phiin conjunctive normal form \(CNF\) overNNBoolean variables andMMclauses\([Biere et al\., 2021](https://arxiv.org/html/2610.41290#bib.bib1)\)\. Each variableviv\_\{i\}takes eithertrueorfalse, represented by11and00, respectively\. A CNF formula is a conjunction of clauses, and each clause is a disjunction of literals\. A literalℓ\\ellis either a variableviv\_\{i\}or its negation¬vi\\lnot v\_\{i\}\. These two literals are referred to as the positive and negative literals ofviv\_\{i\}and have opposite polarities\. We useℒ=\{ℓ0,…,ℓ2​N−1\}\\mathcal\{L\}=\\\{\\ell\_\{0\},\\ldots,\\ell\_\{2N\-1\}\\\}to denote the set of all literals and𝒞=\{c0,…,cM−1\}\\mathcal\{C\}=\\\{c\_\{0\},\\ldots,c\_\{M\-1\}\\\}to denote the set of clauses inϕ\\phi\. The SAT problem asks whether there exists an assignment under whichϕ\\phievaluates totrue\. A formula admitting such an assignment issatisfiable\. Otherwise, it isunsatisfiable\.

#### Conflict\-Driven Clause Learning \(CDCL\)\.

CDCL forms the basis of modern SAT solvers\([Biere et al\., 2021](https://arxiv.org/html/2610.41290#bib.bib1)\)\. During solving, CDCL repeatedly performs Boolean constraint propagation and branching decisions, while conflicts trigger conflict analysis, clause learning, and non\-chronological backtracking\. LetStS\_\{t\}denote the dynamic solver state immediately before thett\-th branching decision\. The state contains the current partial assignment, dynamic search information, and the active clause set𝒞t\\mathcal\{C\}\_\{t\}\. The set𝒞t\\mathcal\{C\}\_\{t\}contains the original and learned clauses retained by the solver atStS\_\{t\}\.

#### CDCL Branching Actions\.

At each branching decision, CDCL determines an unassigned variable and its polarity\. These choices are commonly made by separate variable\-selection and phase\-selection heuristics\. For example, Exponential Variable State\-Independent Decaying Sum \(EVSIDS\) maintains activity scores that emphasize recent conflict participation and selects the eligible unassigned variable with the highest activity\([Biere et al\., 2021](https://arxiv.org/html/2610.41290#bib.bib1)\)\. A phase\-selection heuristic then determines its polarity\. We represent these choices jointly as a decision literal, referred to as the*branching action*\. Applying the action assigns the selected literal to true\. Letℬt⊆ℒ\\mathcal\{B\}\_\{t\}\\subseteq\\mathcal\{L\}denote the set of legal branching actions atStS\_\{t\}\. For each eligible unassigned variable,ℬt\\mathcal\{B\}\_\{t\}contains its positive and negative literals\. We denote the action selected by the solver’s internal branching heuristic asatheur∈ℬta\_\{t\}^\{\\mathrm\{heur\}\}\\in\\mathcal\{B\}\_\{t\}\. Different branching actions from the same solver state can produce different propagation effects, search trajectories, and solving outcomes\.

## 3Method

Figure 1:Overview ofSAT\-ACT, an outcome\-derived learning framework for CDCL branching\. Candidate branching actions initiate independent CDCL rollouts from the same solver state\. The rollout outcomes are compared to extract action preferences, which supervise a state\-conditioned branching action network through pairwise ranking\.In this section, we presentSAT\-ACT, an outcome\-derived learning framework for CDCL branching\. At selected solver states, the framework samples candidate branching actions and runs an independent CDCL rollout for each action from its corresponding state\. We compare the rollout outcomes using three complementary criteria to extract supported action preferences, while uncertain comparisons remain unordered\. A CDCL branching action network encodes the active CNF and dynamic assignment features to produce state\-conditioned scores for branching actions\. The extracted preferences supervise the network through a pairwise ranking objective\. We also introduce non\-dominated heuristic action supervision for the action selected by the solver’s internal branching heuristic\. The heuristic action is retained as a training target only when it remains non\-dominated under the extracted preferences\. Figure[1](https://arxiv.org/html/2610.41290#S3.F1)presents an overview of the framework\.

### 3\.1Outcome\-Derived Action Preference Extraction

CDCL branching is state\-dependent, while static supervision or a single observed trajectory provides limited evidence about other legal branching actions available at the same point in the search\. We therefore run independent CDCL rollouts for multiple candidate branching actions from the same dynamic solver state and record their solving outcomes\. Because all rollouts begin from the same state, their outcomes can be compared under a shared search context\. We then apply three complementary outcome comparison criteria to extract supported action preferences while leaving uncertain comparisons unordered\.

We first sample solver states along CDCL search trajectories\. For each sampled stateStS\_\{t\}, we construct a bounded candidate set𝒜t⊆ℬt\\mathcal\{A\}\_\{t\}\\subseteq\\mathcal\{B\}\_\{t\}\. The heuristic actionatheura\_\{t\}^\{\\mathrm\{heur\}\}is retained in𝒜t\\mathcal\{A\}\_\{t\}\. Each actiona∈𝒜ta\\in\\mathcal\{A\}\_\{t\}initiates an independent CDCL rollout fromStS\_\{t\}\. The action is applied as the next branching decision, after which the solver resumes its internal CDCL procedure under a common configuration and rollout budget\. Each rollout produces an outcome

Ot​\(a\)=\(yt​\(a\),Ct​\(a\),Pt​\(a\),Dt​\(a\),Rt​\(a\)\),O\_\{t\}\(a\)=\\bigl\(y\_\{t\}\(a\),C\_\{t\}\(a\),P\_\{t\}\(a\),D\_\{t\}\(a\),R\_\{t\}\(a\)\\bigr\),\(1\)whereyt​\(a\)∈\{SAT,UNSAT,incomplete\}y\_\{t\}\(a\)\\in\\\{\\mathrm\{SAT\},\\mathrm\{UNSAT\},\\mathrm\{incomplete\}\\\}denotes the rollout status, andCt​\(a\)C\_\{t\}\(a\),Pt​\(a\)P\_\{t\}\(a\),Dt​\(a\)D\_\{t\}\(a\), andRt​\(a\)R\_\{t\}\(a\)record the numbers of conflicts, propagations, decisions, and restarts\. The state sampling, candidate construction, and rollout protocol are detailed in Appendix[A](https://arxiv.org/html/2610.41290#A1)\. These rollouts are used only for training\-data collection and are not required during inference\.

For two actionsai,aj∈𝒜ta\_\{i\},a\_\{j\}\\in\\mathcal\{A\}\_\{t\}, we writeai≻Staja\_\{i\}\\succ\_\{S\_\{t\}\}a\_\{j\}when their rollout outcomes provide sufficient evidence for preferringaia\_\{i\}toaja\_\{j\}\. The resulting preference set is

𝒫t=\{\(ai,aj\)∣ai≻Staj\}\.\\mathcal\{P\}\_\{t\}=\\\{\(a\_\{i\},a\_\{j\}\)\\mid a\_\{i\}\\succ\_\{S\_\{t\}\}a\_\{j\}\\\}\.\(2\)Because the observed outcomes may not distinguish every action pair,𝒫t\\mathcal\{P\}\_\{t\}defines a partial preference relation\. Rather than combining the outcome measures into a predefined scalar score, we use three complementary comparison criteria to determine which preferences are supported\.

#### Criterion 1\. Completion \(C1\)\.

Letτt\(a\)=𝕀\[yt\(a\)∈\{SAT,UNSAT\}\]\\tau\_\{t\}\(a\)=\\mathbb\{I\}\[y\_\{t\}\(a\)\\in\\\{\\mathrm\{SAT\},\\mathrm\{UNSAT\}\\\}\]indicate whether the rollout of actionaareaches a terminal result within the rollout budget\. C1 supportsai≻Staja\_\{i\}\\succ\_\{S\_\{t\}\}a\_\{j\}whenτt​\(ai\)\>τt​\(aj\)\\tau\_\{t\}\(a\_\{i\}\)\>\\tau\_\{t\}\(a\_\{j\}\)\. Thus, an action whose rollout reaches SAT or UNSAT is preferred to one whose rollout remains incomplete\. If both rollouts have the same completion status, C1 provides no preference evidence\.

#### Criterion 2\. Trajectory Pareto \(C2\)\.

For each completed rollout, we define the search\-cost vector𝐜t​\(a\)=\(Ct​\(a\),Pt​\(a\),Dt​\(a\),Rt​\(a\)\)\\mathbf\{c\}\_\{t\}\(a\)=\(C\_\{t\}\(a\),P\_\{t\}\(a\),D\_\{t\}\(a\),R\_\{t\}\(a\)\)\. C2 supportsai≻Staja\_\{i\}\\succ\_\{S\_\{t\}\}a\_\{j\}when𝐜t​\(ai\)⪯𝐜t​\(aj\)\\mathbf\{c\}\_\{t\}\(a\_\{i\}\)\\preceq\\mathbf\{c\}\_\{t\}\(a\_\{j\}\)component\-wise and𝐜t​\(ai\)≠𝐜t​\(aj\)\\mathbf\{c\}\_\{t\}\(a\_\{i\}\)\\neq\\mathbf\{c\}\_\{t\}\(a\_\{j\}\)\. This criterion prefers an action only when its rollout requires no more conflicts, propagations, decisions, or restarts and improves at least one of these quantities\. If the two rollouts exhibit trade\-offs across the search\-cost dimensions, C2 provides no preference evidence\.

#### Criterion 3\. Terminal Closure \(C3\)\.

For each completed rollout, we define a terminal\-closure levelκt​\(a\)\\kappa\_\{t\}\(a\)that measures how directly the rollout reaches its final SAT or UNSAT result\. A larger value indicates that less additional search is required after applying the branching action\. The exact terminal\-closure levels are defined in Appendix[A\.4](https://arxiv.org/html/2610.41290#A1.SS4)\. C3 supportsai≻Staja\_\{i\}\\succ\_\{S\_\{t\}\}a\_\{j\}whenκt​\(ai\)\>κt​\(aj\)\\kappa\_\{t\}\(a\_\{i\}\)\>\\kappa\_\{t\}\(a\_\{j\}\)\. Equal terminal\-closure levels provide no preference evidence\.

For each action pair, we combine the evidence provided by the applicable comparison criteria\. The pair\(ai,aj\)\(a\_\{i\},a\_\{j\}\)is added to𝒫t\\mathcal\{P\}\_\{t\}only when at least one criterion supportsai≻Staja\_\{i\}\\succ\_\{S\_\{t\}\}a\_\{j\}and no criterion supports the opposite direction\. If no criterion distinguishes the actions or the available evidence is conflicting, the pair remains unordered\.

### 3\.2Learning CDCL Branching from Action Preferences

After extracting outcome\-derived action preferences, we use them to train a state\-conditioned CDCL branching action network\. At solver stateStS\_\{t\}, the network encodes the active CNF and dynamic assignment features to score each legal branching actiona∈ℬta\\in\\mathcal\{B\}\_\{t\}withsθ​\(St,a\)s\_\{\\theta\}\(S\_\{t\},a\), which determines its relative ranking\.

#### Literal–Clause Graph\-Based CDCL State Representation\.

We represent the active CNF atStS\_\{t\}as a literal–clause bipartite graph𝒢t=\(ℒt,𝒞t,ℰt\)\\mathcal\{G\}\_\{t\}=\(\\mathcal\{L\}\_\{t\},\\mathcal\{C\}\_\{t\},\\mathcal\{E\}\_\{t\}\)\. Let𝒱t\\mathcal\{V\}\_\{t\}denote the variables represented in the active CNF, and letℒt=\{v\+,v−∣v∈𝒱t\}\\mathcal\{L\}\_\{t\}=\\\{v^\{\+\},v^\{\-\}\\mid v\\in\\mathcal\{V\}\_\{t\}\\\}contain their positive and negative literals\. The set𝒞t\\mathcal\{C\}\_\{t\}contains the active clauses, and an edge\(ℓ,c\)∈ℰt\(\\ell,c\)\\in\\mathcal\{E\}\_\{t\}indicates that literalℓ\\elloccurs in clausecc\.

Literal\-node features encode the current assignment status and assignment level together with occurrence and global search information\. Clause\-node features encode the clause size, the current assignment composition of its literals, and its satisfaction and near\-unit status\. Detailed definitions of these features are provided in Appendix[B](https://arxiv.org/html/2610.41290#A2)\.

The literal and clause features are projected into a shared embedding space to obtain initial representations𝐡ℓ\(0\)\\mathbf\{h\}^\{\(0\)\}\_\{\\ell\}and𝐡c\(0\)\\mathbf\{h\}^\{\(0\)\}\_\{c\}\. We then apply a NeuroCore\-style message\-passing encoder\([Selsam and Bjørner, 2019](https://arxiv.org/html/2610.41290#bib.bib7)\)\. Literal and clause nodes exchange information along their incidence edges, while each literal also incorporates information from its opposite\-polarity counterpart\. After several rounds, the encoder produces contextual literal and clause embeddings𝐡ℓ\\mathbf\{h\}\_\{\\ell\}and𝐡c\\mathbf\{h\}\_\{c\}\.

#### Polarity\-Aware Branching Action Scoring\.

For each variablevv, let𝐡v\+\\mathbf\{h\}\_\{v^\{\+\}\}and𝐡v−\\mathbf\{h\}\_\{v^\{\-\}\}be its positive and negative literal embeddings\. Polarity\-symmetric variable encoding combines them as

𝐮v=ϕsym​\(\[𝐡v\+\+𝐡v−;\|𝐡v\+−𝐡v−\|\]\),\\mathbf\{u\}\_\{v\}=\\phi\_\{\\mathrm\{sym\}\}\\left\(\\left\[\\mathbf\{h\}\_\{v^\{\+\}\}\+\\mathbf\{h\}\_\{v^\{\-\}\}\\,;\\,\\left\|\\mathbf\{h\}\_\{v^\{\+\}\}\-\\mathbf\{h\}\_\{v^\{\-\}\}\\right\|\\right\]\\right\),\(3\)whereϕsym\\phi\_\{\\mathrm\{sym\}\}is a shared learnable transformation\. The resulting representation is invariant to exchanging the two polarities, while𝐡v\+\\mathbf\{h\}\_\{v^\{\+\}\}and𝐡v−\\mathbf\{h\}\_\{v^\{\-\}\}retain polarity\-specific information\.

Graph\-level context aggregation summarizes the variable and clause representations as

𝐠t=Φgraph​\(\{𝐮v\}v∈𝒱t,\{𝐡c\}c∈𝒞t\)\.\\mathbf\{g\}\_\{t\}=\\Phi\_\{\\mathrm\{graph\}\}\\left\(\\\{\\mathbf\{u\}\_\{v\}\\\}\_\{v\\in\\mathcal\{V\}\_\{t\}\},\\\{\\mathbf\{h\}\_\{c\}\\\}\_\{c\\in\\mathcal\{C\}\_\{t\}\}\\right\)\.\(4\)The graph\-level representation𝐠t\\mathbf\{g\}\_\{t\}captures the global context of the current solver state\.

Graph\-conditioned variable encoding then incorporates this context into each variable representation

𝐮~v=Φvar​\(𝐮v,𝐠t\),\\widetilde\{\\mathbf\{u\}\}\_\{v\}=\\Phi\_\{\\mathrm\{var\}\}\\left\(\\mathbf\{u\}\_\{v\},\\mathbf\{g\}\_\{t\}\\right\),\(5\)whereΦgraph\\Phi\_\{\\mathrm\{graph\}\}andΦvar\\Phi\_\{\\mathrm\{var\}\}are learnable aggregation and conditioning functions\. Their implementations are detailed in Appendix[C](https://arxiv.org/html/2610.41290#A3)\.

For a branching actionaaassociated with variablev⁡\(a\)v\(a\), the network computes

sθ​\(St,a\)=ϕscore​\(\[𝐡a;𝐮~v⁡\(a\);𝐠t\]\)\.s\_\{\\theta\}\(S\_\{t\},a\)=\\phi\_\{\\mathrm\{score\}\}\\left\(\\left\[\\mathbf\{h\}\_\{a\}\\,;\\,\\widetilde\{\\mathbf\{u\}\}\_\{v\(a\)\}\\,;\\,\\mathbf\{g\}\_\{t\}\\right\]\\right\)\.\(6\)The action\-specific literal embedding𝐡a\\mathbf\{h\}\_\{a\}distinguishes the two polarities of the same variable, while𝐮~v⁡\(a\)\\widetilde\{\\mathbf\{u\}\}\_\{v\(a\)\}and𝐠t\\mathbf\{g\}\_\{t\}provide variable\-level and graph\-level context\.

#### Preference\-Guided Action Ranking\.

The preference set𝒫t\\mathcal\{P\}\_\{t\}supervises the relative ordering of the branching\-action scores\. For each\(ai,aj\)∈𝒫t\(a\_\{i\},a\_\{j\}\)\\in\\mathcal\{P\}\_\{t\}withai≻Staja\_\{i\}\\succ\_\{S\_\{t\}\}a\_\{j\}, we define the score difference

Δi​j=sθ​\(St,ai\)−sθ​\(St,aj\)\.\\Delta\_\{ij\}=s\_\{\\theta\}\(S\_\{t\},a\_\{i\}\)\-s\_\{\\theta\}\(S\_\{t\},a\_\{j\}\)\.\(7\)We impose the extracted preference relations through a logistic pairwise ranking objective

ℒpref​\(St\)=1\|𝒫t\|​∑\(ai,aj\)∈𝒫tlog⁡\(1\+exp⁡\(−Δi​j\)\)\.\\mathcal\{L\}\_\{\\mathrm\{pref\}\}\(S\_\{t\}\)=\\frac\{1\}\{\|\\mathcal\{P\}\_\{t\}\|\}\\sum\_\{\(a\_\{i\},a\_\{j\}\)\\in\\mathcal\{P\}\_\{t\}\}\\log\\left\(1\+\\exp\(\-\\Delta\_\{ij\}\)\\right\)\.\(8\)This objective encourages the model to assign higher scores to preferred actions without requiring absolute action\-quality targets\. The loss is averaged within each state so that states with different numbers of supported preference pairs contribute on a comparable scale\. We setℒpref​\(St\)=0\\mathcal\{L\}\_\{\\mathrm\{pref\}\}\(S\_\{t\}\)=0when𝒫t\\mathcal\{P\}\_\{t\}is empty\.

#### Non\-Dominated Heuristic Action Supervision\.

The action selected by the solver’s internal branching heuristic can provide a training target, but it may conflict with the outcome\-derived preferences when an evaluated action is preferred to it\. We therefore retain this supervision only when the heuristic action remains non\-dominated among the evaluated candidates\.

Let𝒩t\\mathcal\{N\}\_\{t\}denote the non\-dominated subset of𝒜t\\mathcal\{A\}\_\{t\}

𝒩t=\{a∈𝒜t\|∄a′∈𝒜tsuch thata′≻Sta\}\.\\mathcal\{N\}\_\{t\}=\\left\\\{a\\in\\mathcal\{A\}\_\{t\}\\;\\middle\|\\;\\nexists\\,a^\{\\prime\}\\in\\mathcal\{A\}\_\{t\}\\text\{ such that \}a^\{\\prime\}\\succ\_\{S\_\{t\}\}a\\right\\\}\.\(9\)Since≻St\\succ\_\{S\_\{t\}\}is a partial preference relation and𝒜t⊆ℬt\\mathcal\{A\}\_\{t\}\\subseteq\\mathcal\{B\}\_\{t\}, membership in𝒩t\\mathcal\{N\}\_\{t\}does not imply global optimality\. It only indicates that no evaluated action is preferred to that action\.

Letatheura\_\{t\}^\{\\mathrm\{heur\}\}denote the heuristic action\. We define the supervision gate as

γt=𝕀\[atheur∈𝒩t\]\.\\gamma\_\{t\}=\\mathbb\{I\}\\left\[a\_\{t\}^\{\\mathrm\{heur\}\}\\in\\mathcal\{N\}\_\{t\}\\right\]\.\(10\)When the heuristic action remains non\-dominated under the outcome\-derived preferences, we use it as a training target through a cross\-entropy objective over the legal branching actions

ℒheur​\(St\)=−log⁡exp⁡sθ​\(St,atheur\)∑a∈ℬtexp⁡sθ​\(St,a\)\.\\mathcal\{L\}\_\{\\mathrm\{heur\}\}\(S\_\{t\}\)=\-\\log\\frac\{\\exp s\_\{\\theta\}\(S\_\{t\},a\_\{t\}^\{\\mathrm\{heur\}\}\)\}\{\\sum\_\{a\\in\\mathcal\{B\}\_\{t\}\}\\exp s\_\{\\theta\}\(S\_\{t\},a\)\}\.\(11\)

#### Overall Training Objective\.

The state\-level training objective combines preference\-guided action ranking with non\-dominated heuristic action supervision

ℒ⁡\(St\)=ℒpref​\(St\)\+λheur​γt​ℒheur​\(St\),\\mathcal\{L\}\(S\_\{t\}\)=\\mathcal\{L\}\_\{\\mathrm\{pref\}\}\(S\_\{t\}\)\+\\lambda\_\{\\mathrm\{heur\}\}\\gamma\_\{t\}\\mathcal\{L\}\_\{\\mathrm\{heur\}\}\(S\_\{t\}\),\(12\)whereλheur\\lambda\_\{\\mathrm\{heur\}\}controls the contribution of heuristic action supervision\.

Together, the two terms train the network to respect outcome\-derived action preferences while retaining compatible guidance from the solver’s internal branching heuristic\.

## 4Experiments

In this section, we present a solver\-level experimental analysis of CDCL branching to evaluate the effectiveness ofSAT\-ACT\.

#### Datasets\.

We use three SAT families from G4SATBench\([Li et al\., 2024](https://arxiv.org/html/2610.41290#bib.bib9)\)\. These families are SR, Community Attachment \(CA\), and Popularity\-Similarity \(PS\)\. For each family, 16,000/2,000/2,000 instances are used for model training, validation, and testing, respectively\. Outcome\-derived branching supervision is collected with an instrumented CaDiCaL solver\([Biere et al\., 2024](https://arxiv.org/html/2610.41290#bib.bib28)\)through independent CDCL rollouts\. Dataset and supervision statistics are provided in Appendix[D](https://arxiv.org/html/2610.41290#A4), with solver sampling and evaluation settings in Appendix[F](https://arxiv.org/html/2610.41290#A6)\.

#### Baselines\.

We compareSAT\-ACTwith native CaDiCaL \(3\.0\.0\), NeuroCore\([Selsam and Bjørner, 2019](https://arxiv.org/html/2610.41290#bib.bib7)\), GQSAT\([Kurin et al\., 2020](https://arxiv.org/html/2610.41290#bib.bib19)\), SATformer\([Shi et al\., 2023](https://arxiv.org/html/2610.41290#bib.bib12)\), ImitSAT\([Zhang et al\., 2026](https://arxiv.org/html/2610.41290#bib.bib26)\), and RLAF\([Tönshoff and Grohe, 2026](https://arxiv.org/html/2610.41290#bib.bib21)\)\. For a consistent solver\-level comparison, all learning\-based methods are integrated with the same CaDiCaL solver while retaining their original guidance mechanisms\. NeuroCore, GQSAT, and ImitSAT guide branching decisions during search, whereas SATformer and RLAF provide one\-shot guidance before search\.

#### Metrics\.

We measure solver performance using the relative changes in conflicts \(ΔC\\Delta\_\{C\}\), decisions \(ΔD\\Delta\_\{D\}\), and propagations \(ΔP\\Delta\_\{P\}\) with respect to native CaDiCaL\. Following ImitSAT\([Zhang et al\., 2026](https://arxiv.org/html/2610.41290#bib.bib26)\), we also report median relative propagation per problem \(MRPP\) and the one\-percent win rate \(W\(1%\)\)\. Detailed metric definitions are provided in Appendix[E](https://arxiv.org/html/2610.41290#A5)\.

#### Implementation Details\.

Our models use 10 message\-passing layers with a hidden dimension of 128\. They are trained with AdamW\([Loshchilov and Hutter, 2019](https://arxiv.org/html/2610.41290#bib.bib33)\)for 50 epochs using a learning rate of10−410^\{\-4\}\. We selectλheur\\lambda\_\{\\mathrm\{heur\}\}from\[0,0\.2\]\[0,0\.2\], whereλheur=0\\lambda\_\{\\mathrm\{heur\}\}=0removes non\-dominated heuristic action supervision and corresponds toSAT\-ACT \(Pref\. Only\)\. For the experiments on SR, CA, and PS, the 3\-call and 5\-call settings allow at most three and five model requests per solver run, respectively, and each run has a 100\-second time limit\. Complete hyperparameter configurations and solver evaluation settings are provided in Appendix[F](https://arxiv.org/html/2610.41290#A6)\.

Table 1:Solver\-level comparison on SR, CA, and PS\. Lower is better forΔC\\Delta\_\{C\},ΔD\\Delta\_\{D\},ΔP\\Delta\_\{P\}, and MRPP, while higher is better for W\(1%\)\.
#### Exp\-1\. Comparison with Existing Methods for CDCL Branching\.

Table[1](https://arxiv.org/html/2610.41290#S4.T1)comparesSAT\-ACTwith native CaDiCaL and learning\-based SAT branching baselines\. On SR and PS,SAT\-ACT\(5\-call\) improves the three aggregate search\-cost metrics over the best competing baseline by 2\.26–4\.34 and 20\.83–21\.62 percentage points, respectively\. On CA, RLAF obtains lower aggregate conflicts and propagations, whereasSAT\-ACT\(5\-call\) achieves better decisions, MRPP, and W\(1%\)\. ForSAT\-ACT, the 5\-call setting generally improves over the 3\-call setting; we analyze the complete budget–performance relationship next\.

The performance differences are consistent with the supervision used by each method\. Structural and trajectory\-level supervision can improve branching, but provides less direct evidence for comparing actions at a dynamic solver state\. ImitSAT encodes the CNF and execution trace as sequences, and the difficulty of modeling long sequences may help explain its weaker performance\. RLAF benefits from complete\-run feedback and persistent global guidance, which appears particularly effective on CA, although its weaker MRPP and W\(1%\) results suggest that these gains are less broadly distributed across instances\. In contrast,SAT\-ACTlearns from state\-matched action outcomes and applies its scores at dynamic decision points, yielding strong performance across the three datasets\. Its smaller gains on CA are consistent with the lower coverage of preference pairs reported in Table[5](https://arxiv.org/html/2610.41290#A4.T5)\. Additional analyses of SAT/UNSAT instances and neural inference cost are provided in Appendices[G\.1](https://arxiv.org/html/2610.41290#A7.SS1)and[G\.5](https://arxiv.org/html/2610.41290#A7.SS5), respectively\.

#### Exp\-2\. Effect of Neural Intervention Budget\.

We next examine how solver performance changes with the maximum number of neural model requests allowed during each solver run\. While Table[1](https://arxiv.org/html/2610.41290#S4.T1)reports the representative 3\-call and 5\-call settings, Figure[2](https://arxiv.org/html/2610.41290#S4.F2)evaluatesSAT\-ACT \(Pref\. Only\)andSAT\-ACTover the complete intervention\-budget range\. Increasing the intervention budget generally leads to larger reductions in conflicts, decisions, and propagations\. The effect is most pronounced on SR and CA, where all three search\-cost metrics improve substantially as the budget increases\. PS exhibits larger fluctuations across neighboring budgets, but higher budgets still outperform very small budgets overall\. Across the tested range,SAT\-ACTgenerally matches or outperformsSAT\-ACT \(Pref\. Only\), especially on SR and CA\. These results show that increasing the neural intervention budget can provide additional reductions in search cost\.

Figure 2:Effect of the neural intervention budget on SR, CA, and PS\. Bars report relative changes in conflicts \(ΔC\\Delta\_\{C\}\), decisions \(ΔD\\Delta\_\{D\}\), and propagations \(ΔP\\Delta\_\{P\}\) with respect to native CaDiCaL\.Table 2:Incremental analysis of outcome comparison criteria\. Lower is better for all metrics\.
#### Exp\-3\. Ablation of Outcome Comparison Criteria\.

We analyze the contribution of the three outcome comparison criteria by progressively incorporating different forms of solving evidence\. We compare C1, C1\+C2, and C1\+C2\+C3 under the 5\-call setting while keeping the model, training procedure, and solver evaluation protocol unchanged\. All variants use preference\-guided action ranking without heuristic action supervision\. The results are reported in Table[2](https://arxiv.org/html/2610.41290#S4.T2)\. These results show that the complete C1\+C2\+C3 combination achieves the strongest reductions in conflicts, decisions, and propagations on all three datasets\. The contribution of each added criterion varies across datasets, but every addition improves all three search\-cost metrics\. This pattern suggests that the three outcome comparison criteria provide complementary supervision, with terminal\-closure information adding useful signals beyond completion and trajectory Pareto evidence\. A complete leave\-one\-out analysis is provided in Appendix[G\.2](https://arxiv.org/html/2610.41290#A7.SS2)\.

Table 3:Ablation of heuristic action supervision strategies\. Lower is better for all metrics\.
#### Exp\-4\. Ablation of Non\-Dominated Heuristic Action Supervision\.

Under the 5\-call setting, we compareSAT\-ACTwith four supervision variants\.*Pref\. Only*trains solely from outcome\-derived action preferences and removes heuristic action supervision\.*Heur\. Only*removes preference supervision and trains only on actions selected by the solver’s internal branching heuristic\.*Pref\. \+ Heur\.*combines preference supervision with every heuristic target, regardless of its relation to the evaluated actions\.*Pref\. \+ RG*instead retains heuristic targets through random gating\. The fullSAT\-ACTmodel uses outcome\-derived preferences to retain a heuristic target only when its action remains non\-dominated\. Table[3](https://arxiv.org/html/2610.41290#S4.T3)reports the results\.*Heur\. Only*and*Pref\. \+ Heur\.*underperform*Pref\. Only*across all three datasets, while random gating yields inconsistent improvements\.SAT\-ACTachieves the bestΔC\\Delta\_\{C\}andΔD\\Delta\_\{D\}on all datasets and the bestΔP\\Delta\_\{P\}on CA and PS, while*Pref\. \+ RG*is slightly better on SR\. These results support filtering heuristic targets with outcome\-derived preferences\. We further examine the sensitivity of non\-dominated heuristic action supervision to its weight under the 5\-call setting\. Figure[3](https://arxiv.org/html/2610.41290#S4.F3)reports the relative change in propagations\. Performance on SR remains stable across the evaluated weights\. CA achieves its largest reductions at moderate weights aroundλheur∈\[0\.05,0\.1\]\\lambda\_\{\\mathrm\{heur\}\}\\in\[0\.05,0\.1\], while PS performs best aroundλheur∈\[0\.015,0\.02\]\\lambda\_\{\\mathrm\{heur\}\}\\in\[0\.015,0\.02\]\. Overall, non\-dominated heuristic action supervision remains effective over a range of moderate weights\. Results for all three search\-cost metrics are provided in Appendix[G\.3](https://arxiv.org/html/2610.41290#A7.SS3)\.

Figure 3:Sensitivity to the heuristic action supervision weight on SR, CA, and PS under the 5\-call setting\. The panels report relative changes in propagations \(ΔP\\Delta\_\{P\}\) with respect to native CaDiCaL\.Table 4:Solver integration results on SAT Competition 2023–2025 instances\. Solved is the sum of SAT and UNSAT results, and lower PAR\-2 is better\.
#### Exp\-5\. Evaluation on SAT Competition Benchmarks\.

We evaluateSAT\-ACTwith CaDiCaL on SAT Competition Main Track111[https://satcompetition\.github\.io/](https://satcompetition.github.io/)instances in 2023–2025\. Each year’s competition contains 400 instances\. Both solvers use the same CaDiCaL configuration and per\-instance time limit, differing only in neural branching guidance\. As shown in Table[4](https://arxiv.org/html/2610.41290#S4.T4), the guided solver matches the number of solved instances on SC\-2023 and solves two and three additional instances on SC\-2024 and SC\-2025, respectively\. It also reduces PAR\-2 on all three benchmark sets\. The independent training setup, evaluation protocol, and neural\-call overhead measurements are provided in Appendix[G\.6](https://arxiv.org/html/2610.41290#A7.SS6)\.

## 5Related Work

In this section, we review related studies on learning\-based approaches for SAT solving\.

End\-to\-End Learning for SAT Solving\.End\-to\-end approaches learn to reason directly over neural representations of SAT instances\. Early methods focus on CNF representations\.[Bünz and Lamm \(2017\)](https://arxiv.org/html/2610.41290#bib.bib14)apply GNNs to satisfiability prediction using a signed\-literal graph with clause co\-occurrence and complementarity edges\. NeuroSAT\([Selsam et al\., 2019](https://arxiv.org/html/2610.41290#bib.bib6)\)uses a literal–clause graph with connections between complementary literals and performs iterative message passing between literal and clause nodes\. Permutation\-invariant architectures have also been developed to learn directly from CNF formulas\([Cameron et al\., 2020](https://arxiv.org/html/2610.41290#bib.bib17)\)\. Another group of methods targets circuit representations\. DG\-DAGRNN\([Amizadeh et al\., 2019](https://arxiv.org/html/2610.41290#bib.bib15)\)represents circuit SAT instances as directed acyclic graphs and learns satisfying assignments with gated recursive networks\. DeepSAT\([Li et al\., 2023](https://arxiv.org/html/2610.41290#bib.bib16)\)instead operates on AND\-inverter graphs and incorporates polarity\-aware representations for Boolean reasoning\. Neural reasoning has also been extended to related satisfiability tasks\. HyperSAT\([Chen et al\., 2025](https://arxiv.org/html/2610.41290#bib.bib13)\)develops an unsupervised hypergraph neural framework for Weighted MaxSAT, while NSNet\([Li and Si, 2022](https://arxiv.org/html/2610.41290#bib.bib24)\)formulates SAT and \#SAT as probabilistic inference with neural belief propagation\. These approaches perform prediction, assignment construction, or optimization directly from the input instance\. Our work instead retains the CDCL solving process and learns to guide branching decisions from dynamic solver states\.

Learning\-Guided SAT Solving\.Learning\-guided methods integrate neural predictions into established SAT solvers\. Beyond branching, learned models have been used to guide restart policies\([Liang et al\., 2018](https://arxiv.org/html/2610.41290#bib.bib18)\)and clause deletion\([Liu et al\., 2024](https://arxiv.org/html/2610.41290#bib.bib20)\)\. Learning\-guided techniques have also been applied to stochastic local search for variable selection\([Yolcu and Póczos, 2019](https://arxiv.org/html/2610.41290#bib.bib22)\)and assignment initialization\([Zhang et al\., 2020](https://arxiv.org/html/2610.41290#bib.bib23)\)\. GraSS\([Zhang et al\., 2024](https://arxiv.org/html/2610.41290#bib.bib25)\)learns solver selection from graph\-based representations\. For CDCL branching, several methods learn structural properties of SAT formulas\. NeuroCore\([Selsam and Bjørner, 2019](https://arxiv.org/html/2610.41290#bib.bib7)\)predicts unsat\-core variables to guide variable selection, while SATformer\([Shi et al\., 2023](https://arxiv.org/html/2610.41290#bib.bib12)\)improves this prediction through transformer\-based representations\.[Sun et al\. \(2026\)](https://arxiv.org/html/2610.41290#bib.bib27)develop polarity\-aware representations over hypergraphs for this task, and NeuroBack\([Wang et al\., 2024](https://arxiv.org/html/2610.41290#bib.bib8)\)predicts backbone phases for phase initialization\. Other methods obtain branching guidance from the solving process\. Graph\-Q\-SAT\([Kurin et al\., 2020](https://arxiv.org/html/2610.41290#bib.bib19)\)learns through reinforcement learning and solver interaction\. RLAF\([Tönshoff and Grohe, 2026](https://arxiv.org/html/2610.41290#bib.bib21)\)uses solver\-level algorithm feedback to predict variable weights and polarities, while ImitSAT\([Zhang et al\., 2026](https://arxiv.org/html/2610.41290#bib.bib26)\)learns branching decisions from CDCL execution traces\.

Candidate evaluation under a shared search context also has precedents in combinatorial search\. Classical SAT lookahead solvers probe candidate branches through propagation\-based effects\([Heule and van Maaren, 2021](https://arxiv.org/html/2610.41290#bib.bib29)\), while strong branching in MILP evaluates candidate variables under a shared branch\-and\-bound context\([Khalil et al\., 2016](https://arxiv.org/html/2610.41290#bib.bib30);[Gasse et al\., 2019](https://arxiv.org/html/2610.41290#bib.bib31)\)\. These precedents demonstrate the value of comparing candidate decisions under a shared search context\. Inspired by these precedents, we construct partial action preferences from state\-matched rollout outcomes at dynamic CDCL states and use them to train a branching policy that operates without online candidate probing\.

## 6Conclusion

In this paper, we presentedSAT\-ACT, an outcome\-derived learning framework for CDCL branching\. The framework compares independent rollouts initiated from the same solver state and applies three complementary outcome comparison criteria to derive partial preferences without a predefined scalar action\-quality score\. A state\-conditioned branching action network learns branching priorities from these preferences, while non\-dominated heuristic action supervision retains solver\-heuristic guidance only when the selected choice remains non\-dominated\.

Experiments on three SAT families show thatSAT\-ACTconsistently reduces CDCL search costs relative to native CaDiCaL and compares favorably with existing learning\-based methods\. It also improves PAR\-2 across three SAT Competition benchmarks and increases overall solving coverage\. Ablation studies further demonstrate the contributions of the outcome comparison criteria and non\-dominated heuristic action supervision\. Future work includes reducing offline rollout costs, improving candidate and intervention selection, and extending the framework to broader SAT distributions and solver configurations\.

## AI Use Statement

Generative AI tools were used to support research ideation and execution by assisting with brainstorming, refining methodological choices, and providing feedback on experimental plans and result interpretation\. They were also used to draft portions of the manuscript and revise the authors’ text for clarity and readability\.

We did not use generative AI tools to generate synthetic datasets or formulate or prove mathematical claims\. The remaining required disclosure tasks were either not performed with generative AI or were not applicable to this work\.

The authors reviewed all AI\-assisted suggestions and manuscript text\. Methodological decisions, implementations, experiments, results, and claims were checked by the authors against the source code and experimental records\. The authors determined the final content and take full responsibility for the work\.

## References

- Amizadehet al\.\(2019\)S\. Amizadeh, S\. Matusevych, and M\. WeimerLearning to solve circuit\-sat: an unsupervised differentiable approach\.In7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6\-9, 2019,Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p2.1),[§5](https://arxiv.org/html/2610.41290#S5.p2.1)\.
- Biereet al\.\(2024\)A\. Biere, T\. Faller, K\. Fazekas, M\. Fleury, N\. Froleyks, and F\. PollittCaDiCaL 2\.0\.InComputer Aided Verification \- 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24\-27, 2024, Proceedings, Part I,A\. Gurfinkel and V\. Ganesh \(Eds\.\),Lecture Notes in Computer Science, Vol\.14681,pp\. 133–152\.External Links:[Document](https://dx.doi.org/10.1007/978-3-031-65627-9%5F7)Cited by:[Appendix D](https://arxiv.org/html/2610.41290#A4.p2.1),[§4](https://arxiv.org/html/2610.41290#S4.SS0.SSS0.Px1.p1.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.13.2),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.2.2),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.24.2)\.
- A\. Biere, M\. Heule, H\. van Maaren, and T\. Walsh \(Eds\.\) \(2021\)A\. Biere, M\. Heule, H\. van Maaren, and T\. Walsh \(Eds\.\)Handbook of satisfiability \- second edition\.Frontiers in Artificial Intelligence and Applications, Vol\.336,IOS Press\.External Links:ISBN 978\-1\-64368\-160\-3Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p1.1),[§1](https://arxiv.org/html/2610.41290#S1.p3.1),[§2](https://arxiv.org/html/2610.41290#S2.SS0.SSS0.Px1.p1.1),[§2](https://arxiv.org/html/2610.41290#S2.SS0.SSS0.Px2.p1.1),[§2](https://arxiv.org/html/2610.41290#S2.SS0.SSS0.Px3.p1.1)\.
- Bünz and Lamm \(2017\)B\. Bünz and M\. LammGraph neural networks and boolean satisfiability\.CoRRabs/1702\.03592\.External Links:1702\.03592Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p2.1),[§5](https://arxiv.org/html/2610.41290#S5.p2.1)\.
- Büttner and Rintanen \(2005\)M\. Büttner and J\. RintanenSatisfiability planning with constraints on the number of actions\.InProceedings of the Fifteenth International Conference on Automated Planning and Scheduling \(ICAPS 2005\), June 5\-10 2005, Monterey, California, USA,S\. Biundo, K\. L\. Myers, and K\. Rajan \(Eds\.\),pp\. 292–299\.Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p1.1)\.
- Cameronet al\.\(2020\)C\. Cameron, R\. Chen, J\. S\. Hartford, and K\. Leyton\-BrownPredicting propositional satisfiability via end\-to\-end learning\.InThe Thirty\-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty\-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7\-12, 2020,pp\. 3324–3331\.Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p2.1),[§5](https://arxiv.org/html/2610.41290#S5.p2.1)\.
- Chenet al\.\(2025\)Q\. Chen, S\. Tan, S\. Gao, and J\. LüHyperSAT: unsupervised hypergraph neural networks for weighted maxsat problems\.CoRRabs/2504\.11885\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2504.11885),2504\.11885Cited by:[§5](https://arxiv.org/html/2610.41290#S5.p2.1)\.
- Choet al\.\(2014\)K\. Cho, B\. van Merriënboer, C\. Gulcehre, D\. Bahdanau, F\. Bougares, H\. Schwenk, and Y\. BengioLearning phrase representations using RNN encoder–decoder for statistical machine translation\.InProceedings of the 2014 Conference on Empirical Methods in Natural Language Processing \(EMNLP\),A\. Moschitti, B\. Pang, and W\. Daelemans \(Eds\.\),Doha, Qatar,pp\. 1724–1734\.External Links:[Link](https://aclanthology.org/D14-1179/),[Document](https://dx.doi.org/10.3115/v1/D14-1179)Cited by:[Appendix C](https://arxiv.org/html/2610.41290#A3.p5.2)\.
- Cook \(1971\)S\. A\. CookThe complexity of theorem\-proving procedures\.InProceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3\-5, 1971, Shaker Heights, Ohio, USA,M\. A\. Harrison, R\. B\. Banerji, and J\. D\. Ullman \(Eds\.\),pp\. 151–158\.External Links:[Document](https://dx.doi.org/10.1145/800157.805047)Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p1.1)\.
- Gasseet al\.\(2019\)M\. Gasse, D\. Chételat, N\. Ferroni, L\. Charlin, and A\. LodiExact combinatorial optimization with graph convolutional neural networks\.Advances in neural information processing systems32\.Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p3.1),[§5](https://arxiv.org/html/2610.41290#S5.p4.1)\.
- Giráldez\-Cru and Levy \(2015\)J\. Giráldez\-Cru and J\. LevyA modularity\-based random SAT instances generator\.InProceedings of the Twenty\-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25\-31, 2015,Q\. Yang and M\. J\. Wooldridge \(Eds\.\),pp\. 1952–1958\.Cited by:[Appendix D](https://arxiv.org/html/2610.41290#A4.p1.1)\.
- Giráldez\-Cru and Levy \(2017\)J\. Giráldez\-Cru and J\. LevyLocality in random sat instances\.InProceedings of the Twenty\-Sixth International Joint Conference on Artificial Intelligence, IJCAI\-17,pp\. 638–644\.External Links:[Document](https://dx.doi.org/10.24963/ijcai.2017/89)Cited by:[Appendix D](https://arxiv.org/html/2610.41290#A4.p1.1)\.
- Heule and van Maaren \(2021\)M\. J\. H\. Heule and H\. van MaarenLook\-ahead based SAT solvers\.InHandbook of Satisfiability \- Second Edition,A\. Biere, M\. Heule, H\. van Maaren, and T\. Walsh \(Eds\.\),Frontiers in Artificial Intelligence and Applications, Vol\.336,pp\. 183–212\.External Links:[Document](https://dx.doi.org/10.3233/FAIA200988)Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p3.1),[§5](https://arxiv.org/html/2610.41290#S5.p4.1)\.
- Jeroslow and Wang \(1990\)R\. G\. Jeroslow and J\. WangSolving propositional satisfiability problems\.Ann\. Math\. Artif\. Intell\.1,pp\. 167–187\.External Links:[Document](https://dx.doi.org/10.1007/BF01531077)Cited by:[§A\.2](https://arxiv.org/html/2610.41290#A1.SS2.SSS0.Px1.p1.1)\.
- Khalilet al\.\(2016\)E\. Khalil, P\. Le Bodic, L\. Song, G\. Nemhauser, and B\. DilkinaLearning to branch in mixed integer programming\.InProceedings of the AAAI conference on artificial intelligence,Vol\.30\.Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p3.1),[§5](https://arxiv.org/html/2610.41290#S5.p4.1)\.
- Kurinet al\.\(2020\)V\. Kurin, S\. Godil, S\. Whiteson, and B\. CatanzaroCan q\-learning with graph networks learn a generalizable branching heuristic for a SAT solver?\.InAdvances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6\-12, 2020, virtual,Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p2.1),[§1](https://arxiv.org/html/2610.41290#S1.p3.1),[§4](https://arxiv.org/html/2610.41290#S4.SS0.SSS0.Px2.p1.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.16.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.17.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.27.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.28.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.5.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.6.1),[§5](https://arxiv.org/html/2610.41290#S5.p3.1)\.
- Liet al\.\(2023\)M\. Li, Z\. Shi, Q\. Lai, S\. Khan, S\. Cai, and Q\. XuOn eda\-driven learning for SAT solving\.In60th ACM/IEEE Design Automation Conference, DAC 2023, San Francisco, CA, USA, July 9\-13, 2023,pp\. 1–6\.External Links:[Document](https://dx.doi.org/10.1109/DAC56929.2023.10248001)Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p2.1),[§5](https://arxiv.org/html/2610.41290#S5.p2.1)\.
- Liet al\.\(2024\)Z\. Li, J\. Guo, and X\. SiG4SATBench: benchmarking and advancing SAT solving with graph neural networks\.Trans\. Mach\. Learn\. Res\.2024\.Cited by:[Appendix D](https://arxiv.org/html/2610.41290#A4.p1.1),[§4](https://arxiv.org/html/2610.41290#S4.SS0.SSS0.Px1.p1.1)\.
- Li and Si \(2022\)Z\. Li and X\. SiNSNet: A general neural probabilistic framework for satisfiability problems\.InAdvances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 \- December 9, 2022,S\. Koyejo, S\. Mohamed, A\. Agarwal, D\. Belgrave, K\. Cho, and A\. Oh \(Eds\.\),Cited by:[§5](https://arxiv.org/html/2610.41290#S5.p2.1)\.
- Lianget al\.\(2018\)J\. H\. Liang, C\. Oh, M\. Mathew, C\. Thomas, C\. Li, and V\. GaneshMachine learning\-based restart policy for cdcl sat solvers\.InInternational Conference on Theory and Applications of Satisfiability Testing,pp\. 94–110\.Cited by:[§5](https://arxiv.org/html/2610.41290#S5.p3.1)\.
- Liuet al\.\(2024\)H\. Liu, P\. Xu, Y\. Pu, L\. Yin, H\. Zhen, M\. Yuan, T\. Ho, and B\. YuNeuroSelect: learning to select clauses in SAT solvers\.InProceedings of the 61st ACM/IEEE Design Automation Conference, DAC 2024, San Francisco, CA, USA, June 23\-27, 2024,V\. De \(Ed\.\),pp\. 131:1–131:6\.External Links:[Document](https://dx.doi.org/10.1145/3649329.3656250)Cited by:[§5](https://arxiv.org/html/2610.41290#S5.p3.1)\.
- Loshchilov and Hutter \(2019\)I\. Loshchilov and F\. HutterDecoupled weight decay regularization\.In7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6\-9, 2019,Cited by:[§4](https://arxiv.org/html/2610.41290#S4.SS0.SSS0.Px4.p1.1)\.
- Mironov and Zhang \(2006\)I\. Mironov and L\. ZhangApplications of sat solvers to cryptanalysis of hash functions\.InInternational Conference on Theory and Applications of Satisfiability Testing,pp\. 102–115\.Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p1.1)\.
- Selsam and Bjørner \(2019\)D\. Selsam and N\. BjørnerGuiding high\-performance sat solvers with unsat\-core predictions\.InInternational conference on theory and applications of satisfiability testing,pp\. 336–353\.Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p2.1),[§1](https://arxiv.org/html/2610.41290#S1.p3.1),[§3\.2](https://arxiv.org/html/2610.41290#S3.SS2.SSS0.Px1.p3.1),[§4](https://arxiv.org/html/2610.41290#S4.SS0.SSS0.Px2.p1.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.14.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.15.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.25.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.26.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.3.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.4.1),[§5](https://arxiv.org/html/2610.41290#S5.p3.1)\.
- Selsamet al\.\(2019\)D\. Selsam, M\. Lamm, B\. Bünz, P\. Liang, L\. de Moura, and D\. L\. DillLearning a SAT solver from single\-bit supervision\.In7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6\-9, 2019,Cited by:[Appendix D](https://arxiv.org/html/2610.41290#A4.p1.1),[§1](https://arxiv.org/html/2610.41290#S1.p2.1),[§5](https://arxiv.org/html/2610.41290#S5.p2.1)\.
- Shiet al\.\(2023\)Z\. Shi, M\. Li, Y\. Liu, S\. Khan, J\. Huang, H\. Zhen, M\. Yuan, and Q\. XuSATformer: transformer\-based UNSAT core learning\.InIEEE/ACM International Conference on Computer Aided Design, ICCAD 2023, San Francisco, CA, USA, October 28 \- Nov\. 2, 2023,pp\. 1–4\.External Links:[Document](https://dx.doi.org/10.1109/ICCAD57390.2023.10323731)Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p2.1),[§1](https://arxiv.org/html/2610.41290#S1.p3.1),[§4](https://arxiv.org/html/2610.41290#S4.SS0.SSS0.Px2.p1.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.18.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.29.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.7.1),[§5](https://arxiv.org/html/2610.41290#S5.p3.1)\.
- Sunet al\.\(2026\)Z\. Sun, S\. Ma, P\. Lu, and C\. TaoUnsat core prediction through polarity\-aware representation learning over clause\-literal hypergraphs\.InForty\-third International Conference on Machine Learning,External Links:[Link](https://openreview.net/forum?id=YdQq7DvUfI)Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p2.1),[§1](https://arxiv.org/html/2610.41290#S1.p3.1),[§5](https://arxiv.org/html/2610.41290#S5.p3.1)\.
- Tönshoff and Grohe \(2026\)J\. Tönshoff and M\. GroheLearning from algorithm feedback: one\-shot sat solver guidance with gnns\.InInternational Conference on Learning Representations,Vol\.2026,pp\. 98621–98642\.Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p2.1),[§1](https://arxiv.org/html/2610.41290#S1.p3.1),[§4](https://arxiv.org/html/2610.41290#S4.SS0.SSS0.Px2.p1.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.10.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.21.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.32.1),[§5](https://arxiv.org/html/2610.41290#S5.p3.1)\.
- Vizelet al\.\(2015\)Y\. Vizel, G\. Weissenbacher, and S\. MalikBoolean satisfiability solvers and their applications in model checking\.Proc\. IEEE103\(11\),pp\. 2021–2035\.External Links:[Document](https://dx.doi.org/10.1109/JPROC.2015.2455034)Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p1.1)\.
- Wanget al\.\(2024\)W\. Wang, Y\. Hu, M\. Tiwari, S\. Khurshid, K\. L\. McMillan, and R\. MiikkulainenNeuroBack: improving CDCL SAT solving using graph neural networks\.InThe Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7\-11, 2024,Cited by:[§1](https://arxiv.org/html/2610.41290#S1.p2.1),[§1](https://arxiv.org/html/2610.41290#S1.p3.1),[§5](https://arxiv.org/html/2610.41290#S5.p3.1)\.
- Yolcu and Póczos \(2019\)E\. Yolcu and B\. PóczosLearning local search heuristics for boolean satisfiability\.InAdvances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8\-14, 2019, Vancouver, BC, Canada,H\. M\. Wallach, H\. Larochelle, A\. Beygelzimer, F\. d’Alché\-Buc, E\. B\. Fox, and R\. Garnett \(Eds\.\),pp\. 7990–8001\.Cited by:[§5](https://arxiv.org/html/2610.41290#S5.p3.1)\.
- Zhanget al\.\(2020\)W\. Zhang, Z\. Sun, Q\. Zhu, G\. Li, S\. Cai, Y\. Xiong, and L\. ZhangNLocalSAT: boosting local search with solution prediction\.InProceedings of the Twenty\-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020,C\. Bessiere \(Ed\.\),pp\. 1177–1183\.External Links:[Document](https://dx.doi.org/10.24963/IJCAI.2020/164)Cited by:[§5](https://arxiv.org/html/2610.41290#S5.p3.1)\.
- Zhanget al\.\(2026\)Z\. Zhang, H\. Liu, Y\. Yu, J\. Chen, and X\. XuBoolean satisfiability via imitation learning\.InInternational Conference on Learning Representations,Vol\.2026,pp\. 43867–43889\.Cited by:[Appendix E](https://arxiv.org/html/2610.41290#A5.p1.1),[§1](https://arxiv.org/html/2610.41290#S1.p2.1),[§1](https://arxiv.org/html/2610.41290#S1.p3.1),[§4](https://arxiv.org/html/2610.41290#S4.SS0.SSS0.Px2.p1.1),[§4](https://arxiv.org/html/2610.41290#S4.SS0.SSS0.Px3.p1.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.19.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.20.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.30.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.31.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.8.1),[Table 1](https://arxiv.org/html/2610.41290#S4.T1.2.9.1),[§5](https://arxiv.org/html/2610.41290#S5.p3.1)\.
- Zhanget al\.\(2024\)Z\. Zhang, D\. Chételat, J\. Cotnareanu, A\. Ghose, W\. Xiao, H\. Zhen, Y\. Zhang, J\. Hao, M\. Coates, and M\. YuanGraSS: combining graph neural networks with expert knowledge for SAT solver selection\.InProceedings of the 30th ACM SIGKDD Conference on Knowledge Discovery and Data Mining, KDD 2024, Barcelona, Spain, August 25\-29, 2024,R\. Baeza\-Yates and F\. Bonchi \(Eds\.\),pp\. 6301–6311\.External Links:[Document](https://dx.doi.org/10.1145/3637528.3671627)Cited by:[§5](https://arxiv.org/html/2610.41290#S5.p3.1)\.

## Appendix AAdditional Details of Outcome Collection and Action Preference Extraction

This section provides additional details of outcome collection and action preference extraction in Section[3\.1](https://arxiv.org/html/2610.41290#S3.SS1)\. We describe how decision states and candidate branching actions are selected, how independent rollouts are run from the same solver state, how the rollout budget is defined, and how terminal\-closure levels are determined\.

### A\.1Decision\-State Sampling

For each solver run, we retain a small number of decision states distributed across different stages of the search\. Early decision states are always represented, while additional states are sampled from later parts of the search trajectory\. We also retain states reached after restarts so that the collected states cover both the initial search phase and later search contexts\.

Each retained state corresponds to the solver stateStS\_\{t\}immediately before a branching decision\. The state contains the active clauses, current partial assignment, decision trail, variable activities, saved phases, and other dynamic search information accumulated during CDCL solving\.

### A\.2Candidate Branching Action Sampling and Rollouts

Letℬt\\mathcal\{B\}\_\{t\}denote the legal branching actions atStS\_\{t\}\. We construct a bounded candidate set

𝒜t=\{at1,…,atKt\},𝒜t⊆ℬt\.\\mathcal\{A\}\_\{t\}=\\\{a\_\{t\}^\{1\},\\ldots,a\_\{t\}^\{K\_\{t\}\}\\\},\\qquad\\mathcal\{A\}\_\{t\}\\subseteq\\mathcal\{B\}\_\{t\}\.\(13\)
#### Candidate construction\.

We combine the branching variable selected by the solver’s internal heuristic with activity\-based, residual Jeroslow–Wang \(JW\)\([Jeroslow and Wang, 1990](https://arxiv.org/html/2610.41290#bib.bib32)\), and pseudorandom proposals\. The heuristic variable preserves the solver’s reference action\. Activity reflects accumulated search history, residual JW captures the current unsatisfied\-clause structure, and random proposals broaden coverage beyond the heuristic rankings\. This mixture is a practical design under a limited rollout budget; we do not claim that these sources are optimal or exhaustive\.

We first retain the heuristic variable\. We then construct three proposal pools with up to eight legal branching variables in each pool\. The pools contain the highest\-activity variables, the highest\-scoring variables under residual JW, and a reproducible pseudorandom selection\. For residual JW, each unsatisfied active clause contributes2−r2^\{\-r\}to each of its unassigned active literals, whererris the number of such literals in the clause\. A variable is ranked by the larger of its two literal scores\.

Starting with the heuristic variable, we add previously unselected variables in round\-robin order across the activity, JW, and random proposals until eight distinct variables have been retained or the pools are exhausted\. This interleaving prevents an earlier proposal source from filling the entire candidate budget before the others are considered\. We run a separate rollout for each polarity of every retained variable, yieldingKt≤16K\_\{t\}\\leq 16distinct branching actions\. The heuristic action is therefore retained in𝒜t\\mathcal\{A\}\_\{t\}\. An additional unforced solver continuation is recorded separately as a baseline and does not define another action in𝒜t\\mathcal\{A\}\_\{t\}\.

#### State reconstruction\.

For every action rollout, we reconstruct the target pre\-action state by deterministic re\-execution rather than by loading a solver snapshot\. We launch a fresh solver process, load the original CNF, and re\-execute the original search using the same solver binary, configuration, and random seed as in state collection\. No candidate intervention is applied before reaching the target\. Re\-executing the search prefix regenerates the active clause database, partial assignment, decision trail, variable activities, and saved phases through the solver’s normal updates; it is not merely a reassignment of recorded decision literals\. At the target decision point, we check consistency with the recorded state locator before applying the candidate action\. Variable activities and saved phases are reconstructed through deterministic execution rather than separately loaded or directly checked by the locator\. For offline data collection, we use CaDiCaL 3\.0\.0 inplainmode with seed 1 andstabilizeonly=1\.

#### Action intervention and rollout\.

At the reconstructed stateStS\_\{t\}, we override exactly one branching decision with the candidate literala∈𝒜ta\\in\\mathcal\{A\}\_\{t\}\. This is an ordinary, backtrackable decision, not an assumption or an added unit clause\. Subsequent decisions follow the solver’s internal CDCL procedure, and normal CDCL backtracking may undo the intervention and earlier non\-root assignments\. Thus, a completed rollout reports the global SAT/UNSAT result of the original instance, not the satisfiability of a formula conditioned on the candidate literal\. Completed rollouts for the same instance therefore share its global SAT/UNSAT result; actions differ in whether they finish within the budget and in the search effort required\.

Each rollout records its solving status and the numbers of conflicts, propagations, decisions, and restarts, corresponding toOt​\(a\)O\_\{t\}\(a\)in Section[3\.1](https://arxiv.org/html/2610.41290#S3.SS1)\. These counters are measured relative to the pre\-action state, excluding the replay prefix, and the decision count includes the intervened decision itself\. A rollout is labeled SAT or UNSAT if it reaches a terminal result within the rollout budget, and incomplete if a budget limit terminates it before a terminal result is reached\. All candidate actions rolled out from the same state use the same solver configuration and rollout budget, as specified in Appendix[A\.3](https://arxiv.org/html/2610.41290#A1.SS3)\. Preference pairs are extracted only between actions rolled out from the same pre\-action state; no cross\-state or cross\-instance cost comparisons are used to assign preference labels\.

### A\.3Rollout Budget

To bound the cost of action rollouts, each rollout is executed under a fixed rollout budget\. We represent the budget as

𝐛roll=\(Clim,Dlim,Plim,Tlim\),\\mathbf\{b\}\_\{\\mathrm\{roll\}\}=\\left\(C\_\{\\mathrm\{lim\}\},D\_\{\\mathrm\{lim\}\},P\_\{\\mathrm\{lim\}\},T\_\{\\mathrm\{lim\}\}\\right\),\(14\)whereClimC\_\{\\mathrm\{lim\}\},DlimD\_\{\\mathrm\{lim\}\}, andPlimP\_\{\\mathrm\{lim\}\}denote the maximum numbers of conflicts, decisions, and propagations allowed during the rollout, respectively, andTlimT\_\{\\mathrm\{lim\}\}denotes the maximum rollout time\. For offline supervision collection, we use propagation horizons of 1,000, 15,000, and 5,000 for CA, PS, and SR, respectively, with a 300\-second rollout timeout and no conflict or decision limit\.

These quantities are measured from the point at which the candidate branching action is applied\. The rollout terminates when the solver reaches SAT or UNSAT or when one of the prescribed limits is reached\. Accordingly, the solving status is defined as

yt​\(a\)=\{SAT,if the rollout reaches a satisfying assignment,UNSAT,if the rollout proves unsatisfiability,incomplete,if a rollout limit is reached before termination\.y\_\{t\}\(a\)=\\begin\{cases\}\\mathrm\{SAT\},&\\text\{if the rollout reaches a satisfying assignment\},\\\\ \\mathrm\{UNSAT\},&\\text\{if the rollout proves unsatisfiability\},\\\\ \\mathrm\{incomplete\},&\\text\{if a rollout limit is reached before termination\}\.\\end\{cases\}\(15\)
The same rollout budget is applied to the candidate actions rolled out from the same solver state\. For an incomplete rollout, the solver statistics observed before reaching the rollout limit are retained as part ofOt​\(a\)O\_\{t\}\(a\)\.

### A\.4Terminal Closure

Terminal closure provides additional evidence about how directly a completed rollout reaches its final SAT or UNSAT result\. The decision countDt​\(a\)D\_\{t\}\(a\)includes the forced branching decision itself\. Therefore,

indicates that no additional branching decision is required after applyingaa\.

For a SAT rollout, we define the terminal\-closure level as

κt​\(a\)=\{2,Ct\(a\)=0,Rt\(a\)=0,Dt\(a\)=1,1,Ct\(a\)=0,Rt\(a\)=0,Dt\(a\)\>1,0,Ct​\(a\)\>0​or​Rt​\(a\)\>0\.\\kappa\_\{t\}\(a\)=\\begin\{cases\}2,&C\_\{t\}\(a\)=0,\\;R\_\{t\}\(a\)=0,\\;D\_\{t\}\(a\)=1,\\\\ 1,&C\_\{t\}\(a\)=0,\\;R\_\{t\}\(a\)=0,\\;D\_\{t\}\(a\)\>1,\\\\ 0,&C\_\{t\}\(a\)\>0\\;\\text\{or\}\\;R\_\{t\}\(a\)\>0\.\\end\{cases\}\(17\)
The highest level corresponds to a satisfying assignment reached without any additional branching decision, conflict, or restart\. The intermediate level corresponds to a conflict\-free and restart\-free rollout that still requires additional branching\. A rollout containing a conflict or restart receives the lowest SAT closure level\.

For an UNSAT rollout, we define

κt​\(a\)=\{1,Dt​\(a\)=1,0,Dt​\(a\)\>1\.\\kappa\_\{t\}\(a\)=\\begin\{cases\}1,&D\_\{t\}\(a\)=1,\\\\ 0,&D\_\{t\}\(a\)\>1\.\\end\{cases\}\(18\)
The higher UNSAT closure level is assigned when the forced action leads to the terminal contradiction without another branching decision\. Otherwise, the action receives the lower level\. Conflicts are not used to distinguish UNSAT closure levels because reaching an UNSAT result in CDCL necessarily involves conflict\-based reasoning\.

For two completed actionsaia\_\{i\}andaja\_\{j\}, a higher terminal\-closure level provides preference evidence in favor of that action\. Formally,

κt\(ai\)\>κt\(aj\)⟹ai≻Staj\.\\kappa\_\{t\}\(a\_\{i\}\)\>\\kappa\_\{t\}\(a\_\{j\}\)\\quad\\Longrightarrow\\quad a\_\{i\}\\succ\_\{S\_\{t\}\}a\_\{j\}\.\(19\)Equal closure levels provide no additional preference evidence\.

## Appendix BNode Features for Dynamic CDCL States

We provide the detailed node features used for the dynamic CDCL state representation in Section[3\.2](https://arxiv.org/html/2610.41290#S3.SS2)\. The features describe the current assignment, local formula structure, and global search context\. Normalized quantities are denoted by⋅~\\widetilde\{\\cdot\}\.

### B\.1Literal Features

For a literalℓ\\ellassociated with variablevv, we use

𝐱ℓL=\[uℓ,tℓ,fℓ,d~vasg,o~ℓ,log⁡\(1\+oℓ\),log⁡\(1\+\|𝒱t\|\),log⁡\(1\+\|𝒞t\|\),ρt,d~t\]\.\\mathbf\{x\}^\{L\}\_\{\\ell\}=\\left\[u\_\{\\ell\},t\_\{\\ell\},f\_\{\\ell\},\\widetilde\{d\}^\{\\,\\mathrm\{asg\}\}\_\{v\},\\widetilde\{o\}\_\{\\ell\},\\log\(1\+o\_\{\\ell\}\),\\log\(1\+\|\\mathcal\{V\}\_\{t\}\|\),\\log\(1\+\|\\mathcal\{C\}\_\{t\}\|\),\\rho\_\{t\},\\widetilde\{d\}\_\{t\}\\right\]\.\(20\)
Here,uℓu\_\{\\ell\},tℓt\_\{\\ell\}, andfℓf\_\{\\ell\}indicate whether the literal is unassigned, true, or false under the current partial assignment\.d~vasg\\widetilde\{d\}^\{\\,\\mathrm\{asg\}\}\_\{v\}denotes the normalized assignment level of variablevv\.oℓo\_\{\\ell\}ando~ℓ\\widetilde\{o\}\_\{\\ell\}denote the occurrence count ofℓ\\ellin the active clauses and its normalized counterpart\.ρt\\rho\_\{t\}is the fraction of currently assigned variables, andd~t\\widetilde\{d\}\_\{t\}is the normalized current decision level\. The graph\-size terms provide the current numbers of variables and active clauses on a logarithmic scale\.

### B\.2Clause Features

For a clausecc, letncTn\_\{c\}^\{T\},ncFn\_\{c\}^\{F\}, andncUn\_\{c\}^\{U\}denote the numbers of true, false, and unassigned literals\. Its feature vector is

𝐱cC=\[log⁡\(1\+\|c\|\),ncT\|c\|,ncF\|c\|,ncU\|c\|,qcsat,qc\(1\),qc\(2\)\]\.\\mathbf\{x\}^\{C\}\_\{c\}=\\left\[\\log\(1\+\|c\|\),\\frac\{n\_\{c\}^\{T\}\}\{\|c\|\},\\frac\{n\_\{c\}^\{F\}\}\{\|c\|\},\\frac\{n\_\{c\}^\{U\}\}\{\|c\|\},q\_\{c\}^\{\\mathrm\{sat\}\},q\_\{c\}^\{\(1\)\},q\_\{c\}^\{\(2\)\}\\right\]\.\(21\)
Here,qcsatq\_\{c\}^\{\\mathrm\{sat\}\}indicates whether the clause is currently satisfied, whileqc\(1\)q\_\{c\}^\{\(1\)\}andqc\(2\)q\_\{c\}^\{\(2\)\}indicate unsatisfied clauses with one and two unassigned literals, respectively\.

## Appendix CDetails of Polarity\-Aware Branching Action Scoring

This section provides additional details of the representation modules used for branching\-action scoring in Section[3\.2](https://arxiv.org/html/2610.41290#S3.SS2)\.

For each variablevv, polarity\-symmetric variable encoding constructs

𝐮v=ϕsym​\(\[𝐡v\+\+𝐡v−;\|𝐡v\+−𝐡v−\|\]\)\.\\mathbf\{u\}\_\{v\}=\\phi\_\{\\mathrm\{sym\}\}\\left\(\\left\[\\mathbf\{h\}\_\{v^\{\+\}\}\+\\mathbf\{h\}\_\{v^\{\-\}\}\\,;\\,\\left\|\\mathbf\{h\}\_\{v^\{\+\}\}\-\\mathbf\{h\}\_\{v^\{\-\}\}\\right\|\\right\]\\right\)\.\(22\)
Graph\-level context aggregation first pools the variable and clause representations

𝐦t=∑v∈𝒱t𝐮v\+∑c∈𝒞t𝐡c\|𝒱t\|\+\|𝒞t\|\.\\mathbf\{m\}\_\{t\}=\\frac\{\\sum\_\{v\\in\\mathcal\{V\}\_\{t\}\}\\mathbf\{u\}\_\{v\}\+\\sum\_\{c\\in\\mathcal\{C\}\_\{t\}\}\\mathbf\{h\}\_\{c\}\}\{\|\\mathcal\{V\}\_\{t\}\|\+\|\\mathcal\{C\}\_\{t\}\|\}\.\(23\)
The pooled representation is combined with a learnable global token to obtain the graph\-level context

𝐠t=Φgraph​\(𝐳g,ϕctx​\(𝐦t\)\),\\mathbf\{g\}\_\{t\}=\\Phi\_\{\\mathrm\{graph\}\}\\left\(\\mathbf\{z\}\_\{g\},\\phi\_\{\\mathrm\{ctx\}\}\(\\mathbf\{m\}\_\{t\}\)\\right\),\(24\)where𝐳g\\mathbf\{z\}\_\{g\}is a learnable graph token,ϕctx\\phi\_\{\\mathrm\{ctx\}\}projects the pooled representation, andΦgraph\\Phi\_\{\\mathrm\{graph\}\}is a learnable context aggregation module\.

Graph\-conditioned variable encoding then incorporates this context into each variable representation

𝐮~v=Φvar​\(𝐮v,𝐠t\),\\widetilde\{\\mathbf\{u\}\}\_\{v\}=\\Phi\_\{\\mathrm\{var\}\}\\left\(\\mathbf\{u\}\_\{v\},\\mathbf\{g\}\_\{t\}\\right\),\(25\)whereΦvar\\Phi\_\{\\mathrm\{var\}\}is a shared learnable conditioning module\. In our implementation, both context aggregation modules use GRUs\([Cho et al\., 2014](https://arxiv.org/html/2610.41290#bib.bib34)\)\.

Finally, for a branching actionaaassociated with variablev⁡\(a\)v\(a\), the action score is

sθ​\(St,a\)=ϕscore​\(\[𝐡a;𝐮~v⁡\(a\);𝐠t\]\),s\_\{\\theta\}\(S\_\{t\},a\)=\\phi\_\{\\mathrm\{score\}\}\\left\(\\left\[\\mathbf\{h\}\_\{a\}\\,;\\,\\widetilde\{\\mathbf\{u\}\}\_\{v\(a\)\}\\,;\\,\\mathbf\{g\}\_\{t\}\\right\]\\right\),\(26\)whereϕscore\\phi\_\{\\mathrm\{score\}\}is shared across both polarities\. The action\-specific literal representation𝐡a\\mathbf\{h\}\_\{a\}distinguishes the two polarities of the same variable, while𝐮~v⁡\(a\)\\widetilde\{\\mathbf\{u\}\}\_\{v\(a\)\}and𝐠t\\mathbf\{g\}\_\{t\}provide variable\-level and graph\-level context\.

## Appendix DDatasets and Supervision Statistics

We use the SR, Community Attachment \(CA\), and Popularity\-Similarity \(PS\) families from G4SATBench\([Li et al\., 2024](https://arxiv.org/html/2610.41290#bib.bib9)\)\. Each family contains both SAT and UNSAT instances\. The instances are generated using the SR generator from NeuroSAT\([Selsam et al\., 2019](https://arxiv.org/html/2610.41290#bib.bib6)\), the CA model\([Giráldez\-Cru and Levy, 2015](https://arxiv.org/html/2610.41290#bib.bib10)\), and the PS model\([Giráldez\-Cru and Levy, 2017](https://arxiv.org/html/2610.41290#bib.bib11)\)\. For each family, we use 16,000/2,000/2,000 instances for training, validation, and offline testing, respectively, with balanced SAT and UNSAT instances\. The supervision statistics below aggregate the training, validation, and offline test splits\.

For each instance, an instrumented CaDiCaL solver\([Biere et al\., 2024](https://arxiv.org/html/2610.41290#bib.bib28)\)retains up to six decision states and runs rollouts for up to sixteen candidate branching actions at each retained state\. The resulting upper bounds are 360,000 retained states and 5\.76 million independent CDCL rollouts\. Recording one additional unforced solver continuation at each state gives an upper bound of 6\.12 million solver runs\. These are design upper bounds\. An instance may yield fewer than six retained states, and a state may contain fewer than sixteen candidate actions\. The unforced solver continuation is recorded separately and does not define an additional branching action\.

Each action rollout reconstructs the target state by re\-executing the original search prefix, as described in Appendix[A\.2](https://arxiv.org/html/2610.41290#A1.SS2)\. The three outcome comparison criteria in Section[3\.1](https://arxiv.org/html/2610.41290#S3.SS1)extract partial action preferences from the resulting outcomes\. Raw rollout generation was executed sequentially by family with 20 workers, taking 2 h 22 min for CA, 2 h 07 min for SR, and 2 h 27 min for PS, or approximately 6 h 55 min in total\.

Table[5](https://arxiv.org/html/2610.41290#A4.T5)summarizes the CNF statistics and the resulting outcome\-derived supervision\.

Table 5:Dataset and outcome\-derived supervision statistics\. CNF statistics are reported per instance\. Decision states and rolled\-out actions are reported after supervision filtering\. A state is included only if it produces at least one preference pair\. Rolled\-out actions count candidate branching actions and exclude the additional unforced solver baseline\. Criterion coverage is measured over all action pairs within these retained states, and the three criteria are not mutually exclusive\.
## Appendix EEvaluation Metrics

We evaluate solver search cost using conflicts \(CC\), decisions \(DD\), and propagations \(PP\)\. For these quantities, we report the percentage changesΔC\\Delta\_\{C\},ΔD\\Delta\_\{D\}, andΔP\\Delta\_\{P\}relative to native CaDiCaL, computed from the aggregated counts over the evaluated instances\. Negative values indicate reductions in solver cost\. Following ImitSAT\([Zhang et al\., 2026](https://arxiv.org/html/2610.41290#bib.bib26)\), we additionally report the median relative propagation per problem \(MRPP\) and the one\-percent win rate W\(1%\)\. Letℐ\\mathcal\{I\}denote the set of evaluated instances, and letPiP\_\{i\}andPinatP\_\{i\}^\{\\mathrm\{nat\}\}denote the propagation counts of the evaluated method and native CaDiCaL on instanceii, respectively\. MRPP is defined as

MRPP=mediani∈ℐ⁡\(PiPinat\)\.\\mathrm\{MRPP\}=\\operatorname\{median\}\_\{i\\in\\mathcal\{I\}\}\\left\(\\frac\{P\_\{i\}\}\{P\_\{i\}^\{\\mathrm\{nat\}\}\}\\right\)\.\(27\)Values below one indicate fewer propagations than native CaDiCaL on the median instance\.

To capture instance\-wise improvements, we further report the one\-percent win rate\. Following the definition in ImitSAT, with marginδ=0\.01\\delta=0\.01,

W\(1%\)=100\|ℐ\|∑i∈ℐPinat\>0𝕀\[Pi≤\(1−δ\)Pinat\]\.\\mathrm\{W\}\(1\\%\)=\\frac\{100\}\{\|\\mathcal\{I\}\|\}\\sum\_\{\\begin\{subarray\}\{c\}i\\in\\mathcal\{I\}\\\\ P\_\{i\}^\{\\mathrm\{nat\}\}\>0\\end\{subarray\}\}\\mathbb\{I\}\\left\[P\_\{i\}\\leq\(1\-\\delta\)P\_\{i\}^\{\\mathrm\{nat\}\}\\right\]\.\(28\)W\(1%\) therefore measures the percentage of evaluated instances for which the method reduces propagations by at least1%1\\%relative to native CaDiCaL\. Higher values are better\.

## Appendix FExperimental Setup

### F\.1Implementation Details

Our models are implemented in PyTorch with 10 message\-passing rounds and two\-layer MLPs\. The hidden dimension is 128\. Models are trained using AdamW for 50 epochs with a learning rate of10−410^\{\-4\}\. For SR, CA, and PS, we use a batch size of 128, select the weight decay from\{0,10−5,5×10−5,10−4\}\\\{0,10^\{\-5\},5\\times 10^\{\-5\},10^\{\-4\}\\\}, and retain the checkpoint with the lowest validation loss\. The weightλheur\\lambda\_\{\\mathrm\{heur\}\}for non\-dominated heuristic action supervision is selected from\[0,0\.2\]\[0,0\.2\]\. Settingλheur=0\\lambda\_\{\\mathrm\{heur\}\}=0removes this supervision and corresponds toSAT\-ACT \(Pref\. Only\)\. All hyperparameters are selected exclusively on the validation split and fixed before solver\-level test evaluation\. All models are trained on a machine equipped with an Intel Xeon Gold 6148 CPU at 2\.40 GHz and an NVIDIA Tesla V100 PCIe GPU with 32 GB memory\. For the SR, CA, and PS experiments, CaDiCaL runs on the CPU, while neural inference is performed on the GPU\. Code is available at[https://anonymous\.4open\.science/r/SAT\-ACT\-Review\-1DA2](https://anonymous.4open.science/r/SAT-ACT-Review-1DA2)\.

### F\.2Solver Evaluation

All solver\-level evaluations use CaDiCaL 3\.0\.0 withstabilizeonly=1andpreprocesslight=0, while the remaining solver options retain their default values\. For neural intervention, both the node and cell size checks require2​\|𝒱t\|\+\|𝒞t\|\+\|ℰt\|≤2,000,0002\|\\mathcal\{V\}\_\{t\}\|\+\|\\mathcal\{C\}\_\{t\}\|\+\|\\mathcal\{E\}\_\{t\}\|\\leq 2\{,\}000\{,\}000for the literal–clause representation of each active CNF\.

For each SAT family, we randomly sample 200 instances from the test split, with equal numbers of SAT and UNSAT instances\. We repeat the sampling and solver evaluation five times, with all methods evaluated on the same sampled instances and under the same solver settings\. The reported results are averaged across the five runs\.

Each solver run is limited to 100 seconds\. Native CaDiCaL without neural guidance serves as the reference solver for computingΔC\\Delta\_\{C\},ΔD\\Delta\_\{D\},ΔP\\Delta\_\{P\}, MRPP, and W\(1%\)\.

For online branching methods, the 3\-call and 5\-call settings allow at most three and five model requests per solver run, respectively\. Each request counts toward this intervention budget regardless of whether the proposed branching action is ultimately applied by the solver\.

## Appendix GAdditional Experimental Results

### G\.1Analysis of SAT and UNSAT Results

We separately evaluateSAT\-ACTon SAT and UNSAT instances under both 3\-call and 5\-call settings\. We report the same solver\-level cost metrics used in the main comparison\.

Table[6](https://arxiv.org/html/2610.41290#A7.T6)shows thatSAT\-ACTconsistently reduces conflicts, decisions, and propagations on both SAT and UNSAT instances across all three datasets\. The magnitude of the improvement varies across datasets and termination regimes\. This may reflect the different search characteristics of SAT and UNSAT solving, since SAT solving can terminate after finding one satisfying assignment, whereas UNSAT solving requires completing a proof\. Overall, the results show thatSAT\-ACTremains effective under both termination regimes\.

Table 6:SAT and UNSAT subset analysis ofSAT\-ACT\. Lower is better for all metrics\.Table 7:Leave\-one\-out analysis of outcome comparison criteria\. Lower is better for all metrics\.
### G\.2Additional Ablations of Outcome Comparison Criteria

We further analyze the three outcome comparison criteria using leave\-one\-out ablations\. C1, C2, and C3 denote completion, trajectory Pareto, and terminal closure, respectively\. In addition to the full C1\+C2\+C3 combination, we remove each criterion individually and include the C1\-only variant used in the incremental analysis\. All variants share the same model architecture and solver evaluation protocol, with preference\-guided action ranking as the sole training objective\. Table[7](https://arxiv.org/html/2610.41290#A7.T7)provides a consistent picture across datasets and intervention budgets\. The full C1\+C2\+C3 combination achieves the largest reductions in conflicts, decisions, and propagations in every evaluated setting, while removing any individual criterion degrades all three search\-cost metrics\. This indicates that C1, C2, and C3 contribute complementary supervision rather than being interchangeable\.

The relative importance of individual criteria nevertheless varies across datasets and budgets\. C2 is particularly important for CA under the 5\-call setting and for PS under the 3\-call setting, where removing it causes the largest degradation\. By contrast, C1 has a stronger effect on SR with three calls and on PS with five calls\. Removing C3 also consistently weakens performance, although the magnitude of the degradation varies across settings\. Together, these results show that no single outcome comparison criterion explains the overall gain\. Combining completion, trajectory\-level, and terminal evidence yields the most reliable solver\-level improvements across different SAT distributions and intervention budgets\.

Figure 4:Complete sensitivity analysis of the heuristic action supervision weight on SR, CA, and PS under the 5\-call setting\. The plots report relative changes in conflicts \(ΔC\\Delta\_\{C\}\), decisions \(ΔD\\Delta\_\{D\}\), and propagations \(ΔP\\Delta\_\{P\}\) with respect to native CaDiCaL; lower is better\.
### G\.3Sensitivity to Heuristic Action Supervision Weight

Extending the propagation results in Figure[3](https://arxiv.org/html/2610.41290#S4.F3), we evaluate the sensitivity of non\-dominated heuristic action supervision across all three search\-cost metrics under the 5\-call setting\. The preference\-guided ranking objective, model architecture, and evaluation protocol remain fixed whileλheur\\lambda\_\{\\mathrm\{heur\}\}varies\. Figure[G\.2](https://arxiv.org/html/2610.41290#A7.SS2)reports the relative changes in conflicts, decisions, and propagations\. The three solver\-cost metrics exhibit broadly consistent trends across the tested weights\. SR remains relatively stable over the evaluated range\. CA shows comparable performance across moderate weights, with its strongest reductions generally occurring overλheur∈\[0\.05,0\.1\]\\lambda\_\{\\mathrm\{heur\}\}\\in\[0\.05,0\.1\], while PS performs best overλheur∈\[0\.015,0\.02\]\\lambda\_\{\\mathrm\{heur\}\}\\in\[0\.015,0\.02\]\. Increasing the heuristic action supervision weight beyond these ranges does not consistently improve performance\. These results indicate that non\-dominated heuristic action supervision performs best with a moderate weight\.

### G\.4Generalization to Hard Instances

We further evaluate whether the models used in the main experiments generalize to substantially harder SAT instances\. Specifically, we directly apply the same trained models used for the main\-experiment split to the corresponding Hard split, without retraining, fine\-tuning, or adaptation on any Hard instances\. Therefore, this experiment evaluates cross\-difficulty generalization of the learned branching policies rather than performance after additional training on the target split\.

The Hard instances are substantially larger than those in the main\-experiment split\. SR Hard and CA Hard contain 200–400 variables, with average clause counts of 1616\.47 and 4197\.51, respectively, while PS Hard contains 200–300 variables with an average of 1761\.98 clauses\. We use the 3\-call intervention setting for this generalization evaluation\. The results are reported in Table[8](https://arxiv.org/html/2610.41290#A7.T8)\.

Table 8:Direct generalization of the same trained models used in the main experiments to the corresponding Hard splits\.ΔC\\Delta\_\{C\},ΔD\\Delta\_\{D\}, andΔP\\Delta\_\{P\}denote relative changes in conflicts, decisions, and propagations, respectively\. Lower is better forΔC\\Delta\_\{C\},ΔD\\Delta\_\{D\},ΔP\\Delta\_\{P\}, and MRPP; higher is better for W\(1%\)\.The same models used in the main experiments retain clear solver\-level improvements when directly transferred to the Hard splits\. On SR Hard,SAT\-ACTreduces conflicts, decisions, and propagations by 28\.24%, 27\.44%, and 27\.87%, respectively, and also improves MRPP and W\(1%\) overSAT\-ACT \(Pref\. Only\)\. On CA Hard,SAT\-ACTsimilarly achieves larger reductions in all three aggregate search\-cost metrics, although the overall gains are smaller than on SR Hard\.

On PS Hard,SAT\-ACTimproves the reductions in conflicts, decisions, and propagations from 3\.29%, 3\.37%, and 3\.00% withSAT\-ACT \(Pref\. Only\)to 3\.92%, 4\.00%, and 3\.60%, respectively, while slightly improving W\(1%\)\. Its MRPP is slightly worse than that ofSAT\-ACT \(Pref\. Only\), showing that the instance\-level metrics do not improve uniformly\.

Overall, the results show that the branching policies learned in the main experiments remain effective when directly applied to substantially larger Hard instances\. Since exactly the same trained models are used without any specific training or adaptation, these results provide evidence that the trained branching policies generalize beyond the instance scale observed in the main\-experiment split\.

### G\.5Neural Inference Cost

#### Measurement Protocol\.

We compare the neural inference cost ofSAT\-ACTwith NeuroCore, GQSAT, SATformer, ImitSAT, and RLAF\. For methods that provide online branching guidance, we report results under matched 3\-call and 5\-call intervention budgets\. SATformer and RLAF instead perform a single initialization before search\. Inference time is measured by the model service and reported as average accumulated milliseconds per instance\.

#### Inference\-Cost Comparison\.

Table[9](https://arxiv.org/html/2610.41290#A7.T9)reports the neural inference cost on SR, CA, and PS\. These datasets contain relatively small instances that native CaDiCaL often solves within milliseconds\. The neural inference cost therefore outweighs the runtime benefit obtained from the reduced search cost on these instances\. The main results on SR, CA, and PS should consequently be interpreted as improvements in search efficiency rather than end\-to\-end runtime acceleration\.

Under matched intervention budgets, the inference cost ofSAT\-ACTremains comparable to NeuroCore, GQSAT, and ImitSAT and is often lower than that of the latter two methods\. SATformer and RLAF use one\-shot initialization and do not provide repeated guidance at dynamic solver states\. The online inference overhead ofSAT\-ACTis therefore comparable to existing neural methods with similar deployment mechanisms\.

The runtime tradeoff changes on the substantially harder SAT Competition benchmarks analyzed in Appendix[G\.6](https://arxiv.org/html/2610.41290#A7.SS6)\. As shown in Table[4](https://arxiv.org/html/2610.41290#S4.T4), neural guidance reduces PAR\-2 on all three benchmark sets and solves additional SC\-2024 and SC\-2025 instances\. On the 752 instances solved by both configurations, it reduces total runtime by 10\.15% after accounting for neural\-call overhead\. These results show that the search\-time reduction can outweigh neural inference cost on sufficiently challenging SAT instances\.

Table 9:Neural inference cost of learning\-based SAT branching methods\. All values are average accumulated milliseconds per instance\. Lower is better\.

### G\.6SAT Competition Evaluation

#### Training Instances and Data Split\.

This experiment uses an independently constructed training set derived from the SAT Competition Main Track instances released between 2017 and 2022\. We partition the instances into training, validation, and test splits using an 80/10/10 ratio and a split seed of 42\. Before data collection, we retain formulas with at most 200,000 graph nodes and 1,000,000 literal occurrences\. The graph contains two literal nodes for each variable and one node for each clause\. No additional limits are imposed on the CNF file size or maximum clause length\. The filtering process retains 956 formulas that satisfy these constraints and pass DIMACS parsing\.

#### State and Action Collection\.

The SAT Competition data collection uses a larger candidate set and a different rollout budget from the G4SATBench setup\. Each retained state is restricted to 200,000 graph nodes and 1,000,000 literal occurrences\. At most 10 candidate variables are retained at each state, and both polarities initiate separate rollouts\.

State collection and action rollouts use CaDiCaL 3\.0\.0 with its default solver configuration\. Each forced\-action rollout has a timeout of 1,800 seconds\. No conflict, decision, or propagation limit is imposed\. The resulting collection contains 114,120 reliable forced\-action rollouts\.

After removing states without a supported action preference, the resulting dataset contains 2,831 training states, 313 validation states, and 329 test states\. The training, validation, and test splits contain 418,283, 45,312, and 48,272 directed preference pairs, respectively\.

#### Solver Evaluation\.

Each of SC\-2023, SC\-2024, and SC\-2025 contains 400 Main Track instances\. We evaluate native CaDiCaL and CaDiCaL guided bySAT\-ACTon all instances from the three benchmark sets\. Both configurations use CaDiCaL 3\.0\.0 withstabilizeonly=1andpreprocesslight=0\. All remaining solver options retain their default values\. Both CaDiCaL and neural inference run on the CPU in this evaluation\. Each solver run has a time limit of 5,000 seconds and uses the 3\-call setting, allowing at most three neural requests\. The two configurations otherwise use identical solver settings\.

A neural request is permitted only when both the node and cell size checks satisfy2​\|𝒱t\|\+\|𝒞t\|\+\|ℰt\|≤2,000,0002\|\\mathcal\{V\}\_\{t\}\|\+\|\\mathcal\{C\}\_\{t\}\|\+\|\\mathcal\{E\}\_\{t\}\|\\leq 2\{,\}000\{,\}000\. Here,ℰt\\mathcal\{E\}\_\{t\}denotes the literal–clause incidence cells, which correspond to literal occurrences\.

We evaluate aggregate solving time using PAR\-2,

PAR2=1N​∑i=1N\{Ti,if instance​i​is solved,2​Tmax,otherwise,\\mathrm\{PAR2\}=\\frac\{1\}\{N\}\\sum\_\{i=1\}^\{N\}\\begin\{cases\}T\_\{i\},&\\text\{if instance \}i\\text\{ is solved\},\\\\ 2T\_\{\\max\},&\\text\{otherwise\},\\end\{cases\}\(29\)whereTiT\_\{i\}is the runtime of a solved instance andTmax=5,000T\_\{\\max\}=5\{,\}000seconds\. Each timed\-out instance therefore contributes 10,000 seconds\.

#### Neural\-Call Overhead\.

We report the macro\-averaged NN wait ratio,

NN​Wait​Ratio=1N​∑i=1NTNN​\-​wait,iTsolve,i,\\mathrm\{NN\\ Wait\\ Ratio\}=\\frac\{1\}\{N\}\\sum\_\{i=1\}^\{N\}\\frac\{T\_\{\\mathrm\{NN\\text\{\-\}wait\},i\}\}\{T\_\{\\mathrm\{solve\},i\}\},\(30\)which assigns equal weight to each evaluated instance\. We also report the NN call latency,

NN​Call​Latency=∑iTNN​\-​wait,i∑iNRPC​\-​attempts,i\.\\mathrm\{NN\\ Call\\ Latency\}=\\frac\{\\sum\_\{i\}T\_\{\\mathrm\{NN\\text\{\-\}wait\},i\}\}\{\\sum\_\{i\}N\_\{\\mathrm\{RPC\\text\{\-\}attempts\},i\}\}\.\(31\)The latency measures the end\-to\-end solver waiting time for each neural request and covers communication, queueing, input processing, and model inference\. Table[10](https://arxiv.org/html/2610.41290#A7.T10)reports these measurements over all 400 instances in each benchmark set\.

Table 10:Neural\-call overhead for the SAT Competition evaluation\.The NN wait ratios are 11\.99%, 5\.79%, and 7\.92% on SC\-2023, SC\-2024, and SC\-2025, respectively\. The corresponding NN call latencies are 9\.61, 8\.10, and 8\.43 seconds\. These measurements cover both solved instances and runs that reach the 5,000\-second time limit\.

#### Analysis of Commonly Solved Instances\.

We define the commonly solved set as the instances for which both native andSAT\-ACT\-guided CaDiCaL return SAT or UNSAT\. The two solvers produce identical SAT/UNSAT results on every instance in this set\. Across the three benchmark sets, 752 instances are solved by both solvers, 16 are solved only by native CaDiCaL, 21 are solved only by the guided solver, and 411 remain unsolved by both\. On SC\-2023, both solvers solve 251 instances, but each uniquely solves four instances\. The guided solver obtains net gains of two solved instances on SC\-2024 and three on SC\-2025, resulting in five additional solved instances overall\.

Among the 752 commonly solved instances, the guided solver is faster on 448 instances, corresponding to 59\.57%, while native CaDiCaL is faster on 304 instances\. The guided solver reduces the total runtime by 61,101\.75 seconds, or 10\.15%, corresponding to an aggregate speedup of1\.113×1\.113\\times\. We define the instance\-level runtime ratio asRi=Tnative,i/Tguided,iR\_\{i\}=T\_\{\\mathrm\{native\},i\}/T\_\{\\mathrm\{guided\},i\}, whereRi\>1R\_\{i\}\>1favorsSAT\-ACT\. The median ratios are1\.051×1\.051\\times,1\.128×1\.128\\times, and1\.055×1\.055\\timeson SC\-2023, SC\-2024, and SC\-2025, respectively\. The corresponding aggregate speedups are1\.080×1\.080\\times,1\.073×1\.073\\times, and1\.193×1\.193\\times\. SC\-2024 shows the largest median improvement, whereas SC\-2025 shows the largest aggregate speedup\. This difference suggests that the SC\-2025 gains are concentrated more heavily on instances with longer solving times\.

We also recompute the neural\-call overhead on the commonly solved instances\. The NN wait ratios are 19\.26%, 8\.76%, and 12\.62% on SC\-2023, SC\-2024, and SC\-2025, while the corresponding NN call latencies are 12\.33, 7\.61, and 9\.09 seconds\. Across all 752 instances, the NN wait ratio is 13\.48% and the NN call latency is 9\.67 seconds\. These wait ratios are higher than the full\-set values because the full\-set averages contain many runs that reach the 5,000\-second time limit\. A small number of neural calls accounts for only a small fraction of the total runtime on these timed\-out runs\. The commonly solved set therefore provides a more direct view of neural overhead during successful solving\.

Together, these results show that neural guidance maintains outcome consistency, modestly expands solving coverage, and reduces end\-to\-end runtime on commonly solved instances after accounting for neural\-call overhead, although the gains are not uniform across all instances\.