ImitSAT: Boolean Satisfiability via Imitation Learning

Zewei Zhang    Huan Liu    Yuanhao Yu    Jun Chen    Xiangyu Xu

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.

Download the model

git lfs install
git clone https://huggingface.co/zeweizhang/ImitSAT

Files in this repo

ImitSAT.npz — trained checkpoint (NumPy/JAX arrays).
tokenizer/
    vocab.txt
    tokenizer_config.json
    special_tokens_map.json

Citation

@inproceedings{zhang2026boolean,
      title={Boolean Satisfiability via Imitation Learning},
      author={Zewei Zhang and Huan Liu and YUANHAO YU and Jun Chen and Xiangyu Xu},
      booktitle={The Fourteenth International Conference on Learning Representations},
      year={2026},
      url={https://openreview.net/forum?id=LNqWbY5iIf}
}