**Title: Predicting UNSAT Cores via Polarity-Aware Representation Learning on Clause-Literal Hypergraphs

Abstract:

Graph neural networks have become a prevalent tool in Boolean satisfiability (SAT) research, primarily for extracting structural insights from SAT formulas. These methods aim to either solve SAT instances directly or bolster SAT solvers, encompassing applications like UNSAT-core prediction. Nevertheless, conventional techniques typically represent SAT formulas as bipartite or directed acyclic graphs. Such representations are less effective at capturing clause-level dynamics and higher-order interactions between literals and clauses. Furthermore, they struggle to model intrinsic polarity-related characteristics of SAT, particularly the complementary nature of positive and negative literals associated with a single variable.

To overcome these constraints, we introduce a polarity-aware representation learning framework built upon clause-literal hypergraphs. In this approach, SAT formulas are modeled as clause-literal hypergraphs, supplemented by a clause incidence graph to better capture higher-order structural interactions. We also present a polarity-aware decomposition mechanism that divides variable representations into polarity-invariant and equivariant components. This explicitly models the relationship between positive and negative literals, allowing the resulting literal representations to propagate through the hypergraph structure. Additionally, we integrate a polarity-inversion consistency regularization to strengthen polarity-consistent representations throughout the training process. Our experiments across various SAT datasets validate the efficacy of the proposed method.

Source: arXiv Generated at: 2026-06-02 00:00:00 UTC