Booleaanse Vervulbaarheid via Imitatieleren
Boolean Satisfiability via Imitation Learning
September 29, 2025
Auteurs: Zewei Zhang, Huan Liu, Yuanhao Yu, Jun Chen, Xiangyu Xu
cs.AI
Samenvatting
Wij stellen ImitSAT voor, een vertakkingsbeleid voor conflict-gestuurde clausulelerende (CDCL) oplossers, gebaseerd op imitatieleren voor het Booleaanse vervulbaarheidsprobleem (SAT). In tegenstelling tot eerdere methoden die instantieniveau-signalen voorspellen om CDCL-vertakking indirect te verbeteren, of die vertrouwen op reinforcement learning en onvoldoende CDCL-informatie om vertakking te verbeteren, leert ImitSAT van expert KeyTrace dat een volledige uitvoering samenvat in de reeks overlevende beslissingen. Het herspelen van een KeyTrace op hetzelfde instantie is bijna conflictvrij, wat dichte beslissingsniveau-supervisie biedt en propagaties direct vermindert -- de dominante factor in de werkelijke rekentijd. Deze voorvoegsel-geconditioneerde supervisie stelt ImitSAT in staat om hoogwaardige vertakkingen te reproduceren zonder exploratie, wat resulteert in snellere convergentie, stabiele training en naadloze integratie in CDCL. Uitgebreide experimenten tonen aan dat ImitSAT het aantal propagaties en de rekentijd vermindert, en daarbij state-of-the-art geleerde benaderingen overtreft. Wij hebben de broncode en het getrainde model vrijgegeven op 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