PaperlayerView exact revision on arXiv

Source-linked AI summary

Boolean Satisfiability via Imitation Learning

Zewei Zhang, Huan Liu, Yuanhao Yu, Jun Chen, Xiangyu Xu

arXiv:2509.25411v2cs.AIcs.LG

TL;DR

SAT solvers rely on CDCL branching, but existing learned guidance is indirect or uses reinforcement learning with limited execution history. ImitSAT imitates surviving decisions from expert KeyTraces as prefix-conditioned branching predictions. It reduces propagations and runtime across evaluated settings, often outperforming prior learned approaches.

  • Problem

    Learned CDCL branching has relied on indirect instance-level signals or reinforcement learning that uses limited execution history, while branching quality matters because propagation often dominates runtime.

    Source: §1 · p. 1

  • Method

    ImitSAT collapses solver runs into KeyTraces of surviving decisions and trains a prefix-conditioned autoregressive policy to predict the next branch from dense expert supervision.

    Source: §1 · pp. 1–2

  • Results

    ImitSAT reduces propagations and achieves favorable runtime, outperforming SATformer and Graph-Q-SAT across most evaluated settings while matching them elsewhere.

    Source: §1 · p. 2

  • Takeaways & Limitations

    Replaying KeyTrace decisions on the same instance is nearly conflict-free and reduces propagation events to approximately 4% of those in the raw MiniSAT trail.

    Source: §4.1 · p. 5

    Training was limited to four V100 GPUs, restricting model size and training duration.

    Source: L LIMITATIONS · p. 19

Abstract

from arXiv · show

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

ImitSAT learns CDCL branching from surviving decisions in expert solver traces, addressing limits of indirect instance-level guidance and exploration-heavy reinforcement learning. It reduces propagations and runtime across varied SAT settings, often outperforming prior learned methods.

1 INTRODUCTION

  • Because unit propagation often dominates runtime, more informed branching can translate into faster solving.Source: §1 · p. 1
  • Prior learned guidance either adjusts variable activities only at initialization or uses reinforcement learning with sparse rewards, delayed feedback, and limited execution history.The paper contrasts SATformer’s indirect influence during branching with Graph-Q-SAT’s online agent.Source: §1 · p. 1
  • At inference, ImitSAT predicts the next signed variable from the instance and KeyTrace prefix, then falls back to the native heuristic when uncertain.A small query budget is used, while other CDCL components remain unchanged.Source: §1 · p. 2
  • ImitSAT reduces propagations and achieves favorable runtime, outperforming SATformer and Graph-Q-SAT across most evaluated settings while matching their performance elsewhere.Evaluation includes random 3-SAT and structured satisfiable, unsatisfiable, and non-k-SAT families; training only on random 3-SAT transfers to unsatisfiable and non-k-SAT benchmarks without modification.Source: §1 · p. 2
  • ImitSAT learns branching from expert traces collapsed into surviving decisions, providing dense decision-level supervision for autoregressive sequence modeling.The paper describes these traces as clean, conflict-free training targets aligned with prefix-conditioned branching.Source: §1 · pp. 1–2

2 RELATED WORKS

Prior SAT learning work includes instance-level prediction and learned solver components, while imitation learning has also been applied to control and mixed-integer optimization. ImitSAT instead imitates full CDCL KeyTraces, whose search dynamics differ from those of MIP branch-and-bound.

Related SAT guidance

  • Existing neural SAT work predicts instance outcomes or guides particular solver components, including clause deletion, phase initialization, and branching.Graph-Q-SAT queries an online reinforcement-learning agent during search, whereas SATformer initializes CDCL in a way that indirectly influences later branching.Source: §2 · p. 2

Imitation learning

  • Imitation learning maps expert demonstrations to actions, and related work applies learned branching policies to mixed-integer programming branch-and-bound.The passage also connects autoregressive sequence modeling to next-action prediction in control.Source: §2 · p. 2

ImitSAT

  • Figure 1 contrasts a CDCL run containing backtracks with a KeyTrace that retains only surviving decisions as the expert sequence for imitation.Source: Figure 1 · p. 3

Imitation learning

  • MIP branch-and-bound has a monotone search tree and node-local feedback, whereas CDCL uses non-monotone search, restarts, clause learning, and delayed non-local feedback.Prior MIP approaches typically learn local ranking models, while ImitSAT trains an autoregressive Transformer to imitate entire CDCL KeyTraces.Source: §2 · p. 3

