Boolean Satisfiability via Imitation Learning

## Abstract

Abstract We propose ImitSAT, a branching policy for conflict-driven clause learning (CDCL) solvers based on imitation learning for the Boolean satisfiability problem (SAT). Unlike previous methods that predict instance-level signals to improve CDCL branching indirectly, or rely on reinforcement learning and insufficient CDCL information to enhance branching, ImitSAT learns from expert KeyTrace that collapses a full run into the sequence of surviving decisions. Replaying a KeyTrace on the same instance is nearly conflict-free, providing dense decision-level supervision and directly reducing propagations—the dominant contributor to wall-clock time. This prefix-conditioned supervision enables ImitSAT to reproduce high-quality branches without exploration, yielding faster convergence, stable training, and seamless integration into CDCL. Extensive experiments demonstrate that ImitSAT reduces propagation counts and runtime, outperforming state-of-the-art learned approaches. We released the source code and trained model at https://github.com/zewei-Zhang/ImitSAT .

## 1 Introduction

The Boolean satisfiability (SAT) problem is a cornerstone of theoretical computer science and artificial intelligence (Cook, 1971; Karp, 1972). Beyond its foundational role, SAT serves as the computational backbone of numerous applications, including formal verification, planning, and combinatorial optimization. Modern solvers for SAT are dominated by the conflict-driven clause learning (CDCL) framework (Silva & Sakallah, 1996; Biere et al., 2009), which has scaled to industrial benchmarks of immense complexity. A CDCL run interleaves branching, unit propagation, and conflict analysis. Among these components, the branching rule largely determines the search trajectory, while unit propagation often dominates runtime (Zhang & Malik, 2002; Davis et al., 2008; Moskewicz et al., 2001). As a result, more informed branching decisions can translate directly into faster solving.

Classical branching heuristics, however, are hand-crafted and limited in their adaptability. Recent work has sought to improve solver performance by integrating learning-based guidance. For example, SATformer (Shi et al., 2023) learns instance-level signals to adjust variable activities during initialization, but it exerts no influence once the branching loop begins. Graph-Q-SAT (Kurin et al., 2020) introduces an online agent within CDCL, yet it relies on reinforcement learning (RL), which requires extensive exploration and can be unstable due to sparse rewards and delayed feedback. Moreover, Graph-Q-SAT does not utilize the full CDCL execution history; each branching is conditioned only on a compact graph snapshot of the current state, so the history influences the agent only indirectly.

In contrast, we adopt imitation learning, which trains directly from expert traces. Specifically, we introduce ImitSAT, a CDCL branching learner trained on expert trace replays. Replaying an expert trace on the same instance is nearly conflict-free, eliminating redundant propagations and providing clean training targets.
Since branching is inherently prefix-conditioned, we formulate it as an autoregressive sequence modeling problem, and implement ImitSAT with a Transformer-based learner (Vaswani et al., 2017). Our model captures long-context dependencies while keeping runtime costs practical through lightweight autoregressive attention (Hawthorne et al., 2022).

To obtain expert traces, we collapse full solver runs into sequences of surviving decisions, yielding dense, step-level supervision at every branching point. This approach enables the learner to reproduce high-quality decisions without costly exploration, resulting in faster convergence, more stable training, and natural alignment with the prefix-conditioned structure of branching. During inference, ImitSAT reads the instance together with a KeyTrace prefix and autoregressively predicts the next signed variable as the branch decision. The policy is queried under a small budget, reverting to the native heuristic when uncertain, while all other CDCL components remain unchanged, preserving completeness and robustness.

We evaluate ImitSAT on held-out random 3-SAT instances ranging from 5 to 100 variables, as well as on structured families including satisfiable and unsatisfiable instances and non-$k$-SAT formulas.
Under limited query budgets, ImitSAT consistently reduces propagations relative to a standard CDCL solver and outperforms prior learning-based methods, SATformer and Graph-Q-SAT, across most settings while matching their performance elsewhere.
Wall-clock measurements show that ImitSAT achieves favorable runtime performance against SOTA methods (Shi et al., 2023; Kurin et al., 2020).
Remarkably, although trained solely on simple random 3-SAT, ImitSAT transfers effectively to unsatisfiable and non-$k$-SAT benchmarks without modification.

We summarize the contributions of this work as below.

- •
We propose ImitSAT, the first branching policy for CDCL solvers based on imitation learning.
Unlike prior methods that rely on reinforcement learning, ImitSAT leverages dense, decision-level supervision from expert traces.
- •
We cast branching as a sequential modeling problem by collapsing solver runs into compact sequences of surviving decisions. These sequences serve as clean, conflict-free training targets and align naturally with prefix-conditioned autoregressive modeling.
- •
Extensive experiments demonstrate that ImitSAT yields both practical efficiency and strong generalization.

## 2 Related Works

#### Neural guidance for SAT and CDCL.

Early learning approaches focused on instance-level prediction, using Graph Neural Network (GNNs) (Scarselli et al., 2008) to classify SAT or UNSAT, as seen in NeuroSAT (Selsam et al., 2019; Selsam & Bjørner, 2019) and  (Cameron et al., 2020). Recent work has explored whether Transformers can learn solver behavior directly (Pan et al., 2025).
In parallel with these model-based approaches, complementary efforts target data and benchmarking, including G2SAT (You et al., 2019) and G4SATBench (Li et al., 2024).
Building on these foundations, a second line integrates learning inside solvers to shape specific components: for example, NeuroSelect (Liu et al., 2024) learns clause deletion policies, NeuroBack (Wang et al., 2024) improves phase initialization with GNNs, and RDC‑SAT (Zhai & Ge, 2025) adopts a divide-and-conquer strategy via reinforcement learning. This approach leads to targeted enhancements within solver mechanisms.
More concretely, within the CDCL branching loop, several methods exemplify this integration: NeuroSAT (Selsam & Bjørner, 2019) has been used to guide variable selection; Graph-Q-SAT (Kurin et al., 2020) trains an RL agent queried online during search based on instance information; and SATformer (Shi et al., 2023) trains a GNN Transformer model to initialize the CDCL that indirectly influences branching thereafter.

#### Imitation learning for control.

Imitation learning (IL) learns policies directly from expert demonstrations, that is, sequences of states with associated actions (Osa et al., 2018; Zare et al., 2024). A simple example is behavior cloning (BC), which utilizes supervised learning to map observed situations to expert choices (Pomerleau, 1991).
Building on the principles of imitation learning, the Decision Transformer (Chen et al., 2021) is similar to behavior cloning, framing reinforcement learning as sequence modeling, where an autoregressive Transformer is trained to predict the next action given a sequence rollout of returns, states, and actions. This view connects control to next-token prediction and attains competitive performance without explicit value function learning.
The application of imitation learning extends beyond traditional domains. For instance, beyond robotics and games, IL has guided decision-making in exact optimization solvers. In mixed-integer linear programming, policies learned to imitate strong branching can be used within branch-and-bound and achieve strong results (Gasse et al., 2019). Related work also learns branching policies that integrate into branch-and-bound (Zarpellon et al., 2021).

Motivated by the limitations of neural guidance for SAT detailed above, and drawing inspiration from imitation learning, we propose ImitSAT. The branching policy for CDCL clones a near conflict-free KeyTrace distilled from solver runs. To achieve this, we cast branching as prefix-conditioned sequence prediction and train an autoregressive next-decision model on compact sequences of surviving decisions. This provides dense, decision-level supervision at low per-query cost. These design choices help reduce propagation and improve wall-clock time under small query budgets.

## 3 Preliminaries on SAT

#### Boolean Satisfiability Problem.

