布尔可满足性问题通过模仿学习求解

摘要

我们提出了ImitSAT，一种基于模仿学习的布尔可满足性问题（SAT）冲突驱动子句学习（CDCL）求解器的分支策略。与以往通过预测实例级信号间接改进CDCL分支的方法不同，或依赖强化学习和不充分的CDCL信息来增强分支，ImitSAT从专家KeyTrace中学习，后者将完整运行过程压缩为一系列存续决策序列。在同一实例上重放KeyTrace几乎无冲突，提供了密集的决策级监督，并直接减少了传播——这是实际运行时间的主要贡献者。这种前缀条件监督使ImitSAT无需探索即可重现高质量分支，实现了更快的收敛、稳定的训练以及与CDCL的无缝集成。大量实验表明，ImitSAT减少了传播次数和运行时间，超越了最先进的学习方法。我们在https://github.com/zewei-Zhang/ImitSAT上公开了源代码和训练模型。

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

布尔可满足性问题通过模仿学习求解

Boolean Satisfiability via Imitation Learning

摘要

Support