HyperSAT: Unsupervised Hypergraph Neural Networks for Weighted MaxSAT Problems.

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 nonlinear dependency and sensitive objective function, which are caused by the nonuniform distribution of weights across clauses. In this article, we present HyperSAT, a novel neural approach that employs an unsupervised hypergraph neural network (HNN) model to solve weighted MaxSAT problems. Specifically, we propose a hypergraph representation for weighted MaxSAT instances to encode higher-order relationships between literals and clauses. A cross-attention mechanism and a shared representation constraint loss function are designed to capture the logical interactions between positive and negative literal nodes in the hypergraph, which effectively address the challenges posed by the uneven weight distribution. Compared with GNN-based SAT solvers that perform message passing only along pairwise connections, the proposed HNN enables multi-literal message passing within hyperedges, providing a more expressive mechanism to capture the weighted group interactions in complex clauses. Extensive experiments on various weighted MaxSAT datasets demonstrate that HyperSAT achieves better performance than state-of-the-art learning-based approaches, with average relative improvements ranging from 1.80% to 13.37%.