ImitSAT

  • ImitSAT trains a prefix-conditioned next-decision model on compact sequences of surviving decisions to provide dense supervision at low per-query cost.The paper states these design choices help reduce propagation and improve wall-clock time under small query budgets.Source: §2 · p. 3

3 PRELIMINARIES ON SAT

The preliminaries define SAT formulas and common encodings, then describe CDCL search and its branching heuristics. They emphasize that branching choices affect propagation and conflict costs.

Boolean Satisfiability Problem

  • SAT asks whether a Boolean formula can be made true by assigning each variable true or false; an assignment satisfies the formula when every clause is satisfied.A literal is a variable or its negation, and a clause is a disjunction of literals.Source: §3 · p. 3
  • In k-SAT each clause contains exactly k literals, and 3-SAT is highlighted as an NP-complete case used in theory and empirical benchmarks.Source: §3 · p. 3
  • DIMACS CNF encodes each clause as nonzero integers terminated by 0, with i denoting variable x_i and −i its negation.The paper notes this compact representation is convenient for algorithmic solvers and sequence-based models.Source: §3 · p. 4

Conflict-driven Clause Learning

  • CDCL alternates decisions, unit propagation, and backtracking after conflicts, with learned clauses supporting non-chronological jumps.A level-0 conflict establishes UNSAT, while a complete conflict-free assignment proves SAT.Source: §3 · p. 4

Branching Heuristic and Implementation

  • Branching selects a variable and polarity, and decision quality affects propagation and conflict counts; VSIDS prioritizes variables using decaying activity scores.Activity increases when variables appear in learned clauses and is periodically decayed.Source: §3 · p. 4

4 IMITSAT

ImitSAT learns CDCL branching by distilling solver runs into surviving-decision KeyTraces and predicting the next branch from the instance and trace prefix. Replaying a KeyTrace on the same instance is nearly conflict-free and uses about 4% of the propagations in the raw MiniSAT trail.

4.1 EXPERT KEYTRACE REPLAY

  • KeyTrace removes decision and propagation events undone by backtracking, while restarts reset the working sequence to level 0.This yields a shorter, more stable trail representation of the context needed to advance the search.Source: §4.1 · p. 5
  • On the same instance, KeyTrace replay is nearly conflict-free and uses about 4% of the propagations in the raw MiniSAT trail.The extracted trace preserves surviving decisions and removes search detours.Source: §4.1 · p. 5

4.2 AUTOREGRESSIVE IMITATION FOR CDCL BRANCHING

  • The learner predicts the next signed variable from formula F and a KeyTrace prefix, using behavior cloning on expert decisions.Each surviving decision, together with its implied propagations, supplies a supervised target.Source: §4.2 · pp. 5–6
  • Serialization places the DIMACS formula before the KeyTrace blocks and ends with [D], so the next branch is the next-symbol prediction.Decision literals are followed by their propagated unit assignments; level fields and assignment tags are omitted.Source: §4.2 · p. 6
  • At inference, legal predictions are accepted within a small query budget; illegal predictions fall back to VSIDS.The design preserves completeness and keeps overhead small.Source: §4.2 · p. 7

5 EXPERIMENTS

Experiments compare ImitSAT with learned and classical solvers on random and structured SAT instances, assess runtime and generalization, and examine training techniques.

5.1 IMPLEMENTATION DETAILS

  • The evaluation uses MiniSAT 2.2, SATformer and Graph-Q-SAT baselines, planted random 3-SAT data, and median-normalized propagation metrics.The Perceiver AR learner uses one output latent, giving each query O(N) complexity rather than the O(N^2) cost of a standard Transformer decoder.Source: §5.1 · p. 7

5.2 COMPARISON ON TEST SETS

  • ImitSAT has the lowest MRPP in nearly all random 3-SAT ranges and the highest W1% with 3 calls; Table 1 reports both metrics.It ties SATformer on 61–100 for MRPP.Source: Table 1 · p. 8, §5.2 · p. 8

5.3 GENERALIZATION ON SPECIAL SAT FAMILIES

  • Across structured families, ImitSAT attains the lowest MRPP or ties for best and has the highest or tied W1%, transferring without finetuning.The evaluation includes SAT and UNSAT, 3-SAT and non-k-SAT families, without retraining or tuning.Source: Table 2 · p. 9, §5.3 · p. 9

