用模仿学习提升SAT求解器分支策略，更快找到解。
Boolean Satisfiability via Imitation Learning
- 从专家决策序列中学习分支策略，直接优化每步选择
- 减少传播次数和运行时间，显著优于现有学习方法
- 适合需要高效求解SAT问题的研究者与工业用户
我们提出ImitSAT，一种基于模仿学习的布尔可满足性问题（SAT）求解器分支策略，用于冲突驱动子句学习（CDCL）框架。不同于以往通过预测实例级信号间接改进分支，或依赖强化学习与不充分的CDCL信息，ImitSAT从专家生成的KeyTrace中学习，该记录将完整求解过程压缩为存活决策序列。在相同实例上重放KeyTrace几乎无冲突，提供密集的决策级监督，并直接减少传播次数——这是耗时的主要来源。这种前缀条件监督使ImitSAT无需探索即可复现高质量分支，实现更快收敛、稳定训练，并无缝集成至现有CDCL求解器。大量实验表明，ImitSAT有效降低传播次数与运行时间，超越当前最优学习方法。代码与模型已开源：https://github.com/zewei-Zhang/ImitSAT。
原文摘要 · Abstract (English)
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
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。