HyperSAT: Unsupervised Hypergraph Neural Networks for Weighted MaxSAT Problems

TL;DR

HyperSAT addresses Weighted MaxSAT by modeling each literal as a distinct node and each clause as a weighted hyperedge, solved through an unsupervised HyperGCN-based pipeline with a cross-attention transformer. The method optimizes a joint objective $\mathcal{L}_{total} = \mathcal{L}_{task} + \lambda \mathcal{L}_{shared}$, where $\mathcal{L}_{task}$ aggregates clause weights via $V_j(\bm{Y}) = 1 - \prod_{i \in C_j^+} (1 - y_i) \prod_{i \in C_j^-} y_i$, and $\mathcal{L}_{shared}$ enforces distinct positive/negative literal representations. Empirical results on random Weighted MaxSAT instances show HyperSAT substantially reduces the average weight of unsatisfied clauses compared with baselines, demonstrating strong handling of high-order dependencies and weight heterogeneity. The work highlights the potential of unsupervised hypergraph neural nets for complex combinatorial optimization and suggests future integration with heuristic solvers and extensions to broader problem classes.

Abstract

Graph neural networks (GNNs) have shown promising performance in solving both Boolean satisfiability (SAT) and Maximum Satisfiability (MaxSAT) problems due to their ability to efficiently model and capture the structural dependencies between literals and clauses. However, GNN methods for solving Weighted MaxSAT problems remain underdeveloped. The challenges arise from the non-linear dependency and sensitive objective function, which are caused by the non-uniform distribution of weights across clauses. In this paper, we present HyperSAT, a novel neural approach that employs an unsupervised hypergraph neural network model to solve Weighted MaxSAT problems. We propose a hypergraph representation for Weighted MaxSAT instances and design a cross-attention mechanism along with a shared representation constraint loss function to capture the logical interactions between positive and negative literal nodes in the hypergraph. Extensive experiments on various Weighted MaxSAT datasets demonstrate that HyperSAT achieves better performance than state-of-the-art competitors.

Figures (3)

• Figure 1: An overview of HyperSAT framework.
• Figure 2: Hypergraph Modeling of a Weighted MaxSAT instance $(\neg x_1 \vee x_2 \vee \neg x_3) \wedge (x_1 \vee x_2) \wedge (\neg x_2 \vee x_3 \vee x_4) \wedge (\neg x_1 \vee x_3 \vee \neg x_4)$ with 8 literals, 4 clauses and weights $\{w_1,w_2,w_3,w_4\}$.
• Figure 3: The evolution of loss for HyperSAT and HypOp during an inference process of 300 epochs on the uuf250-1065 dataset.