Soddisfacibilità Booleana tramite Apprendimento per Imitazione
Boolean Satisfiability via Imitation Learning
September 29, 2025
Autori: Zewei Zhang, Huan Liu, Yuanhao Yu, Jun Chen, Xiangyu Xu
cs.AI
Abstract
Proponiamo ImitSAT, una politica di branching per risolutori CDCL (Conflict-Driven Clause Learning) basata sull'apprendimento per imitazione per il problema della soddisfacibilità booleana (SAT). A differenza dei metodi precedenti che prevedono segnali a livello di istanza per migliorare indirettamente il branching CDCL, o che si affidano al reinforcement learning e a informazioni CDCL insufficienti per potenziare il branching, ImitSAT apprende da KeyTrace, un esperto che riduce un'intera esecuzione alla sequenza di decisioni sopravvissute. Riprodurre un KeyTrace sulla stessa istanza è quasi privo di conflitti, fornendo una supervisione densa a livello decisionale e riducendo direttamente le propagazioni – il principale contributore del tempo di esecuzione. Questa supervisione condizionata al prefisso consente a ImitSAT di riprodurre rami di alta qualità senza esplorazione, garantendo una convergenza più rapida, un addestramento stabile e un'integrazione senza soluzione di continuità nel CDCL. Esperimenti estensivi dimostrano che ImitSAT riduce il numero di propagazioni e il tempo di esecuzione, superando gli approcci basati sull'apprendimento più avanzati. Abbiamo rilasciato il codice sorgente e il modello addestrato su 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