arXiv:2605.04819cs.LG2026-05中稿 · ICML

用超图建模布尔可满足性问题,显式捕捉正负文字关系。

Unsat Core Prediction through Polarity-Aware Representation Learning over Clause-Literal Hypergraphs

  • 构建含极性感知的子句-文字超图,捕捉高阶结构交互
  • 通过极性分解与一致性正则化,提升文字表示质量
  • 在多个数据集上显著优于现有方法,适合SAT求解优化

图神经网络已广泛应用于布尔可满足性(SAT)任务中,以从SAT公式中学习结构信息。现有方法通常将SAT公式建模为二分图或有向无环图,难以直接捕捉子句级及文字间的高阶相互作用,且对变量极性等内在特性建模不足,例如变量正负文字间的互补关系。为此,本文提出一种基于子句-文字超图的极性感知表示学习框架。通过引入子句关联图,构建包含高阶结构交互的超图模型;设计极性感知分解机制,将变量表示分为不变与等变成分,显式建模正负文字间的关系,并将文字表示沿超图结构传播;进一步引入极性反转一致性正则化,在训练中强化极性一致的表示。在多个SAT数据集上的实验结果表明,该方法有效提升了未满足核心预测性能。

原文摘要 · Abstract (English)

Graph neural networks have been widely used in Boolean satisfiability (SAT) tasks to learn structural information from SAT formulas. The goal of these studies is to solve SAT instances or to enhance SAT solvers, including tasks such as unsat-core prediction. However, most existing approaches model a SAT formula as a bipartite graph or a directed acyclic graph, which are less direct in capturing clause-level and higher-order interactions among literals and clauses. Moreover, these approaches are limited in modeling intrinsic polarity-related properties of SAT, such as the complementary relationship between the positive and negative literals of a variable. To address these limitations, we propose a polarity-aware representation learning framework over clause-literal hypergraphs. We model SAT formulas as clause-literal hypergraphs augmented with a clause incidence graph to capture higher-order structural interactions. We then introduce a polarity-aware decomposition mechanism that separates variable representations into polarity invariant and equivariant components, explicitly modeling the relationship between positive and negative literals, with the resulting literal representations propagated along the hypergraph structure. We further incorporate a polarity-inversion consistency regularization to reinforce polarity-consistent representations during training. Experimental results on multiple SAT datasets demonstrate the effectiveness of the proposed approach.

SAT求解超图神经网络极性感知

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。