불리언 만족가능성 문제 해결을 위한 그래프 신경망(GNN)의 표현 능력에 대한 연구

On the Expressive Power of GNNs for Boolean Satisfiability

불리언 만족가능성(SAT) 문제를 해결하기 위한 머신러닝 접근 방식은 수작업으로 설계된 휴리스틱을 학습 기반 모델로 대체하는 것을 목표로 합니다. 그래프 신경망(GNN)은 불리언 공식을 자연스러운 그래프 형태로 표현할 수 있기 때문에 SAT 문제 해결을 위한 주요 아키텍처로 부상했습니다. 본 연구에서는 Weisfeiler-Leman (WL) 테스트를 통해 SAT 문제 해결을 위한 GNN의 표현 능력을 분석합니다. 주요 결과로, 전체 WL 계층 구조는 일반적으로 만족 가능한 인스턴스와 불만족 가능한 인스턴스를 구별할 수 없음을 증명합니다. 고차 WL 하에서의 구별 불가능성이 순차적으로 변수를 설정하는 WL 기반 솔버의 실제적인 한계로 이어진다는 것을 보여줍니다. 또한, 정규, 랜덤 및 평면 인스턴스 등 중요한 SAT 인스턴스 패밀리에 필요한 표현 능력을 연구합니다. 실제적인 표현 능력 요구 사항을 정량화하기 위해, G4SAT 벤치마크에서 추출한 랜덤 인스턴스와 국제 SAT 대회에서 얻은 산업용 인스턴스에 대한 실험을 수행했습니다. 연구 결과는 랜덤 인스턴스가 대부분 구별 가능하지만, 산업용 인스턴스는 만족 가능한 할당을 예측하기 위해 더 높은 수준의 표현 능력이 필요하다는 것을 시사합니다.

Machine learning approaches to solving Boolean Satisfiability (SAT) aim to replace handcrafted heuristics with learning-based models. Graph Neural Networks have emerged as the main architecture for SAT solving, due to the natural graph representation of Boolean formulas. We analyze the expressive power of GNNs for SAT solving through the lens of the Weisfeiler-Leman (WL) test. As our main result, we prove that the full WL hierarchy cannot, in general, distinguish between satisfiable and unsatisfiable instances. We show that indistinguishability under higher-order WL carries over to practical limitations for WL-bounded solvers that set variables sequentially. We further study the expressivity required for several important families of SAT instances, including regular, random and planar instances. To quantify expressivity needs in practice, we conduct experiments on random instances from the G4SAT benchmark and industrial instances from the International SAT Competition. Our results suggest that while random instances are largely distinguishable, industrial instances often require more expressivity to predict a satisfying assignment.