5.4 WALL-CLOCK TIME

  • On 61–100 instances, ImitSAT has the lowest wall-clock time overall; on 16–30 and 31–60, MiniSAT remains faster.Figure 4 compares end-to-end solver time with model-call costs included and preprocessing excluded.Source: §5.4 · pp. 9–10, Figure 4 · p. 10

5.5 IMPROVED TRAINING TECHNIQUES

  • Variable-permutation augmentation steadies validation loss, while a staged curriculum expands training from smaller to larger variable ranges.Without augmentation, validation loss peaks early and then rises despite continued training-loss decreases.Source: §5.5 · p. 10

6 CONCLUSION

The conclusion presents ImitSAT as an imitation-learned CDCL branching policy and summarizes its use of expert traces and experimental outcomes.

6 CONCLUSION

  • ImitSAT uses compact sequences of surviving decisions as expert traces for autoregressive branching, producing dense, conflict-free supervision.The conclusion reports reduced propagations, favorable runtime, and generalization beyond 3-SAT against prior learned methods.Source: §6 · p. 10

A ALGORITHM

  • Algorithm 1 extracts a KeyTrace prefix, queries the learner within its budget, and falls back to VSIDS if no query is available or the prediction is illegal.A legal prediction must be unassigned and within the variable range.Source: A ALGORITHM · p. 14
  • The online procedure returns UNSAT at a level-zero conflict and SAT when all variables are assigned.Source: A ALGORITHM · p. 14

B DATASETS

The datasets section describes the planted random 3-SAT corpus, held-out evaluation buckets, and structured SATLIB families; it also identifies propagation as the main CDCL runtime cost.

B DATASETS

  • Random planted 3-SAT instances are grouped by variable-count ranges, with fewer larger instances to balance the decision-probe supervision contributed by each bucket.Training and test instances use a clause–variable ratio in [4.1, 4.4].Source: B DATASETS · p. 14
  • Structured SATLIB evaluation spans SAT and UNSAT, 3-SAT and non-k-SAT families, with all selected subsets limited to at most 100 variables.The families include AIM, JNH, PARITY, PRET, and PHOLE.Source: B DATASETS · p. 15, Table 5 · p. 15

C CDCL RUNTIME BREAKDOWN

  • Propagation accounts for about 89% of mean runtime, conflict analysis about 9%, and decision selection under 2% on the 61–100 test range.The paper identifies reducing needless propagation as the most direct path to wall-clock gains.Source: C CDCL RUNTIME BREAKDOWN · p. 15, Table 6 · p. 15

D KEYTRACE REPLAY

KeyTrace replay nearly eliminates conflicts, reduces decisions by about 80%, and uses roughly 4% of MiniSAT’s propagations, supporting it as a behavior-cloning expert.

D KEYTRACE REPLAY

  • KeyTrace replay nearly eliminates conflicts, cuts decisions by about 80%, and uses roughly 4% of MiniSAT’s propagations, supporting its use as a behavior-cloning expert.The comparison replays extracted KeyTrace decisions in order, with unit propagation after each step.Source: D KEYTRACE REPLAY · pp. 15–16, Table 7 · p. 16

E EARLY DECISIONS SHAPE CDCL

On the SATCOMP subset, ImitSAT matches SATformer and improves wall-clock time over GQSAT on the hardest groups. The experiments also find benefits from early queries, permutation augmentation, and staged training, while bounding the evaluation by the tested settings and computational resources.

E EARLY DECISIONS SHAPE CDCL

  • On the 5–15 test set, querying ImitSAT at the first decision improves MRPP ˜r and W1% versus using three VSIDS decisions first; on 100 and AIM, three calls at search start achieve the best MRPP ˜r and W1%.The compared strategies use the same single-call compute budget in the 5–15 test; on 100 and AIM, subsequent decisions use native VSIDS.Source: E EARLY DECISIONS SHAPE CDCL · p. 16, Table 8 · p. 16, Table 9 · p. 16

F VARIABLE PERMUTATION AUGMENTATION

G STAGED CURRICULUM ACROSS VARIABLE RANGES

  • At a matched 130k-step budget on 16–30, staged training improves sample efficiency; with 430k steps, training from scratch slightly edges it in that range.The full curriculum preserves strong 5–15 performance, whereas models trained only on 16–30 fail to generalize to smaller instances.Source: G STAGED CURRICULUM ACROSS VARIABLE… · p. 17, Table 11 · p. 18

