Satisfatibilidade Booleana via Aprendizado por Imitação

Boolean Satisfiability via Imitation Learning

September 29, 2025

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

cs.AI

Resumo

Propomos o ImitSAT, uma política de ramificação para solucionadores de aprendizado de cláusulas baseado em conflitos (CDCL) que utiliza aprendizado por imitação para o problema de satisfatibilidade booleana (SAT). Diferentemente de métodos anteriores que preveem sinais em nível de instância para melhorar indiretamente a ramificação do CDCL, ou que dependem de aprendizado por reforço e informações insuficientes do CDCL para aprimorar a ramificação, o ImitSAT aprende a partir de KeyTrace especializado, que condensa uma execução completa na sequência de decisões sobreviventes. A reprodução de um KeyTrace na mesma instância é praticamente livre de conflitos, fornecendo supervisão densa em nível de decisão e reduzindo diretamente as propagações — o principal contribuinte para o tempo de execução. Essa supervisão condicionada ao prefixo permite que o ImitSAT reproduza ramificações de alta qualidade sem exploração, resultando em convergência mais rápida, treinamento estável e integração perfeita ao CDCL. Experimentos extensivos demonstram que o ImitSAT reduz as contagens de propagação e o tempo de execução, superando abordagens aprendidas de ponta. Disponibilizamos o código-fonte e o modelo treinado em 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