Boolesche Erfüllbarkeit durch Imitationslernen
Boolean Satisfiability via Imitation Learning
September 29, 2025
papers.authors: Zewei Zhang, Huan Liu, Yuanhao Yu, Jun Chen, Xiangyu Xu
cs.AI
papers.abstract
Wir stellen ImitSAT vor, eine Verzweigungsstrategie für konfliktgetriebene Klausellernverfahren (CDCL), die auf Imitationslernen für das Problem der Booleschen Erfüllbarkeit (SAT) basiert. Im Gegensatz zu früheren Methoden, die Instanz-spezifische Signale vorhersagen, um die CDCL-Verzweigung indirekt zu verbessern, oder sich auf Verstärkungslernen und unzureichende CDCL-Informationen stützen, um die Verzweigung zu optimieren, lernt ImitSAT von einem Experten-KeyTrace, der einen vollständigen Durchlauf in die Sequenz der überlebenden Entscheidungen komprimiert. Das Abspielen eines KeyTrace auf derselben Instanz ist nahezu konfliktfrei und bietet eine dichte Entscheidungsüberwachung auf Ebene der Entscheidungen, wodurch direkt die Propagationen reduziert werden – der dominante Faktor für die Echtzeit. Diese präfix-bedingte Überwachung ermöglicht es ImitSAT, hochwertige Verzweigungen ohne Exploration zu reproduzieren, was zu schnellerer Konvergenz, stabilerem Training und nahtloser Integration in CDCL führt. Umfangreiche Experimente zeigen, dass ImitSAT die Anzahl der Propagationen und die Laufzeit reduziert und dabei state-of-the-art gelernte Ansätze übertrifft. Wir haben den Quellcode und das trainierte Modell unter https://github.com/zewei-Zhang/ImitSAT veröffentlicht.
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