SAT 해결기의 초기 분기 순서 학습

Learning to Rank the Initial Branching Order of SAT Solvers

SAT 문제를 효율적으로 해결하는 데 있어 좋은 분기 순서를 찾는 것은 매우 중요하지만, 그러한 분기 순서를 찾는 것은 어려운 문제입니다. 따라서, 문제를 해결하기 전에 좋은 분기 순서를 예측하는 학습 기반 접근 방식은 잠재력을 가지고 있습니다. 본 논문에서는 그래프 신경망을 사용하여 충돌 기반 절 학습(CDCL) SAT 해결기의 전처리 단계로 분기 순서를 예측하는 것을 연구합니다. 좋은 초기 분기 순서를 제공함으로써 기존의 CDCL SAT 해결기에 상당한 성능 향상을 가져올 수 있음을 보여줍니다. 또한, 이러한 초기 분기 순서를 효율적으로 찾기 위한 세 가지 라벨링 방법을 제시합니다. 마지막으로, 그래프 신경망을 훈련하여 이러한 분기 순서를 예측하고, 실험 결과 GNN으로 초기화된 분기 순서가 무작위 3-CNF 및 준산업용 벤치마크에서 상당한 속도 향상을 가져옴을 확인했습니다. 또한, GNN은 학습 데이터보다 훨씬 큰 규모의 인스턴스에 대한 일반화 능력을 보여주었습니다. 그러나, 더 어렵고 산업용 인스턴스에서는 예측이 속도 향상을 가져오지 못하는 경우가 있음을 발견했습니다. 이는 솔버의 동적 휴리스틱이 제공된 초기 분기 순서를 빠르게 덮어쓰기 때문이며, 또한 이러한 인스턴스의 복잡성으로 인해 GNN 예측이 어렵기 때문이라고 판단됩니다.

Finding good branching orders is key to solving SAT problems efficiently, but finding such branching orders is a difficult problem. Using a learning based approach to predict a good branching order before solving, therefore, has potential. In this paper, we investigate predicting branching orders using graph neural networks as a preprocessing step to conflict-driven clause learning (CDCL) SAT solvers. We show that there are significant gains to be made in existing CDCL SAT solvers by providing a good initial branching. Further, we provide three labeling methods to find such initial branching orders in a tractable way. Finally, we train a graph neural network to predict these branching orders and show through our evaluations that a GNN-initialized ordering yields significant speedups on random 3-CNF and pseudo-industrial benchmarks, with generalization capabilities to instances much larger than the training set. However, we also find that the predictions fail at speeding up more difficult and industrial instances. We attribute this to the solver's dynamic heuristics, which rapidly overwrite the provided initialization, and to the complexity of these instances, making GNN prediction hard.