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

📄 arXiv: 2605.04819v1 📥 PDF

作者: Zhenchao Sun, Shuai Ma, Ping Lu, Chongyang Tao

分类: cs.LG

发布日期: 2026-05-06

备注: Accepted at ICML 2026. Camera-ready version coming soon

💡 一句话要点

提出极性感知的子句-文字超图表示学习框架，用于提升不可满足核心预测。

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)

关键词: 布尔可满足性 SAT求解 不可满足核心预测 图神经网络 超图 表示学习 极性感知 正则化

📋 核心要点

  1. 现有SAT公式建模方法难以捕捉文字和子句间高阶交互，且忽略了变量正负文字间的极性关系。
  2. 提出极性感知的子句-文字超图表示学习框架，显式建模正负文字关系，并利用超图结构传播信息。
  3. 实验结果表明，该方法在多个SAT数据集上有效，提升了不可满足核心预测的性能。

📝 摘要（中文）

本文提出了一种基于子句-文字超图的极性感知表示学习框架，用于解决布尔可满足性（SAT）任务中的不可满足核心预测问题。现有方法通常将SAT公式建模为二分图或有向无环图，难以捕捉文字和子句之间的高阶交互关系，并且在建模SAT固有的极性相关属性（例如变量的正负文字之间的互补关系）方面存在局限性。为了解决这些问题，本文利用子句-文字超图（并辅以子句关联图）来建模SAT公式，以捕捉高阶结构交互。此外，引入极性感知分解机制，将变量表示分解为极性不变和极性等变分量，显式地建模正负文字之间的关系，并将生成的文字表示沿超图结构传播。最后，结合极性反转一致性正则化，以增强训练期间极性一致的表示。在多个SAT数据集上的实验结果表明了该方法的有效性。

🔬 方法详解

问题定义：论文旨在提升布尔可满足性（SAT）问题中不可满足核心（unsat-core）的预测精度。现有方法，如基于二分图或有向无环图的建模方式，无法充分捕捉子句和文字之间的高阶交互关系，并且忽略了SAT问题中固有的极性信息，即一个变量的正负文字之间的互补关系。这些局限性导致现有方法在不可满足核心预测任务中的性能受限。

核心思路：论文的核心思路是通过构建子句-文字超图来更有效地表示SAT公式，并在此基础上进行极性感知的表示学习。超图能够捕捉子句中多个文字之间的复杂关系，而极性感知机制则能够显式地建模变量的正负文字之间的关联。通过结合这两种方法，可以学习到更具表达能力的文字和子句表示，从而提高不可满足核心预测的准确性。

技术框架：该框架主要包含以下几个步骤：1) 将SAT公式建模为子句-文字超图，并辅以子句关联图。2) 引入极性感知分解机制，将变量表示分解为极性不变和极性等变分量，分别表示变量的固有属性和极性相关属性。3) 利用超图神经网络在超图结构上传播文字和子句的表示，从而捕捉它们之间的交互关系。4) 引入极性反转一致性正则化，以增强训练期间极性一致的表示。

关键创新：该论文的关键创新在于：1) 使用子句-文字超图来建模SAT公式，从而能够捕捉高阶的结构交互。2) 提出了极性感知分解机制，显式地建模了变量的正负文字之间的关系。3) 引入了极性反转一致性正则化，以增强训练期间极性一致的表示。这些创新使得该方法能够学习到更具表达能力的文字和子句表示，从而提高了不可满足核心预测的准确性。

关键设计：极性感知分解机制将变量的表示分解为极性不变分量和极性等变分量。极性不变分量表示变量的固有属性，不受极性影响；极性等变分量则表示与极性相关的属性，例如正负文字之间的互补关系。极性反转一致性正则化通过约束正负文字的表示在极性反转操作下的一致性，来增强极性一致的表示。具体的损失函数设计和网络结构细节在论文中有详细描述，包括超图神经网络的具体形式和正则化项的计算方式。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，该方法在多个SAT数据集上显著优于现有的基线方法。具体而言，在某些数据集上，该方法可以将不可满足核心预测的准确率提高5%以上。此外，消融实验验证了极性感知分解机制和极性反转一致性正则化的有效性，证明了它们对提升模型性能的贡献。

🎯 应用场景

该研究成果可应用于提升SAT求解器的性能，尤其是在解决工业界复杂的SAT问题时，准确预测不可满足核心可以帮助快速定位问题根源，加速调试和优化过程。此外，该方法在形式验证、软件测试、硬件设计等领域也具有潜在的应用价值，能够提高相关任务的效率和可靠性。

📄 摘要（原文）

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 expressive in capturing 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 decomposed 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.