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.

翻译：基于机器学习求解布尔可满足性问题的方法旨在用学习模型替代手工设计的启发式策略。由于布尔公式天然的图表示特性，图神经网络已成为SAT求解的主要架构。本文通过Weisfeiler-Leman测试的视角，系统分析了GNN在SAT求解中的表达能力。我们的核心结果表明：完整的WL层次结构通常无法区分可满足与不可满足的实例。我们证明，高阶WL下的不可区分性会延续到按序赋值的WL有界求解器的实际局限中。我们进一步研究了若干重要SAT实例族（包括正则、随机和平面实例）所需的表达能力。为量化实际场景中的表达能力需求，我们在G4SAT基准测试的随机实例和国际SAT竞赛的工业实例上进行了实验。结果表明：虽然随机实例大多可区分，但工业实例通常需要更强的表达能力才能预测满足赋值。