H KEYTRACE EXAMPLE

  • The example KeyTrace trims backtracked suffixes to retain surviving decisions, and replaying it with unit propagation is nearly conflict-free.In the illustrated run, the surviving branch is x4 = ⊥ → x1 = ⊤ → x2 = ⊤, followed by propagation of x3 = ⊥.Source: H KEYTRACE EXAMPLE · p. 18

I LARGE LANGUAGE MODELS (LLMS) USAGE STATEMENT

  • The authors used LLMs to scaffold small analysis or plotting scripts, suggest debugging tips, and polish wording; technical work and results remain their responsibility.LLM outputs were reviewed and edited, and no proprietary data were provided.Source: I LARGE LANGUAGE MODELS (LLMS) USAGE… · p. 18

J ETHICS STATEMENT

  • The study uses procedurally generated SAT instances and public SATLIB benchmarks, with no human subjects or personally identifiable information.The authors describe foreseeable societal risks as minimal.Source: J ETHICS STATEMENT · p. 18

L LIMITATIONS

  • Training on four V100 GPUs restricted model size and training duration, limiting the scale explored in this study.The authors suggest more GPUs could permit longer training on larger datasets and larger models, potentially improving imitation quality and wall-clock performance.Source: L LIMITATIONS · p. 19

M COMPARISON ON SATCOMP

  • On the hardest SATCOMP groups, ImitSAT is fastest and slightly outperforms SATformer in wall-clock time, while GQSAT develops a heavier time tail.Across easier and medium groups, GQSAT, SATformer, and ImitSAT behave similarly.Source: Figure 6 · p. 19, M COMPARISON ON SATCOMP · p. 19

N QUERY BUDGET ANALYSIS

ImitSAT’s query benefits diminish as calls accumulate, and the authors use three as the default budget. Its wall-clock advantage over learned baselines is clearest on harder random 3-SAT ranges.

N QUERY BUDGET ANALYSIS

  • Most propagation benefit comes from the first three queries, while calls beyond six provide only marginal gains, motivating a default budget of three.Each query introduces non-trivial latency, so propagation reductions must be weighed against query overhead.Source: Figure 7 · p. 20, N QUERY BUDGET ANALYSIS · p. 20

O WALL-CLOCK TIME COMPARISON WITH MINISAT

  • On 61–100 random 3-SAT, ImitSAT achieves the best wall-clock performance overall; on 16–30 it is faster than both learned baselines.On 31–60, ImitSAT and MiniSAT have almost identical runtimes, and both are substantially faster than the other learned methods.Source: O WALL-CLOCK TIME COMPARISON WITH… · p. 20

P EVALUATION OF NAIVE GNN COMBINATION

The tested naive GNN embedding substitution underperforms text-only ImitSAT and adds inference and training overhead. Top-K masking has little effect on simpler in-distribution sets but degrades performance on harder out-of-distribution sets.

P EVALUATION OF NAIVE GNN COMBINATION

  • Replacing CNF tokens with self-supervised GNN embeddings underperforms text-only ImitSAT and adds substantial training and inference overhead.The authors describe this as a naive integration that is neither more effective nor more efficient than the text-based model.Source: P EVALUATION OF NAIVE GNN COMBINATION · pp. 20–21, Table 13 · p. 21

Q TOP-K AND FALLBACK ANALYSIS

  • Top-K masking makes almost no difference on 5–15, 16–30, and 31–60, but degrades performance on the harder JNH and AIM datasets.The authors state that falling back to the original CDCL decision procedure is more reliable than forcing a low-confidence model prediction in these cases.Source: Q TOP-K AND FALLBACK ANALYSIS · p. 21

R INTEGRATION WITH ADVANCED SOLVERS

ImitSAT improves CaDiCaL’s branching performance while changing only the branching policy. With Kissat, heavy preprocessing can leave little opportunity for the branching callback to affect synthetic 3-SAT results.

CaDiCaL

Kissat

  • Kissat’s probing and lucky assignments often solve synthetic 3-SAT instances before CDCL decisions, leaving its branching callback rarely invoked.With default settings, Kissat and Kissat+ImitSAT have nearly identical relative propagation statistics on most random buckets; improvements are noticeable only on structured datasets.Source: R INTEGRATION WITH ADVANCED SOLVERS · p. 22
  • With Kissat probing disabled, Table 17 evaluates structured families using median propagation ratio and the fraction of instances with at least a 1% propagation reduction.Both metrics use Kissat without ImitSAT as the baseline.Source: Table 17 · p. 23
Loading 2509.25411v2…