Figure: Figure 1: From a CDCL run to a KeyTrace. The left pane sketches one run in three stages: (1) decide $x_{4}=\top$, then $x_{3}=\top$, hit a conflict, backtrack to the decision on $x_{3}$; (2) set $x_{3}=\bot$, conflict again, backtrack to $x_{4}$; (3) set $x_{4}=\bot$, then decide $x_{1}=\top$ and $x_{2}=\top$ and solve. Unit assignments are omitted for clarity. Collapsing backtracks removes detours and keeps only the surviving root–to–current decisions, yielding the compact *KeyTrace* on the right, which serves as the expert for imitation. A step‑by‑step walkthrough is in Appendix [H](https://arxiv.org/html/2509.25411v1#A8).
Refer to caption: x1.png

The *Boolean satisfiability problem* (SAT) is the canonical decision problem in propositional logic.
It asks whether a Boolean formula $F$ over variables $x_{1},\dots,x_{n}$ can be made true by assigning each variable a value in $\{\top,\bot\}$, where $\top$ denotes *true* and $\bot$ denotes *false*.
A *literal* is either a variable $x_{i}$ or its negation $\lnot x_{i}$.
A *clause* is a disjunction of literals,

$$ $C_{i}\;=\;(\ell_{i,1}\lor\cdots\lor\ell_{i,k_{i}})\,,$ (1) $$

and a formula is in *conjunctive normal form* (CNF) (Plaisted & Greenbaum, 1986) if it is a conjunction of clauses:

$$ $F\;=\;C_{1}\land C_{2}\land\cdots\land C_{m}\,.$ (2) $$

An *assignment* is a mapping $\sigma:\{x_{1},\dots,x_{n}\}\to\{\top,\bot\}$. It satisfies a clause if at least one literal in the clause evaluates to $\top$ under $\sigma$, and it satisfies the entire formula $F$ if every clause is satisfied. We say that $F$ is *satisfiable* (SAT) if such an assignment exists, and *unsatisfiable* (UNSAT) otherwise.

A special case is the *$k$-SAT problem*, where each clause contains exactly $k$ literals. The case $k=3$ (3-SAT) is of particular importance: it is NP-complete (Karp, 1972) and widely used in theoretical analysis and empirical benchmarks.
For example, consider the CNF formula

$$ $F=(x_{1}\lor\lnot x_{3}\lor x_{4})\land(\lnot x_{1}\lor x_{2}\lor x_{3})\land(\lnot x_{2}\lor\lnot x_{3}\lor\lnot x_{4})\,.$ (3) $$

This formula is SAT, since the assignment $x_{1}=\top$, $x_{2}=\top$, $x_{3}=\bot$, $x_{4}=\bot$ makes every clause true.
If no assignment satisfies all clauses, the instance would be UNSAT.

In practice, SAT formulas are often represented in the standard *DIMACS CNF format* (Johnson & Trick, 1996).
In this encoding, each clause is written as a sequence of nonzero integers terminated by 0, where the integer $i$ denotes variable $x_{i}$ and $-i$ denotes its negation $\lnot x_{i}$.
For the formula in Equation [3](https://arxiv.org/html/2509.25411v1#S3.E3), the DIMACS form is:

$$ $F_{\mathrm{DIMACS}}=\texttt{1\ -3\ 4\ 0}\quad\texttt{-1\ 2\ 3\ 0}\quad\texttt{-2\ -3\ -4\ 0}\,.$ (4) $$

This compact numeric encoding is convenient for algorithmic solvers and sequence-based models.

#### Conflict-driven Clause Learning.

Conflict-driven clause learning (CDCL) is the dominant algorithmic framework for practical SAT solvers (Silva & Sakallah, 1996; Biere et al., 2009).
A CDCL solver incrementally explores a branching search tree through three fundamental operations:
*decision* ($\mathtt{D}$), where the solver assigns a value to a chosen literal and thus extends the current partial assignment;
*unit propagation* ($\mathtt{A}$), also known as *Boolean Constraint Propagation* (BCP) (Moskewicz et al., 2001), where implied literals are deduced from unit clauses;
and *backtracking* ($\mathtt{BT}$), where a detected conflict triggers clause learning and a non-chronological jump to an earlier decision level.

At each decision level, the solver selects a decision literal, after which propagation infers additional assignments, possibly none.
If a clause is falsified, conflict analysis derives a a new *learned clause*, identifies its *asserting literal*, and adds the clause to the solver’s database.
The solver then backjumps to the highest decision level where the learned clause becomes unit and enqueues the asserting literal.
A conflict at decision level 0 establishes that the formula is UNSAT, while a complete assignment with no conflicts proves SAT.

#### Branching Heuristic and Implementation.

Branching is the central operation in CDCL: at each step of the search, the solver selects a variable and its polarity to branch on.
The quality of these choices is critical. Strong decisions can greatly reduce the number of propagations and conflicts, whereas weak ones may cause the search to grow exponentially.

Usually, the choice of the next decision variable, together with its phase, is determined by a *branching heuristic*.
The most influential family of heuristics is the *Variable State Independent Decaying Sum* (VSIDS) (Moskewicz et al., 2001).
In VSIDS, variables are assigned activity scores that are increased whenever they appear in learned clauses. These scores are then periodically decayed, ensuring that recently relevant variables are favored for branching.
This dynamic prioritization enables the solver to focus on the most promising parts of the search space. A notable implementation is MiniSAT (Eén & Sörensson, 2003), a lightweight and extensible open-source CDCL solver. Despite its minimalistic codebase, MiniSAT has become a standard platform for both research and industrial applications due to its clarity and effectiveness.

## 4 ImitSAT

Figure: Figure 2: Propagation dominates CDCL time. MiniSAT spends about 88.9% in propagation, 9.2% in conflict analysis, and 1.9% in branching. Reducing propagation is therefore the main route to wall‑clock gains.
Refer to caption: x2.png

As reviewed in Section [3](https://arxiv.org/html/2509.25411v1#S3), branching plays a pivotal role in CDCL: the quality of branching decisions largely determines the efficiency of unit propagation, which is the dominant cost in practice.
Traditional heuristics such as VSIDS are highly effective but ultimately hand-crafted, leaving open the possibility of more principled approaches that can exploit structural patterns in solver traces.
In this paper, we introduce ImitSAT, a framework that leverages expert-guided sequence modeling to learn high-quality branching policies for CDCL solvers.

Our approach consists of two main components:
(i) *KeyTrace construction*, which compresses solver runs by collapsing backtracks into a concise sequence of expert decisions (Section [4.1](https://arxiv.org/html/2509.25411v1#S4.SS1)); and
(ii) an *autoregressive learner*, which imitates the KeyTrace to predict the next branching decision in sequence (Section [4.2](https://arxiv.org/html/2509.25411v1#S4.SS2)).
These components are seamlessly integrated into the CDCL framework. Together, they provide clean supervision signals and enable plug-and-play deployment.

### 4.1 Expert KeyTrace Replay

We seek an expert that guides the solver toward effective branching decisions while avoiding wasted detours.
Raw CDCL trails are often long and contain many decisions that are later undone by backtracking.
An ideal expert should preserve only the decisions that survive and discard detours, thereby yielding clean training targets and eliminating steps that do not advance the search.
In CDCL, unit propagation dominates runtime, typically accounting for 80%–90% of the total solving time (Zhang & Malik, 2002; Davis et al., 2008; Moskewicz et al., 2001), a trend we also confirm in Figure [2](https://arxiv.org/html/2509.25411v1#S4.F2).
This observation suggests that an expert which avoids wasted branches can substantially reduce propagation and thereby improve overall efficiency.

In order to extract expert supervision for branching, we first examine the execution trace of a CDCL solver.
Each run on an instance $F$ produces a *trail*, namely a chronological sequence of decision, propagation, and backtracking events annotated with decision levels:

$$ $\mathcal{T}_{t}=\left((\tau_{1},\lambda_{1},h_{1}),\ldots,(\tau_{t},\lambda_{t},h_{t})\right)\,,$ (5) $$

where $\tau_{i}\in\{\mathtt{D},\mathtt{A},\mathtt{BT}\}$ representing a decision, a unit propagation assignment, or a backtrack event, respectively.
$\lambda_{i}$ is a signed variable with $\lambda_{i}\in\{\pm 1,\ldots,\pm n\}$. We interpret $\lambda_{i}=+j$ as $x_{j}=\top$ and $\lambda_{i}=-j$ as $x_{j}=\bot$.
The value $h_{i}$ is the decision level after the event. Raw trails $\mathcal{T}_{t}$ are often long and contain numerous events that are eventually undone by backtracking. Such redundant segments do not contribute to solving progress, yet they inflate computational cost and inject noise into the context, making it harder to isolate the key decisions that drive the search.

To remove these detours, we construct an expert *KeyTrace* through a systematic extraction procedure.
Specifically, we scan $\mathcal{T}_{t}$ from left to right while maintaining a working sequence $\mathcal{K}$ that starts empty:

$$ $\mathcal{K}\;\leftarrow\;\emptyset.$ (6) $$

For each event $(\tau_{i},\lambda_{i},h_{i})$ we update

$$ $\mathcal{K}\ \leftarrow\ \begin{cases}\mathcal{K}\ \|\ (\mathtt{D},\lambda_{i},h_{i}),&\text{if }\tau_{i}=\mathtt{D},\\ \mathcal{K}\ \|\ (\mathtt{A},\lambda_{i},h_{i}),&\text{if }\tau_{i}=\mathtt{A},\\ \operatorname{trim}_{\leq h_{i}}(\mathcal{K})\ \|\ (\mathtt{D},\lambda_{i},h_{i}),&\text{if }\tau_{i}=\mathtt{BT},\end{cases}$ (7) $$

where $\|$ denotes concatenation.
The operator $\operatorname{trim}_{\leq h}$ removes all suffix events whose level is above $h$.
Restarts are handled by trimming to level 0, i.e., $\mathcal{K}\leftarrow\operatorname{trim}_{\leq 0}(\mathcal{K})$.
After the scan, the resulting sequence

$$ $\mathcal{K}_{t}=\mathcal{K}\,$ (8) $$

is taken as the expert KeyTrace for trail $\mathcal{T}_{t}$.

It is worth noting that the above procedure preserves only the decision and propagation events that survive backtracking, effectively collapsing backtracks into prefix truncations while treating restarts as full resets. This results in a considerably shorter and more stable trail representation, capturing the minimal necessary context for advancing the search.

Empirical evidence demonstrates that replaying the decision sequence encoded in $\mathcal{K}_{t}$ on the same problem instance renders the solver’s run nearly conflict-free, drastically reducing the number of propagation events to approximately 4% of those recorded in the raw MiniSAT trail ( see Figure [3](https://arxiv.org/html/2509.25411v1#S4.F3)). Since propagation constitutes the dominant runtime component of CDCL solvers, this reduction translates directly into significant improvements in solver efficiency.

Figure: Figure 3: Compact KeyTrace replay. The expert replayed only a small share of MiniSAT events: 0.2% conflicts, 19.6% decisions, and 4.3% propagations.
Refer to caption: x3.png

### 4.2 Autoregressive Imitation for CDCL Branching

Given this compact expert KeyTrace, our goal is to train a learner that can imitate expert-quality branching decisions.
In this setting, the expert demonstrations are provided by KeyTraces: each surviving decision, together with its implied propagations, forms a supervised training target.
Unlike reinforcement-style exploration, this approach offers dense, step-level supervision and eliminates detours, allowing the learner to acquire high-quality decision policies with faster convergence and greater stability.

Formally, since a CDCL solver queries one branch at a time, the learning task is to map the formula $F$ together with a KeyTrace prefix $\mathcal{K}_{t}$ to the next signed variable, while operating under a small computational budget.
This task is inherently sequential, as each decision depends on the prefix of earlier assignments.
An autoregressive (AR) model is therefore a natural choice, as it conditions on the serialized prefix and predicts the next element in the sequence.
To realize this, we first serialize the solver state into a compact sequence tailored for autoregression, then specify the AR next-decision learner and its behavior-cloning objective, and finally describe how the learner is integrated into CDCL at inference time.

#### Serialization.

To make the AR learner effective, both the CNF $F$ and the KeyTrace prefix $\mathcal{K}_{t}$ are serialized into one deterministic sequence. The CNF is written in DIMACS integer format $F_{\mathrm{DIMACS}}$, followed by separator tokens [SEP]. The KeyTrace is then presented as blocks, where each decision literal is followed by the unit assignments produced by propagation. Level fields and assignment tags are omitted for compactness. The sequence ends with a decision probe marker [D] that signals a request for the next branch. Formally, with $\mathcal{K}_{t}=\big((\tau_{1},\lambda_{1},h_{1}),\ldots,(\tau_{t},\lambda_{t},h_{t})\big)$,

$$ $\operatorname{enc}(\mathcal{K}_{t})=\big\|_{i=1}^{J}\,(\texttt{D},\,d_{i},\,a_{i,1},\ldots,a_{i,k_{i}}),\qquad d_{i},\,a_{i,k}\in\{\pm 1,\ldots,\pm n\},$ (9) $$

and the full serialized input is

$$ $z(F,\mathcal{K}_{t})=\texttt{[CNF]}\ \|\ F_{\mathrm{DIMACS}}\ \|\ \texttt{[SEP]}\ \|\ \operatorname{enc}(\mathcal{K}_{t})\ \|\ \texttt{[D]}.$ (10) $$

This compact representation aligns exactly with next-decision prediction for an AR learner.

#### Next‑decision AR learner.

The learner implements the policy

$$ $p_{\theta}\!\left(\lambda_{\mathrm{next}}\mid F,\mathcal{K}_{t}\right),\qquad\lambda_{\mathrm{next}}\in\{\pm 1,\ldots,\pm n\},$ (11) $$

using an AR model defined over $z(F,\mathcal{K}_{t})$.
For a generic sequence $x_{1},\ldots,x_{S}$, the AR factorization is

$$ $p_{\theta}(x_{1},\ldots,x_{S})\;=\;\prod_{s=1}^{S}p_{\theta}\!\left(x_{s}\mid x_{<s}\right),$ (12) $$

where $s$ is the index immediately following the decision probe marker [D].
Under this serialization, predicting the next CDCL decision is exactly next‑symbol prediction at position $s$:

$$ $p_{\theta}\!\left(\lambda_{\mathrm{next}}\mid F,\mathcal{K}_{t}\right)\;=\;p_{\theta}\!\left(x_{s}=\lambda_{\mathrm{next}}\mid x_{<s}=z(F,\mathcal{K}_{t})\right).$ (13) $$

Training follows the standard *behavior cloning* paradigm in imitation learning.
Let $\mathsf{Q}$ be the set of triples $(F,\mathcal{K}_{t},d_{t+1})$.
Training minimizes the average negative log‑likelihood of the expert decisions:

$$ $\mathcal{L}(\theta)\;=\;\frac{1}{|\mathsf{Q}|}\sum_{(F,\mathcal{K}_{t},d_{t+1})\in\mathsf{Q}}\Bigl[-\log p_{\theta}\!\left(d_{t+1}\mid z(F,\mathcal{K}_{t})\right)\Bigr],$ (14) $$

which is equivalent to cross‑entropy at the decision probe positions. In other words, the learner directly imitates the expert policy encoded in the KeyTraces.

#### Online integration into CDCL.

At each decision point, the learner is queried under a small budget. The current trail is collapsed into the KeyTrace, the instance and prefix are serialized, and the model predicts one signed variable. If the prediction is legal (i.e., within the variable range and currently unassigned), the solver accepts it and decrements the query budget. Otherwise, the solver immediately falls back to VSIDS heuristic. This design preserves completeness and keeps overhead small. A front‑loaded query schedule is particularly effective, as early decisions strongly shape most of the search as shown in Appendix [E](https://arxiv.org/html/2509.25411v1#A5).
A complete Algorithm [1](https://arxiv.org/html/2509.25411v1#alg1) description is provided in Appendix [A](https://arxiv.org/html/2509.25411v1#A1).

## 5 Experiments

### 5.1 Implementation Details

#### Baselines.

We compare against SATformer (Shi et al., 2023) and Graph‑Q‑SAT (Kurin et al., 2020), which are trained with their public implementations and the training data specified in their papers.

#### CDCL Solver.

A Python reimplementation of MiniSAT 2.2 (Eén & Sörensson, 2003) is used and validated against the official C++ version on full trails $\mathcal{T}_{t}$.
This version streamlines the integration of learning methods, ensuring that all approaches are evaluated in a consistent environment.

#### Datasets.

We generate the random 3–SAT training dataset with a planted assignment (Mezard & Montanari, 2009; Achlioptas et al., 2000; 2005).
The clause–variable ratio is in $[4.1,4.4]$.
Variable ranges include 5 to 15, 16 to 30, 31 to 60, and 61 to 100, with additional fixed sizes of 50 and 100.
For each formula, a MiniSAT run yields the level-annotated trail as Equation [5](https://arxiv.org/html/2509.25411v1#S4.E5). Then, the expert KeyTrace is extracted using Equation [7](https://arxiv.org/html/2509.25411v1#S4.E7).
Every decision position provides one supervision pair, a KeyTrace prefix $\mathcal{K}_{t}$, and its next decision $d_{t+1}$.
For evaluation, we first use the test set, which is drawn from the same generators and variable ranges as those used for training.
Generalization is then assessed on different SAT families from SATLIB (Hoos & Stützle, 2000).
Further dataset details appear in Appendix [B](https://arxiv.org/html/2509.25411v1#A2).

#### AR learner and training.

Perceiver AR (Hawthorne et al., 2022) serves as our architecture for predicting the next decision.
Specifically, the model uses an output latent array that cross-attends to the input. Since only one output is needed for the next branching, we set the latent length to 1.
This results in each query having $O(N)$ complexity in terms of input length, avoiding the $O(N^{2})$ cost associated with a standard Transformer decoder.
Furthermore, our model configuration follows the recommendations in (Hawthorne et al., 2022).
We use 16 attention heads for cross‑attention and self‑attention, 12 Transformer blocks, an MLP expansion of $4\times$, squared‑ReLU activations, and cross‑attention dropout $0.1$.

#### Metrics.

Propagation dominates CDCL time (Zhang & Malik, 2002; Davis et al., 2008; Moskewicz et al., 2001), as seen in Figure [2](https://arxiv.org/html/2509.25411v1#S4.F2) and Table [6](https://arxiv.org/html/2509.25411v1#A3.T6).
We therefore use the number of propagation as the primary signal.
Since instances vary in size and difficulty, we normalize by MiniSAT on a per‑instance basis and aggregate with the median to reduce the influence of outliers.

Let $p_{i}$ be the propagation count of the evaluated method on instance $F_{i}$, and let $p^{\prime}_{i}$ be the corresponding count for MiniSAT.
We report the *Median Relative Propagation Percentage* (MRPP)

$$ $\tilde{r}=\mathrm{med}_{i=1,...,N}\left(\dfrac{p_{i}}{p_{i}^{\prime}}\right)\,,$ (15) $$

values $\tilde{r}<1$ indicate fewer propagation than MiniSAT and hence an improvement.

To capture instance‑wise gains, we also report a one‑percent win rate.
With margin $\delta=0.01$

$$ $W_{\delta}=\frac{1}{N}\sum_{i:\,p_{i}^{\prime}>0}\mathbf{1}\left[p_{i}\leq(1-\delta)\,p_{i}^{\prime}\right]\,.$ (16) $$

This is the fraction of problems on which the method reduces the propagation number by at least 1% relative to MiniSAT; therefore, a larger $W_{1\%}$ is better.

### 5.2 Comparison on test sets

We compare ImitSAT with Graph-Q-SAT and SATformer on held-out random 3-SAT. To align wall-clock budgets, ImitSAT is queried at 3 or 5 times per instance. Graph-Q-SAT uses the same computational budgets. SATformer updates the VSIDS variable scores once at initialization. We report MRPP $\tilde{r}$ and the one percent win rate $W_{1\%}$.

Table [1](https://arxiv.org/html/2509.25411v1#S5.T1) (top) shows that ImitSAT achieves the lowest MRPP $\tilde{r}$ in nearly all ranges. With 3 or 5 calls, it is best on 5–15, 16–30, 31–60, 50, 100, and ties SATformer on 61–100. These results indicate that imitation of the expert, as demonstrated by KeyTrace, consistently reduces propagation under small query budgets.
Building on these MRPP results, Graph-Q-SAT increases propagation number on the 61-100 dataset, indicating weaker guidance under the same budget.
Finally, in Table [1](https://arxiv.org/html/2509.25411v1#S5.T1) (bottom), we report $W_{1\%}$ to show instance‑wise gains. ImitSAT with 3 calls achieves the highest win rate in all ranges.

**Table 1: MRPP $\tilde{r}$ ($\downarrow$) and one percent win ratio $W_{1\%}$ ($\uparrow$) on 3-SAT test sets. GQSAT denotes Graph-Q-SAT.**
| Metric | Method | 5–15 | 16–30 | 31–60 | 61–100 | 50 | 100 |
| --- | --- | --- | --- | --- | --- | --- | --- |
| MRPP $\tilde{r}$ ($\downarrow$) | GQSAT-3calls | 1.00 | 0.94 | 0.89 | 1.15 | 0.71 | 0.85 |
| GQSAT-5calls | 1.00 | 0.90 | 0.82 | 0.94 | 0.70 | 0.80 |  |
| SATformer | 1.00 | 0.89 | 0.84 | 0.78 | 0.88 | 0.81 |  |
| Ours-3calls | 0.75 | 0.83 | 0.75 | 0.78 | 0.74 | 0.76 |  |
| Ours-5calls | 0.73 | 0.77 | 0.75 | 0.80 | 0.66 | 0.83 |  |
| $W_{1\%}$ ($\uparrow$) | GQSAT-3calls | 0.45 | 0.53 | 0.54 | 0.48 | 0.57 | 0.55 |
| GQSAT-5calls | 0.46 | 0.54 | 0.56 | 0.53 | 0.59 | 0.58 |  |
| SATformer | 0.48 | 0.55 | 0.58 | 0.57 | 0.60 | 0.57 |  |
| Ours-3calls | 0.68 | 0.65 | 0.65 | 0.64 | 0.69 | 0.60 |  |
| Ours-5calls | 0.67 | 0.64 | 0.61 | 0.59 | 0.64 | 0.56 |  |

### 5.3 Generalization on special SAT families

In this section, we assess the ability to transfer to structured families that differ from the training generator, covering SAT and UNSAT, 3-SAT, and non-$k$-SAT, without any retraining or tuning. Query budgets match the test sets, with 3 or 5 calls per instance for ImitSAT and Graph-Q-SAT, whereas SATformer adjusts the VSIDS variable scores only once at initialization.

Across all families, ImitSAT attains the lowest MRPP $\tilde{r}$ or ties for best as shown in Table [2](https://arxiv.org/html/2509.25411v1#S5.T2) (top).
The gains are large on PARITY and PRET, and with 5 calls ImitSAT is best on JNH and AIM, and matches the best on PHOLE. Graph-Q-SAT does not reduce propagation number on JNH and AIM, and in fact increases the propagation number. SATformer only shows a gain on the PARITY dataset; all other datasets exhibit no gain or worse performance than MiniSAT.
Table [2](https://arxiv.org/html/2509.25411v1#S5.T2) (bottom) reports the $W_{1\%}$. ImitSAT achieves the highest or tied win rate on all families, including a perfect score on PRET and matching the best on PARITY and PHOLE. These outcomes indicate that imitation of the expert KeyTrace transfers from random 3-SAT to structured regimes without finetuning.

**Table 2: MRPP $\tilde{r}$ ($\downarrow$) and one percent win ratio $W_{1\%}$ ($\uparrow$) on structured SAT families.**
| Metric | Method | JNH | AIM | PARITY | PHOLE | PRET |
| --- | --- | --- | --- | --- | --- | --- |
| MRPP $\tilde{r}$ ($\downarrow$) | GQSAT-3calls | 1.29 | 1.20 | 0.82 | 1.03 | 0.88 |
| GQSAT-5calls | 1.11 | 1.18 | 0.56 | 0.82 | 0.92 |  |
| SATformer | 1.36 | 1.01 | 0.73 | 1.00 | 1.00 |  |
| Ours-3calls | 1.00 | 0.88 | 0.30 | 1.00 | 0.42 |  |
| Ours-5calls | 0.85 | 0.81 | 0.30 | 0.82 | 0.42 |  |
| $W_{1\%}$ ($\uparrow$) | GQSAT-3calls | 0.38 | 0.31 | 0.80 | 0.50 | 0.50 |
| GQSAT-5calls | 0.44 | 0.38 | 0.80 | 0.75 | 0.50 |  |
| SATformer | 0.25 | 0.44 | 0.60 | 0.00 | 0.00 |  |
| Ours-3calls | 0.44 | 0.63 | 0.80 | 0.50 | 1.00 |  |
| Ours-5calls | 0.50 | 0.63 | 0.80 | 0.75 | 1.00 |  |

### 5.4 Wall-clock Time

To measure practical impact, end‑to‑end solve time is recorded for each instance. The timer starts when the CDCL solve loop begins and stops when the instance is solved; CNF parsing and simplification are excluded from the timing. All model inference costs are included. ImitSAT and Graph‑Q‑SAT receive 3 calls per instance to match compute budgets. SATformer adjusts VSIDS variable scores once at initialization.

Across random 3‑SAT test sets and structured families, ImitSAT traces the lowest curves under these budgets, which means more instances are solved in less time, as shown in Figure [4](https://arxiv.org/html/2509.25411v1#S5.F4).
Learning model-based branching introduces query overhead, so wall‑clock gains appear only once propagation savings exceed this cost.

Figure: Figure 4: Wall‑clock time versus instances solved on random test sets and structured families. Curves show end‑to‑end solver time per instance with all model calls included and preprocessing excluded. ImitSAT and Graph‑Q‑SAT use 3 calls per instance. SATformer performs a single VSIDS initialization. The lower curve is better.
Refer to caption: x4.png

### 5.5 Improved Training Techniques

We observe that ImitaSAT is prone to overfitting. To address this issue, we introduce improved training techniques.
First, we apply variable permutation augmentation, where variable IDs are randomly permuted when forming training examples.
As shown in Figure [5](https://arxiv.org/html/2509.25411v1#A6.F5), both training and validation losses decay steadily with augmentation, whereas without augmentation the validation loss peaks early and then rises despite continued decrease in training loss.
Second, we employ a staged curriculum learning strategy that gradually expands the variable range from small to large (Nagatsuka et al., 2021; Pouransari et al., 2024). This accelerates convergence on simple instances while ensuring comprehensive coverage of larger problem sizes.
More details for variable permutation augmentation and curriculum learning are provided in Appendix [F](https://arxiv.org/html/2509.25411v1#A6) and [G](https://arxiv.org/html/2509.25411v1#A7).

## 6 Conclusion

We presented ImitSAT, a CDCL branching policy based on imitation learning. By collapsing solver runs into compact sequences of surviving decisions, we obtain expert traces that capture high-quality branching behavior. These traces allow us to formulate branching as an autoregressive prediction problem, yielding dense, conflict-free supervision that enables stable and efficient training. Extensive experiments show that ImitSAT reduces propogations, achieves favorable runtime, and generalizes well beyond 3-SAT, outperforming prior learning-based methods. Future work could extend this approach to richer expert demonstrations, hybrid imitation–reinforcement learning schemes, or broader domains of combinatorial reasoning.

## References

- Achlioptas et al. (2000)
Dimitris Achlioptas, Carla Gomes, Henry Kautz, and Bart Selman.
Generating satisfiable problem instances.
In *Proceedings of the AAAI/IAAI Conference*, pp. 256–261, 2000.
- Achlioptas et al. (2005)
Dimitris Achlioptas, Haixia Jia, and Cristopher Moore.
Hiding satisfying assignments: two are better than one.
*Journal of Artificial Intelligence Research*, 24:623–639, 2005.
- Asahiro et al. (1996)
Yuihci Asahiro, Kazuo Iwama, and Eiji Miyano.
Random generation of test instances with controlled attributes.
*DIMACS Series in Discrete Mathematics and Theoretical Computer Science*, pp. 377–393, 1996.
- Biere et al. (2009)
Armin Biere, Marijn Heule, and Hans van Maaren.
*Handbook of satisfiability*, volume 185.
IOS press, 2009.
- Cameron et al. (2020)
Chris Cameron, Rex Chen, Jason Hartford, and Kevin Leyton-Brown.
Predicting propositional satisfiability via end-to-end learning.
In *Proceedings of the AAAI Conference on Artificial Intelligence*, volume 34, pp. 3324–3331, 2020.
- Chen et al. (2021)
Lili Chen, Kevin Lu, Aravind Rajeswaran, Kimin Lee, Aditya Grover, Misha Laskin, Pieter Abbeel, Aravind Srinivas, and Igor Mordatch.
Decision transformer: Reinforcement learning via sequence modeling.
In *Advances in Neural Information Processing Systems*, volume 34, pp. 15084–15097, 2021.
- Cook (1971)
Stephen A Cook.
The complexity of theorem-proving procedures.
In *Proceedings of the third annual ACM symposium on Theory of computing*, pp. 151–158, 1971.
- Davis et al. (2008)
John D Davis, Zhangxi Tan, Fang Yu, and Lintao Zhang.
A practical reconfigurable hardware accelerator for boolean satisfiability solvers.
In *Proceedings of the 45th annual Design Automation Conference*, pp. 780–785, 2008.
- Eén & Sörensson (2003)
Niklas Eén and Niklas Sörensson.
An extensible sat-solver.
In *International conference on theory and applications of satisfiability testing*, pp. 502–518. Springer, 2003.
- Gasse et al. (2019)
Maxime Gasse, Didier Chételat, Nicola Ferroni, Laurent Charlin, and Andrea Lodi.
Exact combinatorial optimization with graph convolutional neural networks.
In *Advances in Neural Information Processing Systems*, volume 32, 2019.
- Haken (1985)
Armin Haken.
The intractability of resolution.
*Theoretical computer science*, 39:297–308, 1985.
- Hawthorne et al. (2022)
Curtis Hawthorne, Andrew Jaegle, Cătălina Cangea, Sebastian Borgeaud, Charlie Nash, Mateusz Malinowski, Sander Dieleman, Oriol Vinyals, Matthew Botvinick, Ian Simon, et al.
General-purpose, long-context autoregressive modeling with perceiver ar.
In *International Conference on Machine Learning*, pp. 8535–8558. PMLR, 2022.
- Hoos & Stützle (2000)
Holger H. Hoos and Thomas Stützle.
SATLIB: An online resource for research on SAT.
In I. P. Gent, H. van Maaren, and T. Walsh (eds.), *SAT 2000*, pp. 283–292. IOS Press, 2000.
SATLIB is available online at [http://www.satlib.org](http://www.satlib.org).
- Johnson & Trick (1996)
David S. Johnson and Michael A. Trick (eds.).
*Cliques, Coloring, and Satisfiability: The Second DIMACS Implementation Challenge*, volume 26 of *DIMACS Series in Discrete Mathematics and Theoretical Computer Science*.
American Mathematical Society, 1996.
- Karp (1972)
Richard M. Karp.
Reducibility among combinatorial problems.
In Raymond E. Miller, James W. Thatcher, and Jean D. Bohlinger (eds.), *Complexity of Computer Computations*, The IBM Research Symposia Series, pp. 85–103. Springer, Boston, MA, 1972.
doi: 10.1007/978-1-4684-2001-2˙9.
- Kurin et al. (2020)
Vitaly Kurin, Saad Godil, Shimon Whiteson, and Bryan Catanzaro.
Can q-learning with graph networks learn a generalizable branching heuristic for a sat solver?
In *Advances in Neural Information Processing Systems*, pp. 9608–9621, 2020.
- Li et al. (2024)
Zhaoyu Li, Jinpei Guo, and Xujie Si.
G4satbench: Benchmarking and advancing sat solving with graph neural networks.
*Transactions on Machine Learning Research*, 2024.
- Liu et al. (2024)
Hongduo Liu, Peng Xu, Yuan Pu, Lihao Yin, Hui-Ling Zhen, Mingxuan Yuan, Tsung-Yi Ho, and Bei Yu.
Neuroselect: Learning to select clauses in sat solvers.
In *Proceedings of the 61st ACM/IEEE Design Automation Conference*, pp. 1–6, 2024.
- Mezard & Montanari (2009)
Marc Mezard and Andrea Montanari.
*Information, physics, and computation*.
Oxford University Press, 2009.
- Moskewicz et al. (2001)
Matthew W Moskewicz, Conor F Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik.
Chaff: Engineering an efficient sat solver.
In *Proceedings of the 38th annual Design Automation Conference*, pp. 530–535, 2001.
- Nagatsuka et al. (2021)
Koichi Nagatsuka, Clifford Broni-Bediako, and Masayasu Atsumi.
Pre-training a bert with curriculum learning by increasing block-size of input text.
In *Proceedings of the International Conference on Recent Advances in Natural Language Processing (RANLP 2021)*, pp. 989–996, 2021.
- Osa et al. (2018)
Takayuki Osa, Joni Pajarinen, Gerhard Neumann, J Andrew Bagnell, Pieter Abbeel, Jan Peters, et al.
An algorithmic perspective on imitation learning.
*Foundations and Trends® in Robotics*, 7(1-2):1–179, 2018.
- Pan et al. (2025)
Leyan Pan, Vijay Ganesh, Jacob Abernethy, Chris Esposo, and Wenke Lee.
Can transformers reason logically? a study in SAT solving.
In *International Conference on Machine Learning*, 2025.
URL [https://openreview.net/forum?id=5BGC2I2fxx](https://openreview.net/forum?id=5BGC2I2fxx).
- Plaisted & Greenbaum (1986)
David A Plaisted and Steven Greenbaum.
A structure-preserving clause form translation.
*Journal of Symbolic Computation*, 2(3):293–304, 1986.
- Pomerleau (1991)
Dean A Pomerleau.
Efficient training of artificial neural networks for autonomous navigation.
*Neural computation*, 3(1):88–97, 1991.
- Pouransari et al. (2024)
Hadi Pouransari, Chun-Liang Li, Jen-Hao Chang, Pavan Kumar Anasosalu Vasu, Cem Koc, Vaishaal Shankar, and Oncel Tuzel.
Dataset decomposition: Faster llm training with variable sequence length curriculum.
In *Advances in Neural Information Processing Systems*, volume 37, pp. 36121–36147, 2024.
- Scarselli et al. (2008)
Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfardini.
The graph neural network model.
*IEEE transactions on neural networks*, 20(1):61–80, 2008.
- Selman et al. (1996)
Bart Selman, David G Mitchell, and Hector J Levesque.
Generating hard satisfiability problems.
*Artificial intelligence*, 81(1-2):17–29, 1996.
- Selsam & Bjørner (2019)
Daniel Selsam and Nikolaj Bjørner.
Guiding high-performance sat solvers with unsat-core predictions.
In *International conference on theory and applications of satisfiability testing*, pp. 336–353. Springer, 2019.
- Selsam et al. (2019)
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill.
Learning a SAT solver from single-bit supervision.
In *International Conference on Learning Representations*, 2019.
URL [https://openreview.net/forum?id=HJMC_iA5tm](https://openreview.net/forum?id=HJMC_iA5tm).
- Shi et al. (2023)
Zhengyuan Shi, Min Li, Yi Liu, Sadaf Khan, Junhua Huang, Hui-Ling Zhen, Mingxuan Yuan, and Qiang Xu.
Satformer: Transformer-based unsat core learning.
In *2023 IEEE/ACM International Conference on Computer Aided Design (ICCAD)*, pp. 1–4. IEEE, 2023.
- Silva & Sakallah (1996)
JP Marques Silva and Karem A Sakallah.
Grasp-a new search algorithm for satisfiability.
In *Proceedings of International Conference on Computer Aided Design*, pp. 220–227. IEEE, 1996.
- Vaswani et al. (2017)
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin.
Attention is all you need.
In *Advances in Neural Information Processing Systems*, volume 30, 2017.
- Wang et al. (2024)
Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth McMillan, and Risto Miikkulainen.
Neuroback: Improving CDCL SAT solving using graph neural networks.
In *The Twelfth International Conference on Learning Representations*, 2024.
URL [https://openreview.net/forum?id=samyfu6G93](https://openreview.net/forum?id=samyfu6G93).
- Warners & Van Maaren (1998)
Joost P Warners and Hans Van Maaren.
A two-phase algorithm for solving a class of hard satisfiability problems.
*Operations research letters*, 23(3-5):81–88, 1998.
- You et al. (2019)
Jiaxuan You, Haoze Wu, Clark Barrett, Raghuram Ramanujan, and Jure Leskovec.
G2sat: Learning to generate sat formulas.
In *Advances in Neural Information Processing Systems*, volume 32, 2019.
- Zare et al. (2024)
Maryam Zare, Parham M Kebria, Abbas Khosravi, and Saeid Nahavandi.
A survey of imitation learning: Algorithms, recent developments, and challenges.
*IEEE Transactions on Cybernetics*, 2024.
- Zarpellon et al. (2021)
Giulia Zarpellon, Jason Jo, Andrea Lodi, and Yoshua Bengio.
Parameterizing branch-and-bound search trees to learn branching policies.
In *Proceedings of the AAAI Conference on Artificial Intelligence*, volume 35, pp. 3931–3939, 2021.
- Zhai & Ge (2025)
Shumao Zhai and Ning Ge.
Learning splitting heuristics in divide-and-conquer SAT solvers with reinforcement learning.
In *The Thirteenth International Conference on Learning Representations*, 2025.
URL [https://openreview.net/forum?id=uUsL07BsMA](https://openreview.net/forum?id=uUsL07BsMA).
- Zhang & Malik (2002)
Lintao Zhang and Sharad Malik.
The quest for efficient boolean satisfiability solvers.
In *International conference on computer aided verification*, pp. 17–36. Springer, 2002.

## Appendix A Algorithm

The integration of the CDCL and ImitSAT is shown in Algorithm [1](https://arxiv.org/html/2509.25411v1#alg1).

Figure: Algorithm 1 Online CDCL branch with ImitSAT.

## Appendix B Datasets

This section details the training corpus, held‑out test sets, and the structured SAT families used in evaluation.
For the synthetic data, both train and test, all instances are random 3-SAT with a planted assignment and a clause–variable ratio in $[4.1,\,4.4]$ (Mezard & Montanari, 2009; Achlioptas et al., 2000; 2005).
We categorize instances by the number of variables $n_{v}$ to control difficulty and balance the number of decision probes contributed by each category.
Since larger $n_{v}$ produces longer trails and thus more supervision per instance, we allocate fewer instances at larger $n_{v}$. This ensures each bucket contributes a similar amount of training signal.
We define buckets as ranges of variable counts (e.g., “5–15”), with each bucket grouping instances by the number of variables $n_{v}$ they contain.

#### Training dataset.

Counts denote the number of CNF instances per bucket.

**Table 3: Training buckets for random 3-SAT with a planted assignment.**
| Bucket (variables $n_{v}$) | # Instances |
| --- | --- |
| 5–15 | 2,000,000 |
| 16–30 | 1,000,000 |
| 31–60 | 500,000 |
| 61–100 | 100,000 |
| 50 | 1,000,000 |
| 100 | 100,000 |

#### Held‑out test buckets.

To keep evaluation time reasonable, we use fewer instances at larger $n_{v}$. For $n_{v}{=}100$, we increase the sample size to reduce variance.

**Table 4: Held‑out test buckets for random 3–SAT.**
| Bucket (variables $n_{v}$) | # Instances |
| --- | --- |
| 5–15 | 5,000 |
| 16–30 | 5,000 |
| 31–60 | 1,000 |
| 61–100 | 100 |
| 50 | 100 |
| 100 | 500 |

#### Structured families from SATLIB.

To assess cross‑distribution generalization, we evaluate on classic structured benchmarks from SATLIB (Hoos & Stützle, 2000).
The suite spans both SAT and UNSAT, and includes 3-SAT and non–$k$–SAT regimes.
Specifically, we use AIM (Asahiro et al., 1996), which is equivalent to 3-SAT, focusing on the $n_{v}=100$ SAT portion. We also consider the SAT subset of JNH (Selman et al., 1996) with $n_{v}=100$ and PARITY (Warners & Van Maaren, 1998; Hoos & Stützle, 2000) in the compressed series, both as structured SAT families distinct from our random generator. Additionally, PRET (Johnson & Trick, 1996; Hoos & Stützle, 2000) is a two-coloring UNSAT problem with $n_{v}=60$, and the pigeonhole principle (PHOLE) (Haken, 1985) is used as a non–$k$–SAT and UNSAT stress test.
All subsets described above are considered with $n_{v}\leq 100$.
Table [5](https://arxiv.org/html/2509.25411v1#A2.T5) lists the families.

**Table 5: The structured families referenced in our generalization experiments are all sourced from SATLIB.**
| Family | $k$–SAT ? | SAT/UNSAT |
| --- | --- | --- |
| AIM | 3–SAT | SAT |
| JNH | non–$k$–SAT | SAT |
| PARITY | non–$k$–SAT | SAT |
| PHOLE | non–$k$–SAT | UNSAT |
| PRET | non–$k$–SAT | UNSAT |

## Appendix C CDCL runtime breakdown

To quantify the main cost drivers in CDCL, we instrument the Python MiniSAT on the 61–100 test range and time each major component. Table [6](https://arxiv.org/html/2509.25411v1#A3.T6) and Figure [2](https://arxiv.org/html/2509.25411v1#S4.F2) show that propagation accounts for about 89% of the mean runtime, conflict analysis for about 9%, and decision selection for under 2%. Reducing needless propagation is therefore the most direct path to wall‑clock gains.

**Table 6: The CDCL runtime breakdown on the 61–100 test set. Propagation dominates the runtime, motivating metrics and methods that reduce propagation.**
| Event | mean ms | median ms | share of mean % |
| --- | --- | --- | --- |
| Propagation | 65.624 | 38.378 | 88.88 |
| Conflict | 6.809 | 3.999 | 9.22 |
| Decision | 1.400 | 0.975 | 1.90 |

## Appendix D KeyTrace replay

We confirm KeyTrace is a suitable expert because replaying it yields a near conflict-free run with far fewer propagations.
To demonstrate its effectiveness, for each instance, we replay the extracted KeyTrace by applying its decisions in order and running unit propagation after each step. As shown in Table [7](https://arxiv.org/html/2509.25411v1#A4.T7) and Figure [3](https://arxiv.org/html/2509.25411v1#S4.F3), the event counts during the KeyTrace replay can be compared to those of the original MiniSAT run. Notably, conflicts are essentially eliminated, decisions drop by about 80%, and propagations fall to roughly 4% of the MiniSAT total. Together, these results support using KeyTrace as the expert for behavior cloning: it isolates the surviving branch sequence and removes the detours that drive most propagation.

**Table 7: Effect of KeyTrace replay on the 61–100 range. Means over instances and the share relative to MiniSAT. Replay is nearly conflict‑free and uses only a small fraction of propagation.**
| Event | MiniSAT mean | KeyTrace mean | KeyTrace as % of MiniSAT |
| --- | --- | --- | --- |
| Conflict | 71.96 | 0.11 | 0.15% |
| Decision | 103.94 | 20.38 | 19.61% |
| Propagation | 1474.64 | 62.74 | 4.25% |

## Appendix E Early decisions shape CDCL

This section examines whether the time at which the model is queried affects the overall search.
On the 5–15 test set, we compare two 1-call schedules under identical compute budgets: (1) query ImitSAT at the first branching decision, or (2) make three VSIDS decisions before querying ImitSAT once. All other decisions use the native VSIDS heuristic.
We report MRPP $\tilde{r}$ and the $1\%$ win rate $W_{1\%}$.
Table [8](https://arxiv.org/html/2509.25411v1#A5.T8) shows that delaying the single query (2) does not reduce propagations and greatly lowers the win rate. In contrast, a front‑loaded query (1) improves both metrics. This supports allocating the model budget to early decisions, as they significantly shape the search.

**Table 8: Early guidance is more effective. One model call on the 5–15 test set. Front‑loading the call at the first decision yields larger gains than delaying it.**
| Method | $\tilde{r}$ ($\downarrow$) | $W_{1\%}$ ($\uparrow$) |
| --- | --- | --- |
| call after 3 VSIDS | 1.00 | 0.27 |
| call at first decision | 0.91 | 0.55 |

## Appendix F Variable Permutation Augmentation

Permutation augmentation is designed to mitigate overfitting and enhance the robustness of the learner.
We train models on 5–15 variables for 20 epochs, or about 300k steps.
Figure [5](https://arxiv.org/html/2509.25411v1#A6.F5) plots the training and validation losses. With permutation augmentation, the two curves track each other and decay steadily. Without augmentation, the training loss continues to decrease, while the validation loss peaks early and then rises, a classic sign of overfitting to variable identities. The aggregate metrics confirm this, as in Table [9](https://arxiv.org/html/2509.25411v1#A6.T9) that removing permutation leads to a higher MRPP $\tilde{r}$ and a low win rate, whereas the augmented model achieves a strong MRPP $\tilde{r}$ and a much higher win rate $W_{1\%}$. The slightly higher training loss under augmentation is expected, as the task is more challenging; however, the gain is evident in generalization.

Figure: Figure 5: Training and validation loss curves with and without variable‑permutation augmentation on the 5–15 range for 20 epochs. Permutation keeps training and validation closely aligned and prevents overfitting, while removing it lowers training loss but drives validation loss up.
Refer to caption: x5.png

**Table 9: Effect of variable‑permutation augmentation. Models trained on 5–15 for 20 epochs. Augmentation prevents overfitting and improves test set metrics.**
| Method | $\tilde{r}$ ($\downarrow$) | $W_{1\%}$ ($\uparrow$) |
| --- | --- | --- |
| w/o permutation | 1.00 | 0.28 |
| w/ permutation | 0.75 | 0.64 |

## Appendix G Staged curriculum across variable ranges

The staged curriculum is designed to accelerate learning and maintain competence across a wide range of variables (Nagatsuka et al., 2021; Pouransari et al., 2024).
The curriculum trains on 5–15 for 20 epochs, then continues on 16–30 for 4 epochs, about 130k steps in the second stage. Two baselines are used on 16–30 without any curriculum. The first matches the second‑stage budget by only about 130k steps. The second uses a total of 430k steps that match the curriculum training steps.

Table [10](https://arxiv.org/html/2509.25411v1#A7.T10) summarizes the results. At the matched 130k steps budget on 16–30, the staged model achieves a much lower $\tilde{r}$ and a higher $W_{1\%}$ than training the model “w/o stage” from scratch; this shows clear sample efficiency. When step counts are fully matched as “w/o stage*”, training from scratch on 16–30 narrows the gap and slightly edges out the staged model in that range. This suggests that the primary benefit of the curriculum is faster and more stable convergence, rather than better performance. Crucially, when the curriculum progresses through all stages, it preserves strong performance on 5–15, whereas models trained only on 16–30 fail to generalize to smaller instances.

**Table 10: Stage‑training ablation. Ours uses a curriculum that trains on 5–15 for 300k steps, then continues on 16–30 for 130k steps. The *w/o stage* trains only on 16–30 with the same second‑stage budget, about 130k steps. And *w/o stage** trains only on 16–30 with a total of about 430k steps that matches the overall curriculum steps. Curriculum improves sample efficiency and yields better coverage of the 5–15 range.**
| Method | 5-15 $\tilde{r}$ ($\downarrow$) | 5-15 $W_{1\%}$ ($\uparrow$) | 16-30 $\tilde{r}$ ($\downarrow$) | 16-15 $W_{1\%}$ ($\uparrow$) |
| --- | --- | --- | --- | --- |
| w/o stage | 1.00 | 0.05 | 1.00 | 0.49 |
| w/o stage* | 1.00 | 0.43 | 0.80 | 0.66 |
| w/ stage | 0.75 | 0.67 | 0.83 | 0.63 |

## Appendix H KeyTrace Example

This section walks through Figure [1](https://arxiv.org/html/2509.25411v1#S3.F1) on an example instance, showing a short CDCL run and how it collapses into a KeyTrace.
Consider the CNF $F$ over $x_{1},x_{2},x_{3},x_{4}$,

$$ $\displaystyle F=$ $\displaystyle(x_{1}\vee x_{2}\vee\lnot x_{3})\;\wedge\;(\lnot x_{4}\vee\lnot x_{2}\vee\lnot x_{3})\;\wedge\;(x_{1}\vee x_{3}\vee\lnot x_{4}\vee x_{2})$ (17) $\displaystyle\wedge\;(\lnot x_{3}\vee\lnot x_{1}\vee\lnot x_{4})\;\wedge\;(x_{3}\vee\lnot x_{4}\vee\lnot x_{2})\;\wedge\;(\lnot x_{2}\vee x_{4}\vee x_{3}).$ $$

#### One CDCL trail.

A CDCL run interleaves decisions ($\mathtt{D}$), unit propagations ($\mathtt{A}$), and backtracks ($\mathtt{BT}$), each annotated with the decision level.
One plausible trail is

$$ $\begin{split}\mathcal{T}=\big(&(\mathtt{D},+4,1),\;(\mathtt{D},+3,2),\;(\mathtt{BT},-3,1),\;\\ &(\mathtt{BT},-4,0),\;(\mathtt{D},+1,1),\;(\mathtt{D},+2,2),\;(\mathtt{A},-3,2)\;\big)\end{split}$ (18) $$

It can be read in three stages, matching the left panel of Figure [1](https://arxiv.org/html/2509.25411v1#S3.F1).
*Stage 1:* branch $x_{4}=\top$, then $x_{3}=\top$; a conflict is reached and the solver backtracks, forcing $x_{3}=\bot$ at a lower level.
*Stage 2:* a second conflict occurs and the run backtracks to level 0, flipping the earlier choice to $x_{4}=\bot$.
*Stage 3:* branch $x_{1}=\top$ and $x_{2}=\top$; unit propagation assigns $x_{3}\!=\!\bot$, and all clauses are satisfied, so $F$ is declared SAT.

#### Collapsing to a KeyTrace.

Applying the extraction rule in Equation [7](https://arxiv.org/html/2509.25411v1#S4.E7) trims away backtracked suffixes and keeps only the surviving root–to–current decisions.
For the trail above, the resulting expert KeyTrace is

$$ $\mathcal{K}=\bigl((\mathtt{BT},-4,0),\;(\mathtt{D},+1,1),\;(\mathtt{D},+2,2),\;(\mathtt{A},-3,2)\bigr),$ (19) $$

i.e., the final branch $x_{4}=\bot\rightarrow x_{1}=\top\rightarrow x_{2}=\top$ and then propagate $x_{3}=\bot$ shown in the right panel of Figure [1](https://arxiv.org/html/2509.25411v1#S3.F1).
Replaying $\mathcal{K}$ on the same instance with unit propagation between steps is nearly conflict‑free and avoids the detours taken in the original run, which is why KeyTrace provides clean targets for imitation.

## Appendix I Large Language Models (LLMs) Usage Statement

We used LLMs as general‐purpose assistants to scaffold small analysis or plotting scripts, suggest debugging tips, and polish wording. All technical ideas, algorithms, model designs, experiments, and reported results are the sole responsibility of the authors. LLM outputs were reviewed and edited for correctness and clarity. No proprietary data were provided to LLMs, and LLMs are not authors.

## Appendix J Ethics statement

This work uses procedurally generated SAT instances and public SATLIB benchmarks; no human subjects or personally identifiable information are involved. The research poses minimal foreseeable risks to society. We will release code and models under a permissive license to encourage transparent and responsible use.

## Appendix K Reproducibility statement

We will release the following: (i) pretrained models; (ii) our Python reimplementation of MiniSAT 2.2, as well as the integration code for ImitSAT; (iii) training code, including all hyperparameters; (iv) generators for random planted 3-SAT data, along with the exact train/test datasets; and (v) environment specifications. The dataset definitions and splits are detailed in Appendix [B](https://arxiv.org/html/2509.25411v1#A2).

## Appendix L Limitations

The study was limited by computational resources, as all models were trained on four V100 GPUs, which restricted both model size and training duration. To address these constraints, staged curriculum learning was used to accelerate training. With greater access to GPUs, it would be possible to train models for longer periods on larger datasets and scale model size, potentially leading to improvements in imitation quality and wall-clock performance.

## Peer Reviews

confidence: 3
contribution: 2
initial_rating: 4
presentation: 3
questions: How does the efficiency of ImitSAT maintain as the size of the SAT problem changes? To what sized instance can it generalize?

How is the query budget determined?
soundness: 2
strengths: The paper is easy to follow and the idea is simple but effective. 

The method is well-motivated by the run-time analysis that propagation is the most time-consuming part of CDCL solving.

The algorithm introduces a budget for querying the model to ensure efficiency.

The approach shows good performance, beating Graph-Q-SAT and SATFormer on structured SAT families outside of training distribution.
summary: Conflict Driven Clause Learning (CDCL) is the state of the art approach for solving boolean satisfiability (SAT) problems. During CDCL solving, the majority of the solving time is spent on unit propagation, the efficiency of which is heavily influenced by the branching decisions quality.

This paper introduces ImitSAT, which learns to branch in a CDCL solver using imitation learning. To do this, key traces are first extracted by collapsing a CDCL branching search tree into a single sequence of decisions. Then, an autoregressive learner is trained to predict the key traces sequentially through imitation learning. By learning to make better quality branching decisions, ImitSAT is able to cut down solving time. Experiments show that ImitSAT outperforms SATFormer and Graph-Q-SAT.
weaknesses: The idea of using imitation learning for branching is not new. For example, it has been successfully applied to guide branch-and-bound for mixed integer programming [1,2].

The algorithm consumes the query budgets greedily, which, given the limited budget could potentially be far from optimal for instances larger than those in Appendix E. Are there simple heuristics that can improve this?

The experiments are on very small sized SAT problems, which provides limited insight to how ImitSAT can be used in practice.

Training is computationally expensive, since CDCL solvers are used to solve a problem entirely to produce a single key trace as a training instance. Therefore, the generalization ability of the method is crucial and calls for a deeper look. 


[1] He H, Daumé H, Eisner J. Learning to search in branch and bound algorithms. Advances in neural information processing systems. 2014;27.

[2] Khalil E, Le Bodic P, Song L, Nemhauser G, Dilkina B. Learning to branch in mixed integer programming. InProceedings of the AAAI conference on artificial intelligence 2016 Feb 21 (Vol. 30, No. 1).

---

confidence: 3
contribution: 3
initial_rating: 8
presentation: 3
questions: 1. Have you tried applying your method to industrial benchmarks like SATCOMP? It does not have to outperform the baseline solver, but it would be good to know where ImitSAT stands in real-world settings. 
2. How does the performance look if you only use the model decisions? 
3. Have you experimented with higher query budgets than 5? It would be interesting to plot performance over query budget. 
4. Equation (10) does not index $F_{DIMACS}$ by $t$, so is it always the original input formula? That is, does it not include the learned clauses? If so, wouldn't that compromise the decision optimality since the model does not see the clauses that were learned during the run? 
5. When the model's top answer is illegal, you fall back to the VSIDS heuristic. Why not mask out the illegal variable decisions from the model's output logits/probabilities? In doing so, you could use the model's top legal decision. 
6. In Figure 4, can you also include the time of the baseline un-augmented MiniSAT solver? 
7. Have you considered bootstrapping the training process by using the model to improve the trails dataset? For example, whenever the model produces a trail with fewer propagations, you could use the produced model trail for subsequent epochs instead of the KeyTrace one. 
8. Were the two baselines trained on the same 3-SAT dataset on which ImitSAT was trained, or were they trained on their original papers' datasets? 
9. Can you also include the KeyTrace ratios in Tables 1 & 2? 
10. To see the time scaling with query budgets, can you include the 5-call ImitSAT to Figure 4, possibly accompanied by higher query budget variants?
soundness: 3
strengths: 1. The paper is clear and easy to follow. 
2. The key idea is fairly interesting: distilling a post-processed solver policy into a neural network. 
3. The authors compare their method against two somewhat recent baselines. 
4. The paper evaluates the method on both in-distribution and out-of-distribution instances.
5. The method outperforms the reported baselines while having a lower runtime.
summary: The paper introduces ImitSAT, a framework for learning a CDCL decision policy by imitation learning on condensed solver runs. This works by post-processing solver trails to eliminate intermediate conflicts and backtracking steps, which results in compact trails that only contain the key decisions made by the solver. In doing so, the model learns to imitate an improved version of the underlying solver, which can then be used to guide the solver decisions under a certain query budget. The authors compare their method to two other learned hybrid solvers, namely GQSAT and SATformer, in terms of solver-relative performance and wall-clock time on both in-distribution and out-of-distribution benchmarks. Results show that ImitSAT considerably outperforms both baselines on almost all benchmarks under a much lower runtime.
weaknesses: 1. The authors do not evaluate their method on industrial instances, so it's unclear how well it scales to real-world settings. 
2. The attempted query budgets are quite low (up to 5 decisions), so it's unclear how well the method scales with higher budgets. 
3. Wall clock time comparisons are missing the pure VSIDS heuristic baseline (i.e., without the model), which would be the ultimate test to see if the proposed method speeds up the CDCL solver. 
4. It is unclear in Section 5.1 whether the SATformer and Graph-Q-SAT baseline models were pertrained on their original papers' dataset or on the same random 3-SAT dataset that ImitSAT was trained on. If it's the former, then the comparison in Table 1 is quite unfair since the baselines were trained on a different dataset. 
5. Using a text model is arguably not ideal for embedding formulas compared to GNNs as it fails to capture key properties such as invariance to clause permutation and variable renaming. However, I do understand that it might be more convenient to work with text.

---

confidence: 4
contribution: 3
initial_rating: 6
presentation: 3
questions: Please reply to my comments listed in ‘Weaknesses’.
soundness: 3
strengths: 1. The paper is generally well-written, with clear explanations.

2. The description of the dataset construction method is detailed and reasonable.

3. Experimental results are satisfactory.
summary: This paper studies SAT problem. As claimed by the authors, previous learning-based method were limited. In this work, they propose a branching policy for CDCL SAT solvers based on imitation learning. The authors conduct experiments to evaluate the effectiveness of their approach. They claim that their proposed method reduces propagation counts and outperforms previous learning-based method.
weaknesses: 1. What is the SAT solver integrated by SATformer in the experiment? According to the SATformer paper, combining it with CaDiCaL and Kissat can produce performance improvements.

2. MiniSAT, used by ImitSAT, is relatively outdated. How does ImitSAT perform compared to current SOTA solvers (such as Kissat and CaDiCaL)? Can combining ImitSAT with these solvers bring further performance improvements?


Decision: Accept (Poster)