Satisfacibilidad Booleana mediante Aprendizaje por Imitación

Boolean Satisfiability via Imitation Learning

September 29, 2025

Autores: Zewei Zhang, Huan Liu, Yuanhao Yu, Jun Chen, Xiangyu Xu

cs.AI

Resumen

Proponemos ImitSAT, una política de ramificación para solucionadores de aprendizaje de cláusulas basado en conflictos (CDCL) que utiliza aprendizaje por imitación para el problema de satisfacibilidad booleana (SAT). A diferencia de métodos anteriores que predicen señales a nivel de instancia para mejorar indirectamente la ramificación en CDCL, o que dependen de aprendizaje por refuerzo e información insuficiente de CDCL para optimizar la ramificación, ImitSAT aprende de KeyTrace, un experto que condensa una ejecución completa en la secuencia de decisiones sobrevivientes. Al reproducir un KeyTrace en la misma instancia, se logra un proceso casi libre de conflictos, proporcionando supervisión densa a nivel de decisión y reduciendo directamente las propagaciones —el principal contribuyente al tiempo de ejecución—. Esta supervisión condicionada por prefijos permite a ImitSAT reproducir ramificaciones de alta calidad sin necesidad de exploración, logrando una convergencia más rápida, un entrenamiento estable y una integración fluida en CDCL. Experimentos exhaustivos demuestran que ImitSAT reduce el número de propagaciones y el tiempo de ejecución, superando a los enfoques aprendidos más avanzados. Hemos publicado el código fuente y el modelo entrenado en 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