Boolean Satisfiability via Imitation Learning
On the map: Offline RL and imitation learning from data → Imitation learning methods
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
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.
Builds on
19 of 50 references.
Closest ancestors · 2
Same direction, newest first
- 2023A Survey of Imitation Learning: Algorithms, Recent Developments, and Challenges5 Sep
- 2018An Algorithmic Perspective on Imitation Learning16 Nov
Other references · 17
- 2017Attention Is All You Needcited by 60,361
- 2021Decision Transformer: Reinforcement Learning via Sequence Modelingcited by 1,546
- 2019Exact Combinatorial Optimization with Graph Convolutional Neural Networkscited by 318
- 2018Learning a SAT Solver from Single-Bit Supervisioncited by 200
- 2020Parameterizing Branch-and-Bound Search Trees to Learn Branching Policiescited by 63
- 2019Guiding High-Performance SAT Solvers with Unsat-Core Predictionscited by 62
- 2022General-purpose, long-context autoregressive modeling with Perceiver ARcited by 60
- 2022MLPInit: Embarrassingly Simple GNN Training Acceleration with MLP Initializationcited by 31
- 2024Dataset Decomposition: Faster LLM Training with Variable Sequence Length Curriculumcited by 26
- 2019G2SAT: Learning to Generate SAT Formulascited by 20
- 2021NeuroBack: Improving CDCL SAT Solving using Graph Neural Networkscited by 19
- 2023G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networkscited by 18
5 more
- 2024Graph Sparsification via Mixture of Graphscited by 17
- 2024Can Transformers Reason Logically? A Study in SAT Solvingcited by 16
- 2022SATformer: Transformer-Based UNSAT Core Learningcited by 14
- 2022RSC: Accelerating Graph Neural Networks Training via Randomized Sparse Computationscited by 12
- 2024Global Benchmark Databasecited by 2
Built on by
Not cited yet.
Similar, not cited
Close in wording, no citation either way
- 2025Learning from Algorithm Feedback: One-Shot SAT Solver Guidance with GNNs
- 2026SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers
- 2024A Reinforcement Learning based Reset Policy for CDCL SAT Solvers
- 2023Learning Reliable Logical Rules with SATNet
- 2025Neural Approaches to SAT Solving: Design Choices and Interpretability
- 2026Imitation Learning for Connection-Tableau Construction
- 2026Learning How to Cube
- 2025SATURN: SAT-based Reinforcement Learning to Unleash LLMs Reasoning