Boolean Satisfiability via Imitation Learning
We propose ImitSAT, 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 to
improve CDCL branching indirectly, or rely on reinforcement learning and
insufficient CDCL information to enhance branching, ImitSAT learns from expert
KeyTrace that collapses a full run into the sequence of surviving decisions.
Replaying a KeyTrace on the same instance is nearly conflict-free, providing
dense decision-level supervision and directly reducing propagations -- the
dominant contributor to wall-clock time. This prefix-conditioned supervision
enables ImitSAT to reproduce high-quality branches without exploration,
yielding faster convergence, stable training, and seamless integration into
CDCL. Extensive experiments demonstrate that ImitSAT reduces propagation counts
and runtime, outperforming state-of-the-art learned approaches. We released the
source code and trained model at https://github.com/zewei-Zhang/ImitSAT
68dded9d6024653e8a3ed0e2
Zewei Zhang
claimed_verified
2025-10-02T13:55:13.434Z
63e03e8942591dda0b9a0dec
/avatars/fbf54bc5a8aadc7399d1a1be9b9d6b65.svg
Zewei Zhang
user
zeweizhang
68dded9d6024653e8a3ed0e3
Huan Liu
68dded9d6024653e8a3ed0e4
Yuanhao Yu
68dded9d6024653e8a3ed0e5
Jun Chen
68dded9d6024653e8a3ed0e6
Xiangyu Xu
Boolean Satisfiability via Imitation Learning
We propose ImitSAT, 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 to
improve CDCL branching indirectly, or rely on reinforcement learning and
insufficient CDCL information to enhance branching, ImitSAT learns from expert
KeyTrace that collapses a full run into the sequence of surviving decisions.
Replaying a KeyTrace on the same instance is nearly conflict-free, providing
dense decision-level supervision and directly reducing propagations -- the
dominant contributor to wall-clock time. This prefix-conditioned supervision
enables ImitSAT to reproduce high-quality branches without exploration,
yielding faster convergence, stable training, and seamless integration into
CDCL. Extensive experiments demonstrate that ImitSAT reduces propagation counts
and runtime, outperforming state-of-the-art learned approaches. We released the
source code and trained model at https://github.com/zewei-Zhang/ImitSAT
ImitSAT, a branching policy for CDCL solvers using imitation learning from expert traces, reduces propagation counts and runtime by providing dense decision-level supervision.
ImitSAT conflict-driven clause learning CDCL Boolean satisfiability problem SAT imitation learning KeyTrace decision-level supervision propagations wall-clock time prefix-conditioned supervision learned approaches