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

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.

The Boolean satisfiability problem (SAT) is about determining whether a set of logical constraints can all be true at the same time. Many computing tasks, including planning, verification, and security, can be expressed in this form. However, hard SAT formulas remain challenging, and modern solvers still rely heavily on carefully designed decision rules. Our work focuses on unsat core prediction, which aims to identify variables involved in the conflicting part of an unsatisfiable formula. We develop PASAT, a machine learning model that pays special attention to the positive and negative forms of each Boolean variable. These two forms should share some information while still reflecting their opposite signs. PASAT learns this relationship while representing each clause as a group of related logical terms in a hypergraph. By also training on formulas with swapped signs, PASAT learns more consistent representations for predicting unsat core variables. Across several SAT datasets, PASAT predicted unsat core variables more accurately than existing learning-based methods. When used to guide classical SAT solvers, its predictions helped them solve more benchmark problems.