불린 만족 문제를 위한 모방 학습 기반 접근법

초록

우리는 불 만족 문제(SAT)를 위한 모방 학습 기반의 충돌 기반 절 학습(CDCL) 솔버 분기 정책인 ImitSAT를 제안한다. 이전 방법들이 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

불린 만족 문제를 위한 모방 학습 기반 접근법

Boolean Satisfiability via Imitation Learning

초록

Support