Булева выполнимость через обучение с подражанием
Boolean Satisfiability via Imitation Learning
September 29, 2025
Авторы: Zewei Zhang, Huan Liu, Yuanhao Yu, Jun Chen, Xiangyu Xu
cs.AI
Аннотация
Мы представляем ImitSAT — стратегию ветвления для решателей, основанных на конфликтно-управляемом обучении дизъюнктов (CDCL), которая использует обучение с подражанием для задачи выполнимости булевых формул (SAT). В отличие от предыдущих методов, которые предсказывают сигналы на уровне экземпляров для косвенного улучшения ветвления в CDCL, или полагаются на обучение с подкреплением и недостаточную информацию о CDCL для улучшения ветвления, ImitSAT обучается на экспертных KeyTrace, которые сводят полный прогон к последовательности сохранившихся решений. Повторение KeyTrace на том же экземпляре практически не вызывает конфликтов, обеспечивая плотный надзор на уровне решений и напрямую сокращая количество распространений — основной фактор, влияющий на время выполнения. Этот надзор, обусловленный префиксом, позволяет ImitSAT воспроизводить высококачественные ветвления без необходимости исследования, что приводит к более быстрой сходимости, стабильному обучению и бесшовной интеграции в CDCL. Многочисленные эксперименты показывают, что ImitSAT сокращает количество распространений и время выполнения, превосходя современные подходы, основанные на обучении. Мы опубликовали исходный код и обученную модель на 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