# Boolean Satisfiability via Imitation Learning

arXiv: https://arxiv.org/abs/2509.25411 · HTML: https://mlsanity.com/paper/2509.25411/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Imitation learning methods, one of 13 directions in Offline RL and imitation learning from data.
- Builds on 19 of its 50 references that are in the map.
- First posted on arXiv 29 Sep 2025.

## Placed in

- Offline RL and imitation learning from data / [Imitation learning methods](https://mlsanity.com/offlinerl/imitation-learning-methods/)

## Builds on (most cited first, 19 of 19)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Decision Transformer: Reinforcement Learning via Sequence Modeling](https://mlsanity.com/paper/2106.01345/) (2021)
- [An Algorithmic Perspective on Imitation Learning](https://mlsanity.com/paper/1811.06711/) (2018)
- [Exact Combinatorial Optimization with Graph Convolutional Neural Networks](https://mlsanity.com/paper/1906.01629/) (2019)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [A Survey of Imitation Learning: Algorithms, Recent Developments, and Challenges](https://mlsanity.com/paper/2309.02473/) (2023)
- [Parameterizing Branch-and-Bound Search Trees to Learn Branching Policies](https://mlsanity.com/paper/2002.05120/) (2020)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [General-purpose, long-context autoregressive modeling with Perceiver AR](https://mlsanity.com/paper/2202.07765/) (2022)
- [MLPInit: Embarrassingly Simple GNN Training Acceleration with MLP Initialization](https://mlsanity.com/paper/2210.00102/) (2022)
- [Dataset Decomposition: Faster LLM Training with Variable Sequence Length Curriculum](https://mlsanity.com/paper/2405.13226/) (2024)
- [G2SAT: Learning to Generate SAT Formulas](https://mlsanity.com/paper/1910.13445/) (2019)
- [NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks](https://mlsanity.com/paper/2110.14053/) (2021)
- [G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks](https://mlsanity.com/paper/2309.16941/) (2023)
- [Graph Sparsification via Mixture of Graphs](https://mlsanity.com/paper/2405.14260/) (2024)
- [Can Transformers Reason Logically? A Study in SAT Solving](https://mlsanity.com/paper/2410.07432/) (2024)
- [SATformer: Transformer-Based UNSAT Core Learning](https://mlsanity.com/paper/2209.00953/) (2022)
- [RSC: Accelerating Graph Neural Networks Training via Randomized Sparse Computations](https://mlsanity.com/paper/2210.10737/) (2022)
- [Global Benchmark Database](https://mlsanity.com/paper/2405.10045/) (2024)

## Abstract (arXiv)

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