Satisfiabilité booléenne par apprentissage par imitation

Boolean Satisfiability via Imitation Learning

September 29, 2025

papers.authors: Zewei Zhang, Huan Liu, Yuanhao Yu, Jun Chen, Xiangyu Xu

cs.AI

papers.abstract

Nous proposons ImitSAT, une politique de branchement pour les solveurs CDCL (Conflict-Driven Clause Learning) basée sur l'apprentissage par imitation pour le problème de satisfiabilité booléenne (SAT). Contrairement aux méthodes précédentes qui prédisent des signaux au niveau de l'instance pour améliorer indirectement le branchement CDCL, ou qui s'appuient sur l'apprentissage par renforcement et des informations CDCL insuffisantes pour optimiser le branchement, ImitSAT apprend à partir de KeyTrace, une trace experte qui résume une exécution complète en une séquence de décisions survivantes. La relecture d'une KeyTrace sur la même instance est quasiment exempte de conflits, fournissant une supervision dense au niveau des décisions et réduisant directement les propagations -- le principal contributeur au temps d'exécution. Cette supervision conditionnée par le préfixe permet à ImitSAT de reproduire des branches de haute qualité sans exploration, conduisant à une convergence plus rapide, un entraînement stable et une intégration transparente dans CDCL. Des expériences approfondies démontrent qu'ImitSAT réduit le nombre de propagations et le temps d'exécution, surpassant les approches apprises de pointe. Nous avons publié le code source et le modèle entraîné à l'adresse suivante : 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