GNN解布尔满足性时表达能力有限，难区分可满足与不可满足实例。
On the Expressive Power of GNNs for Boolean Satisfiability
- 用WL测试分析GNN在SAT中的表达能力，发现高阶WL也无法普遍区分
- 随机实例基本可区分，但工业实例需更强表达力才能预测解
- 揭示了现有GNN模型在真实场景下的理论局限性
机器学习求解布尔满足性（SAT）旨在用学习模型替代手工设计的启发式方法。图神经网络（GNN）因其能自然表示布尔公式而成为主流架构。本文从Weisfeiler-Leman（WL）测试角度分析GNN在SAT求解中的表达能力。主要结论是：全阶WL层级无法在一般情况下区分可满足与不可满足实例。高阶WL的不可区分性会转化为对顺序变量赋值的WL有界求解器的实际限制。我们进一步研究了规则、随机和平面类等重要SAT实例族所需的表达能力。为量化实际表达需求，我们在G4SAT基准的随机实例和国际SAT竞赛的工业实例上进行了实验。结果表明，尽管随机实例大多可区分，工业实例通常需要更高表达力才能预测满足赋值。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。