---
datasets:
- zeweizhang/ImitSAT-KeyTrace
language:
- en
license: apache-2.0
pipeline_tag: other
tags:
- imitation-learning
- boolean-satisfiability
- SAT
- CDCL
- branching-policy
- perceiver-ar
- autoregressive
- decision-sequence
---

<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
```bash
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
```bibtex
@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}
}
```