模倣学習によるブール充足可能性問題

要旨

我々は、ブール充足可能性問題（SAT）に対する模倣学習に基づく、コンフリクト駆動節学習（CDCL）ソルバーのための分岐ポリシーであるImitSATを提案する。従来の手法が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