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