ImitSAT

<p align="center"> <h1 align="center"><em>ImitSAT</em>: Boolean Satisfiability via Imitation Learning</h1> <!-- <br /> --> <div align="center"> <strong>Zewei Zhang</strong> &nbsp;&nbsp; <strong>Huan Liu</strong> &nbsp;&nbsp; <strong>Yuanhao Yu</strong> &nbsp;&nbsp; <a href="https://www.ece.mcmaster.ca/~junchen/"><strong>Jun Chen</strong></a> &nbsp;&nbsp; <a href="https://xuxy09.github.io/"><strong>Xiangyu Xu</strong></a> </div> <div align="center"> <br> <a href="https://arxiv.org/abs/2509.25411"><img src="https://img.shields.io/badge/arXiv-Preprint-brightgreen.svg" alt="arXiv Preprint"></a> <a href="https://colab.research.google.com/drive/1NuLn_Umt57TLEGueQj-ff8-yaM8BQiCy?usp=sharing"><img src="https://colab.research.google.com/assets/colab-badge.svg" alt="google colab logo"></a> <a href="https://github.com/zewei-Zhang/ImitSAT"> <img src="https://img.shields.io/badge/GitHub-Repo-black?logo=github" alt="GitHub repository"> </a> </div> <p align="center"> <em>More details, training/evaluation scripts, and ablations can be found in the <a href="https://github.com/zewei-Zhang/ImitSAT">GitHub repository</a> and the <a href="https://arxiv.org/abs/2509.25411">paper</a>.</em> </p>

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}
}