More details, training/evaluation scripts, and ablations can be found in the
GitHub repository
and the paper.
Introduction
ImitSAT is 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, ImitSAT learns from expert KeyTrace—a sequence of surviving decisions from a full solver run. This prefix-conditioned supervision enables ImitSAT to reproduce high-quality branches, reducing propagations and wall-clock time.
1@inproceedings{zhang2026boolean,
2 title={Boolean Satisfiability via Imitation Learning},
3 author={Zewei Zhang and Huan Liu and YUANHAO YU and Jun Chen and Xiangyu Xu},
4 booktitle={The Fourteenth International Conference on Learning Representations},
5 year={2026},
6 url={https://openreview.net/forum?id=LNqWbY5iIf}
7}
