Learning to Solve Weighted Maximum Satisfiability with a Co-Training Architecture

TL;DR

This paper tackles weighted MaxSAT by introducing SplitGNN, a co-training GNN that merges supervised message passing on an edge-splitting factor graph with an unsupervised, GPU-accelerated solution boosting layer. The edge-splitting graph, guided by a spanning tree, creates four edge types to enable targeted, direction-aware information flow, while the USB layer refines solutions through relaxation-based optimization. Empirically, SplitGNN achieves faster convergence and higher quality solutions than prior GNN-based solvers on unweighted MaxSAT and, notably, outperforms modern heuristic solvers on large, hard weighted benchmarks, with strong generalization across diverse structural instances. The work demonstrates the viability of end-to-end learning for weighted MaxSAT and highlights the benefits of combining structured graph representations with hybrid optimization strategies for combinatorial problems.

Abstract

Wepropose SplitGNN, a graph neural network (GNN)-based approach that learns to solve weighted maximum satisfiabil ity (MaxSAT) problem. SplitGNN incorporates a co-training architecture consisting of supervised message passing mech anism and unsupervised solution boosting layer. A new graph representation called edge-splitting factor graph is proposed to provide more structural information for learning, which is based on spanning tree generation and edge classification. To improve the solutions on challenging and weighted instances, we implement a GPU-accelerated layer applying efficient score calculation and relaxation-based optimization. Exper iments show that SplitGNN achieves 3* faster convergence and better predictions compared with other GNN-based ar chitectures. More notably, SplitGNN successfully finds solu tions that outperform modern heuristic MaxSAT solvers on much larger and harder weighted MaxSAT benchmarks, and demonstrates exceptional generalization abilities on diverse structural instances.

Figures (4)

• Figure 1: A Factor graph to represent the WCNF formula $(x_1 \lor x_2 \lor x_3) \land (\neg{x_2} \lor x_3) \land (\neg x_1 \lor x_2) \land \neg x_3$ with 3 variables and 4 clauses, where the weights of the clauses are $100, 23, 7, 45$, respectively. This formula is unsatisfiable. When $x_1=1,x_2=0,x_3=1$, the satisfied clauses have the largest weights, which is an optimal solution of this problem.
• Figure 2: A round of message passing in SplitGNN. The embeddings are propagated through four different aggregation functions represented by four types of edges: cyan for parent edges, green for child edges, red for non-tree up edges, and gold for non-tree down edges. Left: The embeddings of clauses are updated by the embeddings of literals. Right: The embeddings of literals are updated by the embeddings of clauses.
• Figure 3: The architecture of SplitGNN. The embeddings of literals are first updated through message passing for $T$ layers. Next, the prediction of variables is fed into an unsupervised solution boosting (USB) layer, where GPU-accelerated score calculation and relaxation-based optimization techniques are employed to generate better solutions. The better solution found can update the slack variable values and the parameters of the message passing to achieve transfer learning.
• Figure 4: Comparison of the average number of unsatisfied clauses achieved by SplitGNN and GMS-N under different training epochs.

Theorems & Definitions (1)

• Definition 1: Edge-splitting factor graph