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

arXiv: https://arxiv.org/abs/2605.04819 · HTML: https://mlsanity.com/paper/2605.04819/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 15 of its 32 references that are in the map.
- First posted on arXiv 6 May 2026.

## Builds on (most cited first, 15 of 15)

- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Inductive Representation Learning on Large Graphs](https://mlsanity.com/paper/1706.02216/) (2017)
- [Hypergraph Convolution and Hypergraph Attention](https://mlsanity.com/paper/1901.08150/) (2019)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [NLocalSAT: Boosting Local Search with Solution Prediction](https://mlsanity.com/paper/2001.09398/) (2020)
- [NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks](https://mlsanity.com/paper/2110.14053/) (2021)
- [NSNet: A General Neural Probabilistic Framework for Satisfiability Problems](https://mlsanity.com/paper/2211.03880/) (2022)
- [G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks](https://mlsanity.com/paper/2309.16941/) (2023)
- [SATformer: Transformer-Based UNSAT Core Learning](https://mlsanity.com/paper/2209.00953/) (2022)
- [DeepSAT: An EDA-Driven Learning Framework for SAT](https://mlsanity.com/paper/2205.13745/) (2022)
- [Graph Neural Networks and Boolean Satisfiability](https://mlsanity.com/paper/1702.03592/) (2017)
- [GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection](https://mlsanity.com/paper/2405.11024/) (2024)
- [Learning from Algorithm Feedback: One-Shot SAT Solver Guidance with GNNs](https://mlsanity.com/paper/2505.16053/) (2025)
- [HyperSAT: Unsupervised Hypergraph Neural Networks for Weighted MaxSAT Problems](https://mlsanity.com/paper/2504.11885/) (2025)

## Abstract (arXiv)

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.