Graph-Based Attention for Differentiable MaxSAT Solving
Authors: Sota Moriyama
Katsumi Inoue
Venue: NeurIPS 2025 spotlight ()
Keywords: Maximum Satisfiability
Weighted Maximum Satisfiability
Graph Neural Network
Graph Attention
T-Norm
Neurosymbolic
Primary area: optimization
TL;DR: We introduce SAT-based Graph Attention Networks (SGATs), a t-norm–based GNN architecture for differentiable (weighted) MaxSAT solving, and demonstrate that SGATs outperform existing state-of-the-art continuous approaches on standard benchmarks.

Abstract: The use of deep learning to solve fundamental AI problems such as Boolean Satisfiability (SAT) has been explored recently to develop robust and scalable reasoning systems. This work advances such neural-based reasoning approaches by developing a new Graph Neural Network (GNN) to differentiably solve (weighted) Maximum Satisfiability (MaxSAT). To this end, we propose SAT-based Graph Attention Networks (SGATs) as novel GNNs that are built on t-norm based attention and message passing mechanisms, and structurally designed to approximate greedy distributed local search. To demonstrate the effectiveness of our model, we develop a local search solver that uses SGATs to continuously solve any given MaxSAT problem. Experiments on (weighted) MaxSAT benchmark datasets demonstrate that SGATs significantly outperform existing neural-based architectures, and achieve state-of-the-art performance among continuous approaches, highlighting the strength of the proposed model.

Graph-Based Attention for Differentiable MaxSAT Solving
Sota Moriyama 1.
Katsumi Inoue²
The Graduate University for Advanced Studies, SOKENDAI National Institute of Informatics {sotam, inoue inoue)@nii @@nii aaciiiac.... .j.
Abstract
The use of deep learning solve fundamental AI problems such as Boolean Satisfiability (SAT) has been explored recently to develop robust and scalable reasoning systems. This work advances such neural- reasoning approaches by developing new Graph Neural Network (GNN) to differentiably solve (weighted) Maximum Satisfiability (MaxSAT). To this end, we propose SAT-based Graph Attention Networks (SGATs) as novel GNNs that are built on t-norm based at- tention and message passing mechanisms, and structurally designed to approx- imate greedy distributed local search. To demonstrate the effectiveness of our model, we develop local search solver that uses SGATs to continuously solve any given MaxSAT problem. Experiments (weighted) MaxSAT benchmark datasets demonstrate that SGATs significantly outperform existing neural-based architec- tures, and achieve sfateoof-the-ar performance among continuous approaches, highlighting the strength of the proposed model
Introduction
Neuro-symbolic AI aims to develop robust and scalable reasoning systems by combining the strengths
of both symbolic logic and neural networks (20) 6]. Boolean Satisfiability (SAT), fundamental
reasoning problem in Al and Computer Science, has long been examined as important topic in
neuro-symbolic research. There have been many studies on developing SAT solving methods using
deep learning. which can either solve SAT problems in end-to-end manner [22 11, or can be
combined with existing discrete solvers to enhance their performance [I].
Maximum Satisfiability (MaxSAT), an optimization generalization of SAT, has been viewed as promising approach towards accomplishing various neuro-symbolic tasks (9 (28) SATNet one representative approach, capable of learning to solve structured reasoning tasks such as visual sudoku by employing differentiable MaxSAT solving layer (27). This layer is built upon continuous optimization algorithm, specifically based on the use of Semidefinite Programming (SDP) (26). While this algorithm has proved effective on certain problem types, other promising approaches have also been proposed, such as the use of Fourier analysis [12 and Graph Neural Networks [17 The latter, however, remains largely underexplored.
Graph Neural Networks (GNNs) have been widely used in relational and symbolic domains, as well in multiple neuro-symbolic systems [3] There has recently been surge of interest in using GNNs as a key building block for combinatorial optimization problems [3] In particular, several works have applied GNNs MaxSAT solving, either in an end-to-end manner 17]. or by using their predictions as heuristics for existing solvers
[16]. In contrast, we propose GNN architectures capable
All used code is contained in the repository:
39th Conference on Neural Information Processing Systems (NeurIPS 2025).

---

of differentiably solving weighted MaxSAT problems, and are effective against practical problem instances.
In this paper, we present SAT-based Graph Attention Networks (SGATs) as novel GNNs crafted for solving MTxSAT, which are the first GNNs to be able to handle weighted MaxSAT problems. SGATs are composed of GNN layers with novel t-norm based attention, where attention mechanisms operate on values computed using t-norms. When clause is unsatisfied by a candidate assignment, the clause node sends messages to all its connected variable nodes, requesting them to update their values in parallel towards satisfying the clause. The attention mechanism then computes priorities to decide which variable nodes should change their values to maximally satisfy those requests from clauses, allowing the model to learn which clauses focus on. Intuitively, this can be regarded learning a general heuristic that can be applied to variety of MaxSAT problems. To show the effectiveness of SGATs, we further build local search algorithm that finds solutions with the continuous optimization of GNNs through iterative training, which can be used with any GNN architecture as the backbone.
To evaluate the effectiveness of our model, we first compare the performance against existing neural- based architectures using benchmark instances from the MaxSAT Evaluations in 2018. We then conduct ablation studies analyze the effectiveness of each component of SGATs, including the t-norm based attention and message passing mechanisms. Subsequently, we use benchmark instances used in MaxSAT evaluations from 2020 2024, and compare the qualities of the predictions with solvers based on state-of- of-the-art (SOTA) continuous approaches. The experimental results show that SGATs demonstrate excellent stability and performance compared existing neural architectures and mechanisms during training, and is able to achieve the SOTA performance for continuous solvers on all benchmark sets. We discuss the limitations and broader impacts of our work in Appendix and Appendix G respectively.
Our key contributions are as follows:
We present SAT-based Graph Attention Networks (SGATs) as the first GNN architecture specifically designed for MaxSAT solving, and able to handle weighted MaxSAT prob- lems.
We introduce novel t-norm based attention and message passing mechanisms that are specifically designed to approximate greedy distributed local search.
We demonstrate that SGAT's outperform existing neural architectures, and achieve SOTA performance for continuous solvers on all benchmark sets.
2 Related Work
2.1 Differentiable Solvers
In SAT, there have been multiple works attempting to construct differentiable solvers, with deep learning being the main method accomplish this. Particularly, most works have focused on using
GNNs [I] as well as Recurrent Neural Networks (RNNs) [22]. Others have attempted to use
these models as heuristics for state-of-the-arr (SOTA) solvers, in an effort to further bridge the gap
between the two fields (21 31, with reinforcement learning being one prominent approach [8] [1].
To support further research in this domain, [55] has built codebase that deploys wide range of neural architectures, as well as benchmarks known to date. Constraint Satisfaction Problems (CSPs) are another related field, with works focusing on learning search heuristics or end-to-end solvers via
neural architectures, with the use of GNNs and transformer variants 23 29].
In the context of MaxSAT solving, not many differentiablee solvers have been proposed to this day, and works that do mainly focus on solving synthesized problems with the use of GNNs [17]. However, there are no works that utilize Graph Attention Networks (GATs), which had been shown to be effective for related problems such as SAT, CSP, and Minimal Unsatisfiable Subset extraction 4 29 [8] In contrast, our work focuses on developing a much more robust GNN architecture that employs attention and message passing mechanisms that utilize t-norm computation, direction not explored in prior works to the best of our knowledge.
2

---

2.2 Continuous Optimization Based MaxSAT Solvers
Several approaches have been proposed for MaxSAT solving with the use of continuous optimization. The Mixing method (26) is one such approach, specifically using low-rank coordinate descent for Semidefinite Programming (SDP). Together with multiple techniques such as franch-and-bounde has achieved SOTA performance in solving Max2SAT problems, a special case of MaxSAT problems where each clause has strictly literals 255. FourierSAT is another continuous optimization based approach, utilizing the Fourier analysis of Boolean functions to handle various types of Boolean constraints [2]. Although this is the only line of work to address weighted MaxSAT, their current implementation does not fully support this, indicating the practical difficulties of handling them.
3 Background
3.1 SAT, MaxSAT and Weighted MaxSAT
In Boolean Satisfiability (SAT), a propositional logic formula consisting of variables, negations (-), conjunctions (A), and disjunctions (V) is encoded into Conjunctive Normal Form (CNF). A CNF formula is composed by conjunctions of multiple sub-formulas called clauses, with each clause being composed by disjunctions of variables or their negations, called literals. Each variable can be assigned a logical value of false (0) or true (1), and the formula is satisfied if and only if there exists an assignment where at least one literal in each clause is mapped to true (each clause satisfied).
In Maximum Satisfiability (MaxSAT), the objective is to find the assignment of variables that maximizes the number of satisfied clauses in the formula. In weighted MaxSAT, the objective shifts to finding the assignment that maximizes the total weight of satisfied clauses. In the following sections, we will use n and m to denote the number of variables and clauses in a problem, and wy to denote the weight of clause C, Furthermore, we refer to cost as the total sum of weights of unsatisfied clauses.
In MaxSAT, there two major categories of algorithms: complete and incomplete. Complete algorithms guarantee that given solutions are optimal, while incomplete algorithms aim to find good-quality assignments within reasonable time frame. In our work, we focus on the latter, mainly as guaranteeing optimalities of solutions are difficult with continuous approaches. The current SOTA incomplete solvers are based Stochastic Local Search, with multiple of them being proposed in recent years
5 33
3.2 Graph Attention Network
Recent research has shown the usage of GNNs with combinatorial optimization problems (including MaxSAT) to be promising B [7]. As such, we take inspiration from Graph Attention Networks (GATs), one of the SOTA architectures for graph based learning [24]. GATs equipped with attention mechanisms that compute specific weights (attention coefficients) for each neighboring node in order to prioritize important nodes, enabling leap in model capacity.
The attention mechanism of GAT's proceeds as follows. First, the attention coefficients eij and normalized attention coefficients Oij for neighbor node j of node i are calculated:
Cij = LeakyReLU (a" T [Wha]] Wh2 Why]/WhWWWWe (eeay)
(xp(C))
aij = ΣnEN, exp (Ess)
Here, a E R22 is a weight vector, || is concatenation operation, and W E RFF' W E XF are weight matrices (F and F' represent the number of features in a node at the input and output. and nd Fe the number of features in an edge), with the LeakyReLU nonlinearity being applied (ReLU with a slight negative slope). Furthermore, h; E R² is the feature of node i, eij E R is the edge feature between node i and j. and MG, is the set of neighbors of node i. The above notation is slightly modified to allow the use of multi dimensiaiansional edge features 77. Subsequently, these normalized attention coefficients are used to compute the final output feature hg E FR for node i:
h = Σ ai Wh;
(2)
JEN,
3

---

SGAT Block (k Blocks)
MaxSAT Problem JF
T-norm (V to C)
SGAT (C V7
T-norm (V C)
Bipartite Graph
Normalization
Approximate Solution v(K) v(t) 0.9
Initial Assignment &
Transform
F= (x - (=))
#= (x(x))= = =Z
k times
T-norm Aggregation
SGAT
Normalization
0.7
0.1
0.75
(m) 10-1--1(0pp v(rr))
Update
0.3g
closer to
0.9
0.25
Compute clause satisfaction
Attention (0. 70.7.0.3)
Center 0.5, Slope = 2.75
Architectural Diagram of SGATs. Each SGAT block is composed of t-norm layer, SGAT layer, and normalization layer. Red represents the values that are learned.
Figure 1:
4 SAT-based Graph Attention Network
In this section, we present key building blocks for constructing SGAT's shown in Figure SGATs are composed of three main components: (i) T-norm layers that compute clause valuations u(C) from the valuations of connected variables v(x), (ii) SGAT layers that update the valuations of variables based on the valuations of connected clauses, and (iii) a normalization layer that ensures the valuations of all variables are sufficiently spread out. A single block of SGATs approximates distributed local search step, with the attention mechanism learning which clauses to focus on, essentially serving as heuristic. We denote variables by zy and clauses by Cj. with valuations v(r,)),((,)) [0, 1]. For clarity, v(x;) and ((C)) correspond to features at nodes h2 and hytno respectively.
4.1 Graph Representation of MaxSAT Problems
Before applying GNNs to MaxSAT problems, have to transform them into graphs. To accomplish this, we employ a factor graph representation of given formulas, done in
61
C1
hg
prior works involving SAT and MaxSAT Solving 22 30 [7].
X1
Specifically, opt for representation similar obtain a bipartite graph with two types of nodes for both the
30 and
B55
C2
h4
clauses and variables as shown in Figure 2 The positive and negative polarities of the variables are then embedded into the edge features.
ha
X2
624
C3
hs
While existing graph representations used edge features to mainly differentiate between the polarities of variables, propose to embed crucial information as edge features, to allow the model to further differentiate between similar connections. We define the edge feature Ci.j+n between variable x; and
Figure 2: Bipartite graph for F (x) V--o:)A(ar Vx2]A(-a,) Solid and dashed lines each represent the positive and negative polarities re- spectively.
clause C, as follows:
W IN, 0,0
W
porm
if NZ
Cijtn
where w norn
Wj
0,0, (NT WÇ
norm ifieN,
max; Wik
Here, NVt and Nj correspond the set of variables with positive and negative polarities included in clause Cj. and umoom E (0, 1] represents the normalized weight of clause Cj. Note that when the denominator is O, we set the corresponding value to 0. These features align with common strategies

---

p(G) 0.7x(e(x,)
0.3x(o(x)) + 0.3)
Update messages my
mis ((G))+0
m2a = =(x2)
((C))
C
(0g)
23
0.7
(1 P(g-n))
v(G)) 0.6 (h2)
C1
224
0.3
X2
Railiv
X2
(64)
Negative
0.7 v(c2)
C2
m2
v(x))
0.4
m24 v + 0.3
Input Valuation of variable v(x))
Clause to Vuriables
(ii) Variable to 2 clauses
(a) Update message myy for æı and Cj-n- The above is visualization for v(C)-n) 0.6.
(b) Visualization of the update procedure with SGATs.
Figure 3: Illustration of the SGAT layer.
prioritizing shorter clauses over long ones 10 while also giving higher scores to clauses with larger weights; this is especially relevant edge features directly used for attention computation.
4.2 T-norm Layer: Variable to Clause
Here, we propose the use of (-norm based aggregations when computing clause valuations from connected variable valuations, shown in the bottom left of Figure [ By using t-norms, we compute clause valuations continuously while keeping valuations in [0, 1]. Given fuzzy truth degrees 01,- d1...... Og E [0, 1] the fuzzy conjunctions of these values can be computed using t-norms T [0, 1] > 1]. We specifically use the following three well-known t-norms:
1. Gödel t-norm: To(a1 a+) min (ai............................. ak)
2. Product t-norm: (a .... (kk) 11 04
3. Eukasiewicz t-norm: Ty, (a,,,..... .............................. .4)) max (0. -x= (k: 1))
As each clause is disjunction of literals, we compute valuations by negating the conjunction of each negated literal. Using strong negation defined as - for E [0, 1]. we set ö, = 1 v( if by Fir and Üür v(2rr) if 4,r -r for clause C, 41 V Lee. and define
(C,) 1 (Gn, ... -.e.).
where E PG L...
For simplicity, refer to the clause valuation computed by the chosen t-norm as v(C)).
Unsupervised Loss Function. By applying a t-norm aggregation, obtain clause valuations v(Ck). We then define a loss function that computes the total cost of the current assignment as:
T2 1 Wh (1 (1-v vCk)))
Σk W6
where m is the total number of clauses. The equation is weighted mean squared error of how unsatisfied each clause is, with the weights corresponding to the given weights for each clause. This loss function forces the model to train to minimize the total weight of unsatisfied clauses, without requiring any sort of ground truth labels, with the assumption that cost (all clauses satisfied) the optimal solution.
4.3
SGAT Layer: Clause to Variable
To efficiently learn which variables to update, employ attention mechanism and message- passing function that update the valuations variables based on the valuations of the clauses to which they connected (Figure (bb). Specifically, define the update message my and attention message my between variable x; and clause C,-n as follows:
(o(a)) + (1 - v-((C_)))) if E otherwise
{mg [1
if i m otherwise
ml (0(x,) (o1)))(1-((C,))) v((C-n))
m
5

---

The update messages mi represent the valuation the clause requests the variable to move toward, as shown in Figure 3a The attention messages m. represent the strength of this request by flipping the valuation for negatively appearing literals, aligning all messages in a common direction regardless of polarity. Using these messages, Equations (I) and (2) are redefined as:
LeakyReLU (a" (WeellWee)))
ej
v((x))
E JEN:
From the equation, long as the input valuations v(z,) [0, ai E [0, 1], and Ejex, ar the outputs v (xx4) [0, 1] are guaranteed to hold. This eliminates the need for additional activation functions after each layer, simplifying the computation of both variable assignments and the loss function. Additionally, we clamp the values of update messages to range [0. 1] whenever they leave the range (possible with certain t-norms). Extensive information on how SGATs handle imput-output dimensions is provided in Appendix(A) A
SGATs are approximations of greedy distributed local search; they perform local search in fully parallel and greedy manner. After computing clause valuations v(C), they send messages (m ! to all connected variable nodes (greedy) in parallel, with the strength proportional to how unsatisfied the clause valuation remains (mz)). The variables then use the attention mechanism explained above to decide which clause messages to prioritize, to maximally satisfy those requests from clauses. SGATs learn these distributed local search heuristics through attention, which lead to the best approximations.
Multi-head attention. Velickovic et al. 24 further employed multi-head attention to stabilize the learning process of self-attention for GATs. We also employ the same strategy by computing K independent attention coefficients and averaging the outputs of all heads. As the outputs for each head are guaranteed to be range [0,1], the final outputs here are also guaranteed to be in range [0.1].
4.4 Normalization Layer
To prevent feature values from being overly concentrated or dispersed, we apply normalization layer based on the sigmoid function, as shown in the bottom right of Figure The normalized feature for node i E [0, 1] is computed as:
M1 = 17 (2h, k))
where (-) denotes the sigmoid function, 7 parameter for controlling the spread of the values, and E [-1, 1] a parameter for controlling the center of the values. The input feature h; E [0, 1] is first scaled the [-1, range, after which the sigmoid modulates how close the output is to 0 or 1.
4.5 Approximation Ratio of SGATs
In previous works 17 the capabilities of differentiable MaxSAT solvers were evaluated theoreti- cally using the approximation ratio, which is the lower bound of the ratio of the value computed with the algorithm to the optimal value. In [17]. /2-apprroi ratio for unweighted MaxSAT is achieved by GNN architectures with hidden dimension sizes dependent on the number of clauses. We can prove that SGAT's achieve a 1 1/2-approximation for any unweighted Max-E&SAT problem (problems with exactly l literals per clause), and that this guarantee holds with fixed architectural settings independent the number of clauses. This result establishes a deterministic baseline that helps understand the theoretical capabilities of SGATs. The details are provided in Appendix E
4.6 Local Search with GNNs
To solve MaxSAT problems with SGATs, we introduce LS-GNN (Local Search with GNN, Algorithm D a novel local search solver based on the continuous optimization of SGAT's. LS-GNN takes as input a weighted MaxSAT instance F and returns the best valuation thest and cost Crest found for a given problem within a time limit. Starting from a random valuation v, SGAT maps the current valuations of variables and clauses to valuations that aim to maximize clause satisfaction. We iteratively optimize SGATs to minimize the loss in Equation
33) moving the valuations toward better solutions.

---

Algorithm 1: LS-GNN
In Weighted MaxSAT instance F, timeout T.
Out: Best valuation Uhest and its cost Ches- random assignment
Whest = =0 Creu +0C,
2 while elapsed time < T do
k: == 0, klocal = 0, Vocall 0, Clocal +00
while early stopping 2 k - klocol do optimize SGAT with respect to v cOst(F, SGAT(F,
ifc < Clocal then
Vlocal SGAT(F, v), ksocal k, Glocal C end k- k +
10
11
end
Clocat Chest then
13
Ubest = Vlocal, Cbest
Glocal
end
15
(1 - 3) B.A
16 end
To reduce the risk of the algorithm being stuck in a local optimum, we periodically randomize a subset of valuations (L15). This is done by sampling a binary mask 3 via thresholding uniform random distribution, and injecting new random valuations procedure is triggered whenever the best cost stops improving for early stopping epochs (L4). The parameters early stopping. elapsed time, 8. and A control the termination and randomization behavior of L.-LSSSNNNN GNGN;; their specific values are provided in Appendix A
for the masked variables. The randomization
While Algorithm 1 used SGAT's the GNN model, it can be used with any arbitrary model that is able to output assignment predictions. For simplicity, we refer to the LS-GNN with SGAT' and GATs LS-SGAT and LS-GAT, respectively.
5 Experiments
In this section, we conduct multiple experiments to answer the following questions regarding SGATs: Q1) Are SGAT's better than existing GNN architectures? Q2) What component makes our model efficient? and Q3) How can LS-GNN be compared with other continuous solvers? For evaluation, we use instances used in non-partial unweighted and weighted benchmark instances provided in MaxSAT evaluations which we denote MS and WMS (and collectively referred to as WMS+). also prepare a subset of these datasets with instances that are below specific file sizes such as 2MB for purposes such as training, and denote as WMS+(2MB). The training and testing splits are shown in Appendix D
5.1 Model Architecture
To evaluate the effectiveness of our model in learning to solve practical instances (MaxSAT Evaluation benchmark instances), we first conduct experiments using different model architectures. Provided that there is only one work regarding end-to-end MTxSAT solving with GNNs [7]. we also compare with models that were built for SAT. Specifically, we use NeuroSAT 22 and GGNN [1] with unsupervised loss functions presented in [19). they were shown to empirically work well [15]
Specific details regarding models are given in Appendix B
We compare the model performance on the MS2018(2MB) dataset, with training done on two different datasets: MS2018(2BB), and (ii) SR(U040,,00), randomly generated dataset with 40
hhtp::/mmaxxa-ccalautionnggg

---

SGAT
MS-ESFG NeuroSAT
0.9
GGNN
0.9
Satisfied Weight Ratio
Satisfied Weight Ratio
0.8
0.7
0.7
0.6
0.6
0.5
0.5
0.4
0.4
SGAT
MS-ESFG
NeuroSAT
20
40
60
80
20
40
60
80
Epochs
Epochs
(a) Trained with MS2018/2MB.
(b) Trained with SR(U(40,200)..
Figure 4: Comparative analysis of model architectures, with different training datasets. Test sets for both were MS2018(2MB). Solid: Test, Dashed: Train.
200 variables 22
We use the satisfied weight ratio performance metric, which is defined as:
Satisfied Weight Ratio == Wh roundder (Cx)(C)))
Wk
where (C(C)) E [0, 1] is the valuation of clause Cs computed using the Gödel t-norm, we is the weight of clause Ck. and the total number clauses. This score represents the ratio of the total weight of satisfied clauses to the total weight of all clauses, with a higher score indicating a strictly better solution.
We used SGATs with 6 SGAT blocks composed with Gödel T-norm layers and SGAT layers with 2 attention heads and 4 channels. For training, used the Adam optimizer with learning rate of 2 x 10 3 and a batch size of 4. For existing models, the default provided settings were used. The number of blocks are generally chosen strike the best balance between performance and computational efficiency, with the specific empirical results shown in Appendix [
5.1.1 Results
As shown in Figure completely fail to do so. Given that the training dataset consists of problems from various domains, we can infer that SGATs are capable of learning solve wide range of problems. Figure 4b] further supports this conclusion; even with synthesized datasets, our model is able to learn a distributed local search heuristic that has high performance practical (non-synthesized) datasets. Overall, this shows our models' dominant strength in solving MaxSAT problems. Additionally, the scalability difference between existing models and SGAT's shown to be huge, due the large difference in parameter numbers. For the training with MS2018(2MB)) existing architectures could only handle batch size of In contrast, SGAT's could support batch sizes of up contributing the high stability of our model. Extensive results are shown and discussed in Appendix D
model is able to learn solve from practical instances, while others
5.2 Ablation Study
To highlight which components of our model yields the highest performance increase, performed ablation studies focusing on two points: (a) SGAT and T-norm layer, and (b) types of t-norm. For (a), we consider two variants of our model, one with SGATs swapped GAT with Sigmoid, and another swapping out the T-norm layers with GATs. As SGATs are dependent on T-norm layers being used, we do not experiment with T-norm layers swapped with SGATs. For (b), we compare using three different fundamental t-norms that have been frequently used for machine learning: Gödel, Product, and Eukasiewicz. The experiments were all performed with WMS+2018(MBB as the training and testing set, with the same model parameters as the previous experiment.

---

0.86
0.86
Satisfied Weight Ratio
Satisfied Weight Ratio
0.82
0.82
0.80
0.80
MMM
0.76
0.76
0.74
0.74
SGAT
GAT
Gödel
Product
0.72
0.72
tukaslewicz
500
1000
1500
2000
500
1000
1500
2000
Epochs
Epochs
(a) Ablation SGAT Layer and T-norm Layer
Ablation of different t-norms.
Figure 5: Results of ablation studies. Training and testing were done on WMS+2018(2MB) Solid:
Test, Dashed: Train.
5.2.1 Results
Figure shoos the results for each ablation study. From the first ablation study, we can that our current model architecture achieves the best performance, with significantly high stability. Furthermore,
shows
that having the T-norm layer for clause value updates in place of GAT layer highly increases the stability, even though the total number of trainable layers essentially halve.
From the second ablation study, better than Lukasiewicz. This is thought to be because Lukasiewicz outputs 0 when the input values too low, making the gradients zero in certain regions, hindering the training process. On the other hand, the other two t-norms do not have this issue, resulting in more stable and effective optimization. Additionally,
observe that Gödel and Product t-norms work substantially
observe that Gödel converges slightly faster than Product. This is thought to be due to the compatibility between SGAT layers and Gödel t-norm; as it is guaranteed that no variable will have higher values than the clause it is connected to, the update message never goes out of the range [0, I], removing the need of any clamping procedures.
5.3 Local Search with SGATs
In our second experiment, tested the performance of solvers based continuous optimization at approximating solutions on both unweighted and weighted benchmark instances. We used LS- LS-GNN with GATs and SGATs pretrained in the previous experiment (as LS-GAT and LS-SGAT) backbone models. We compared our solvers to three existing solvers based on continuous optimization: the Mixing method (25) the MIXSAT algorithm (6)), and FourierSAT [12. The default settings were used for all solvers. As the only continuous solver that addresses weighted MaxSAT is FourierSAT AT, we conduct experiments comparing our model only with FourierSAT on WMS instances. We specifically make implementation changes to support weights, as the original does not do so at default.
To evaluate the approximations computed by each solver, we calculated the incomplete scores, a metric that has been used to evaluate incomplete MaxSAT solvers recent years of MaxSAT evaluations. The incomplete scores defined as
(1 + cost of best known cost for i)
score(s, i) (1 + cost of solution for i found by s)
where is the instance and s the solver used. For reference, we retrieve the best known cost for each instance from the official MaxSAT Evaluation results. We combine this with the best found cost for each dataset and timeout setting, keeping it comparable with existing methods. However, we note that due our solvers finding better solutions than the competition results, the best known cost completely identical to the official results.

---

Table 1: Average Incomplete Score for solvers based on continuous optimization, evaluated on unweighted (MS) and weighted (WMS) benchmark instances. Bold shows the best score, and underlined show the second best score.
60s timcout
300s timcout
Type
Solvers
2020
2021
2022
2023
2024
2020
2021
2022
2023
2024
Mixing
0.3729
0.3442
0.3864
0.0703
0.1564
0.3603
0.3443
0.3864
0.0703
0.1564
MIXSAT
0.4887
0.5017
0.4980
0.1367
0.3077
0.4796
0.5053
0.5269
0.1429
0.3100
MS
AT
0.4304
0.4023
0.3560
0.1429
0.1189
0.4498
0.4672
0.4205
0.1692
0.1595
LS-GAT 0.3948
0.4268
0,4839
0.0331
0.1284
0.4281
0,4359
0.5263
0.0919
0. 1413
LS-SGAT
0.5237
0.5420
0.6202
0.1653
0.3516
0.5289
0.5541
0.6403
0.1828
0.3684
Aou
0.2304
0.3340
0,4452
0.2974
0.0144
0.2369
0.3523
0.4490
0.2967
0.0163
WMS "LS-GTT
0.6936
0.7197
0.6925
0.7636
0.6650
0.7384
0.8005
0.728
0.8216
0.7156
LS-SGAT
0.8499
0.8973
0.7587
0.8432
0.7816
0.8342
0.8835
0.7594
0.8471
0.7840
5.3.1 Results
Table [ shows the average incomplete score for each solver depending on the year of evaluation. From the results, we can see that LS-SGAT clearly outperforms every other existing solver based on continuous optimization, with average improvement of 0.055 for MS, and 0.09 for WMS versus the second best solver. However, we can also observe that the differences are not constant for every year. This is analyzed to be due to the types of problem each year contains; some solvers perform better on specific instances than others. Nevertheless, we can confirm that the overall, SGAT's perform significantly better on a wide range of problems compared to existing continuous methods.
Another important factor that we observed was that the size of problems the algorithm was able to handle was much different. While SGATs were able to handle all but one instance, others went over the timelimit on tens to up to hundreds of instances, showing that our model and algorithm scales much better than existing approaches. This is mainly due to the efficiency of GNN architectures; GNNs tend to have much fewer parameters, which are independent of the problem size. We further analyze this with more experimental results in Appendix D
SGATs as Initialization Heuristics. While our primary concern is to develop a differentiable method for MaxSAT solving. it is worth investigating how SGAT's can predict good assignments for a given Weighted MaxSAT instance and whether such a predicted assignment can be used as an initial assignment for SOTA solver. In this context, we have conducted additional experiment where the predictions of SGAT's are used as initialization heuristics for tfate-of-the-ar incomplete solvers. The results were positive, with incomplete solvers being able to achieve substantially higher incomplete scores when combined with SGATs, supporting our claim that SGATs can work equally well in practical settings. The extensive results are shown in Appendix C
6 Conclusion and Future Work
We presented SGATs as novel GNNs that utilize attention and message passing mechanisms that oper- ate on t-norms. SGAT layers approximate greedy distributed local search, with their heuristics being the main learnable component. To demonstrate the effectiveness of our model, we further developed a continuous local search algorithm that is built on top of SGAT's to solve given MaxSAT instances in a continuous manner. Experimental results showed that SGATSs train in a highly stable manner, with approximations clearly outperforming those produced by existing neural- based architectures. Our model also outperforms tfte-offthheart continuous solving approaches, demonstrating the strength of our model to output good approximations, even against theoretically sound approaches.
Future works will be focused on expanding the current framework to support partial MaxSAT problems, which require the satisfaction of hard clauses, and is known to be difficult for Neural Networks. Another interesting direction would be to incorporate SGATs into machine learning systems for tasks such as recognition and prediction. Especially in neuro-symbolic systems where MaxSAT solvers are used [9. SGAT's can easily replace the solvers to allow for end-to-end learning.
10

---

Acknowledgments
This work has been supported by JSPS KAKENHI Grant Number JP25K03190, JST CREST Grant Number JPMICR22D3 and JST SPRING Grant Number JPMISP2104, Japan.
References
[1] Saced Amizadeh, Sergiy Matusevych, and Markus Weimer. Learning To Solve Circuit-SAT: An Unsupervised Differentiable Approach. In 7th International Conference on Learning Representations, ICLR. OpenReview.net, 2019. URL https://openreeview wwwpaarrviiie.neeffrrnrn net/forum? id=BJxgz2R9t7
[2] Shaowei Cai and Zhendong Lei. Old techniques in new ways: Clause weighting, unit propaga- tion and bybridization for maximum satisfiability. Artif. Intell., 287:103354, 2020. doi: 10.1016 J.ARTINT 103354. https:/s:////i htt.///0o.orr//.... 1016/j artint 2
[3] Quentin Cappart, Didier Chételat, Elias B. Khalil, Andrea Lodi, Christopher Morris, and Petar Velickovic. Combinatorial Optimization and Reasoning with Graph Neural Networks. J. Mach. html
Learn. Res., 14:130:1-130:0 2023. http:tt:://mne wttp://pappps//////211eeeeeee
[4] Wenjing Chang, Hengkai Zhang, and Junwei Luo. Predicting Propositional Satisfiability Based on Graph Attention Networks. Int. Comput. Intell. Syst., 15(1)884, 2022. doi: 10.1007/ $44196-022-0013999 (tLp:tt:::/// //doi. 0ttp://000000/4441100000-0000010
[5] Yi Chu, Shaowei Cai, and Chuan Luo. NuWLS: Improving Local Search for (Weighted) Partial Thirty-Sevents AAAI Conference on Artificial Intelligence, pages 3915-3923. AAAI Press, 2023. doi: 10. 10.1609/AAAAV3314.25555 URL
MaxSAT by New Weighting Techniques.
https://doi..org// 1609/ aaai. v3714. 25505
[6] Artur d' Avila Garcez and Luís C. Lamb. Neurosymbolic Al: the 3rd wave. Artif. Intell. Rev. 56 (11):12387-12466 2023. doi: 10.1007/S10462-0033 10443-004--W W. URL https://////
1007/s10462- 023- 10448-w
[7] Matthias Fey and Jan E. Lenssen. Fast Graph Representation Learning with PyTorch Geometric.
In ICLR Workshop on Representation Learning on Graphs and Manifolds, 2019.
[8] Thomas Fournier, Arnaud Lallouet, Télio Cropsal, Gaël Glorian, Alexandre Papadopoulos, Antoine Petitet, Guillaume Perez, Suruthy Sekar, and Wijnand Suijlen. A Deep Reinforce- ment Learning Heuristic for SAT based on Antagonist Graph Neural Networks. In 34th IEEE International Conference on Tools with Artificial Intelligence, ICTAI, pages 1218-1222. IEEE, 2022. doi: 10. 111////AAA51111222222222222 00. URL https://doi. org.oi..org/// 1109/
ICTAI56018 00185
[9] Eleonora Giunchiglia, Mihaela Catalina Stoian, Salman Khan, Fabio Cuzzolin, and Thomas Lukasiewicz. ROAD-R: the autonomous driving dataset with logical requirements. Mach.
Learn., 11( 2023. doi: 10.1007/S10994-022 103-09999-3--6322--2 URL https:///oo
org/10. 1007/ s1000////1944---00 023-06322-22222
[10] Said Jabbour, Jerry Lonlac, Lakhdar Saïs, and Yakoub Salhi. Revisiting the Learned Clauses Database Reduction Strategies. Int. J. Artif. Intell. Tools, 2788):1850333:1 1850033:19, 2018. doi:
StRLhhtpps://// wtt.oiooog//..1111
80218213018500338
[11] Vitaly Kurin, Saad Godil, Shimon Whiteson, and Bryan Catanzaro. Can Q-Learning with Graph Networks Learn a Generalizable Branching Heuristic for SAT Solver? In Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems, 2020. URL
[12] Anastasios Kyrillidis, Anshumali Shrivastava, Moshe Vardi, and Zhiwei Zhang. FourierSAT:
A Fourier Expansion- -Based Algebraic Framework for Solving Hybrid Boolean Constraints. In The Thirty-Forr Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, pages 1552-1560.
11

---

AAAI Press, 2020. doi: 10.160%/AAALVV340225555 URL ftttp:://doi.0rg11..1oo aaai. v34102.5515
[13] Luís C. Lamb, Artur d' Avila Garcez, Marco Gori, Marcelo O. R. Prates, Pedro C. Avelar, and Moshe Y. Vardi. Graph Neural Networks Meet Neural-Symbolic Computing: A Survey and Perspective. In Pruceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, pages 4877-4884 ijcai.org. 2020. doi: I0.24966/IICAA22200606
htll.ttts:://do org/ / 10. 24963/ jicaiiiaa... 2020/6229999
[14] Yujia Li, Daniel Tarlow, Marc Brockschmidt, and Richard Zemel. Gated Graph Sequence Neural Networks. In 4th International Conference Learning Representations, ICLR 2016, Conference Track Proceedings, 2016. URL httt:://axii. owg/ 1511, 05493
[15] Zhaoyu Li, Jinpei Guo, and Xujie Si. G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks. Trans. Mach. Learn. Res., 2024, 2024. URL https /oopeneevie net /
[16] Chanjuan Liu, Guangyuan Liu, Chuan Luo, Shaowei Cai, Zhendong Lei, Wenjie Zhang, Yi Chu, and Guojing Zhang. Optimizing local search-based partial MaxSAT solving via initial assignment prediction. Science China Information Sciences, 221011112000--222000,, 2024, doi: 10.1007//114432--23-390000
URL /el.ltttgee/ooooooo////000001/12
[17] Minghao Liu, Fuqi Jia, Pei Huang, Fan Zhang, Yuchen Sun, Shaowei Cai, Feifei Ma, and Jian Zhang. Can Graph Neural Networks Learn to Solve MaxSAT Problem? CoRR, abs/21 11.0568, 2021. URL htRpsstps: / wrwiv. org/ abs/ 2111. 2111.07568.
[18] Sota Moriyama, Koji Watanabe, and Katsumi Inoue. GNN Based Extraction of Minimal Unsatisfiable Subsets. In Inductive Logic Programming 32nd International Conference, ILP 2023, volume 14363 of Lecture Notes in Computer Science, pages 77-92. Springer, 2023. doi: 10.10007998-3-03144499
URL https: //doi 10 1007 htt.:////000000077776--30----990
[19] Emils Ozolins, Karlis Freivalds, Andis Draguns, Eliza Gaile, Ronalds Zakovskis, and Sergejs Kozlovics. Goal-Aware Neural SAT Solver. In International Joint Conference Neural Networks, IJCN 2022, Padua, Italy, July 18-23, 2022, pages 1-8. IEFE, 2022. doi: 10. (B99DCCNN500442222288777777 URL battps:///o/ org/ 110.1011000/C11155544.4... 9892733
[20] Md. Kamruzzaman Sarker, Lu Zhou, Aaron Eberhart, and Pascal Hitzler. Neuro-symbolic artificial intelligence. A/ Commuun., 34(3):197-209, 2021. doi: 10.3233/AIC-210084 URL https://doo
org/10. 3233/ CIB//AIC-200 210084
[21] Daniel Selsam and Nikolaj S. Bjömer. Guiding High-Performant SAT Solvers with Unsat-Cors Predictions. In Mikolás Janota and Inés Lynce, editors, Theory and Applications of Satisfiability Testing 5AT 2019 22nd International Conference, volume 11628 of Lecture Notes in Computer Science, pages 336-353. Springer, 2019. doi: 10. 10001007---0000-220000 7 //doi.org/// 1007 00007/977-220 0-77788--300-220 000------8----2--------------- 24228-99222
24. URL httpp
[22] Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning SAT Solver from Single-Bit Supervision. In 7th International Conference on Learming Represenaations, ICLR 2019. OpenReview.net, 2019, URL htttttts///ppereiiiii
net//forum?.d-HHJCC_LM. 1A5tm
[23] Jan Tönshoff, Berke Kisin, Jakob Lindner, and Martin Grohe One Model, Any CSP: Graph Neural Networks as Fast Global Search Heuristics for Constraint Satisfaction. In Proceedings of the -heoon International Joint Conference on Artificial Intelligence, IJCAI 2023, pages doi: 10.2496//IICA1.2222//776 URI. https://doii arg/10
4280 ijcai.org, 2023.
24963/ijcaa /tt/////4a..223/776 2023/476
[24] Petar Velickovic, Guillem Cucurull, Arantxa Casanova, Adriana Romero, Pietro Liò, and Yoshua Bengio. Graph Attention Networks. In 6th International Conference on Learning Represen- tations, ICLR 20/8. OpenReview.net, 2018. URI, httpppp://opeeeeeieee..eeee wwwpenwwwwwwwwwwwweeeeeeeeeeeeee wwtp:/rrmt.eetitieeeemm
rJXMpikCZ
12

---

[25] Po- Po-Wei Wang and J. Zico Kolter. Low-Rank Semidefinite Programming for the MAX2SAT Problem. In The Thirty- Third AAAI Conference on Artificial Intelligence, AAAI 2019, pages 1641-1649. AAAI Press, 2019. doi: 10. 10.1609/AAALV333000 13311113311111111 1641. URthttps:: //doi org/10. aaai.v33i11.
v33101 33011641
[26] Po- Fei Wang, Wei-Cheng Chang, and J. Zico Kolter. The Mixing method: coordinate descent for low-rank semidefinite programming. CoRR, 2ee/1706.00444 2017. htttt:tttparr::
org/abs/17066 00476
[27] Po-Wei Wang, Priya L. Donti, Bryan Wilder, and J. Zico Kolter. SATNet:
Bridging deep learning and logical reasoning using differentiable satisfiability solver. In Proceedings of the 36th International Conference on Machine Learning, ICML 2019, volume 97 of Proceedings of Machine Learning Research, pages 6545-6554, PMLR, 2019. http:htt://prroeeeeie
mlr. wwwps/eeeer wttp//99///////eeeeee/ html
[28] Meixi Wu, Wenya Wang, and Sinno Jialin Pan. Deep Weighted MaxSAT for Aspect- based Opinion Extraction. In Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing, EMNLP 2020, pages 5618-5628. Association for Com- putational Linguistics, 2020. doi:
URI. https
//doi.org/11 1ww.1116/11v0000 emn www.p-main.n....mmmmmmmmmmmmmaam 453
[29] Zhun Yang, Adam Ishay, and Joohyung Lee. Learning Solve Constraint Satisfaction Problems with Recurrent Transformer. In The Eleventh International Conference on Learning Represen- tations, ICLR 2023. OpenReview.net, 2023. URL https::t////// htttps://openrevier. fore/fff 2dC
[30] Emre Yolcu and Barnabás Póczos. Learning Local Search Heuristics for Boolean Satisfiability. In Advances Neural Information Processing Systems 32: An- nual Conference on Neural Information Processing Systems 2019, NeurIPS 2019.
pages 7990-8001, 2019. URL htttps://proceedinnng Abstract. html
[31] Wenjie Zhang, Zeyu Sun, Qihao Zhu, Ge Li, Shaowei Cai, Yingfei Xiong, and Lu Zhang. ALocalSAT: Boosting Local Search with Solution Prediction. In Proceedings of the Twenty- Ninth International Joint Conference Artificial Intelligence, ISCAI 2020, pages 1177-1183. ijcai.org, 2020. doi: 10.24963IJCAA.20200166 URL httpt:///doii 2020/164
[32] Jiongzhi Zheng, Kun He, Jianrong Zhou, Yan Jin, Chu-Min Li, and Felip Manyà. BandMaxSAT: Local Search MaxSAT Solver with Multi-armed Bandit. In Proceedings of the Thirty- First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July 2022, pages 1901-1907. ijcai.org. 2022. doi: 10.24963/DCAL22222266 URL https: orw.:/...rg/1... wtt.:/..........11111 24963/jjcacicci 2022/264
[33] Jiongzhi Zheng, Zhuo Chen, Chu-Min Li, and Kun He. Rethinking the Soft Conflict Pseudo Boolean Constraint on MaxSAT Local Search Solvers. In Proceedings of the Thirty-Third Inter- national Joint Conference on Artificial Intelligence, IJCAI 2024, pages 1989-1997. ijcai.org.
2024. URL https::t////// //w:://wwww www..jje.. ijcai. wrw. http/proceednngs//222//222
13

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: The abstract and introduction clearly state that the paper proposes SGAT's and uses them for solving MaxSAT problems using continuous optimization, which matches the core contributions evaluated through experiments (Sections 3, and 6).
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or
NA answer to this question will not perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results
be expected to generalize other settings.
is fine to include aspirational goals as motivation as long is clear that these goals are not attained by the paper.
2. Limitations
Question:
Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification: The paper discusses how the proposed method currently does support partial MaxSAT and that integration into complete solvers remains future work (Section 6).
An extensive discussion is given Appendix F
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on a few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low images are taken in low lighting. Or speech-to-text system might be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory assumptions and proofs
14

---

Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [Yes]
Justification: The appendix contains a complete proof (Appendix Ep. and all assumptions are clearly stated.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Does the paper fully disclose all information needed to reproduce the main ex- perimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless whether the code and data are provided or not)?
Question:
Answer: [Yes]
Justification: The paper describes model architecture, training setup, evaluation metrics, and datasets used (Section 5), with additional details provided in Appendix D
Guidelines:
The answer NA means that the paper does not include experiments.
the paper includes experiments, a No answer to this question will not perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution a novel architecture, describing the architecture fully might suffice, or if the contribution is specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, provide access to the model. In general. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how replicate the results, access hosted model (e.g.. in the case of a large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily new algorithm, the paper should make it clear how to reproduce that algorithm.
(b) the contribution is primarily a new model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is a new model (e.g., a large language model), then there should either be way access this model for reproducing the results way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (c.g., to registered users), but it should possible for other researchers to have some path to reproducing verifying the results.
15

---

5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, described in supplemental material?
Answer: [Yes]
Justification: The datasets are from publicly available MaxSAT evaluations. The code is available at lattps://gt heggtgtt........ com/ Sotam2369/SSATT
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurlPS code and data submission guidelines (https://nips.cm
for more details.
While we encourage the release of code and data, we understand that this might not be possible, so "No" an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https
http:/.cccpublbc/uuuuceee Codeeubmii ssi criionPooiccy for more details.
The authors should provide instructions on data access and preparation, including how access the raw data, preprocessed data, intermediate data, and generated data,
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information possible in supplemental material (appended to the paper) recommended, but including URLs to data and code permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: Section 5 and Appendix D detail the model parameters, optimizers, datasets, and training protocol. More information can be found in the repository.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core the paper to a level of detail that is necessary appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, as supplemental material.
7. Experiment statistical significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [Yes]
Justification: Experiments were conducted multiple times, and the graphs are clearly accom- panies by error bars. The appendix also provides a detailed description of the experimental results.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by emoor bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
16

---

The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
It should be clear whether the error bar is the standard deviation the standard error of the mean.
is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out range (e.g. negative eтror rates).
If error bars reported in tables plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification: The appendix describes the compute setup including GPU usage and timeout thresholds.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary failed experiments that didn't make into the paper).
9. Code ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics
Answer: [Yes]
Justification: No ethical issues arise; standard datasets and models are used, and no sensitive or human data is involved.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require a deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., there a special consid- eration due to laws or regulations in their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification: The conclusion highlights possible integration into neuro-symbolic systems and other ML pipelines, noting both performance and deployment benefits. An extensive discussion is given in Appendix
17

---

Guidelines:
The answer NA means that there no societal impact of the work performed.
If the authors answer NA or No. they should explain why their work has no societal impact why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considcrations.
The conference expects that many papers will be foundational research and tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning conrectly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Does the paper deseribe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification: The paper introduces no high-risk model or dataset requiring special safe- guards.
Guidelines:
The answer NA means that the paper poses such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model. for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Justification: All datasets and methods are cited properly with references to their original publications and public repositories.
Guidelines:
The answer NA means that the paper does not existing assets.
The authors should cite the original paper that produced the code package dataset.
The authors should state which version of the asset used and, possible, include URL.
18

---

The name of the license (e.g., CC-BY 4.0) should be included for each asset. For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.
assets are released, the license, copyright information, and terms use in the package should be provided. For popular datasets, paperssi thoode com/ comddatasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided. If this information is not available online, the authors are encouraged to reach out to the asset's 's creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
Justification: The SGAT model is novel, and its details are fully described in the paper with implementation provided in the repository.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification: No human subjects or crowdsourcing were involved.
Guidelines:
The answer NA means that the paper does involve crowdsourcing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According to the NeurlPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or equivalent approval/review based the requirements of your country institution) were obtained?
Answer: [NA]
Justification: No human subject data was used.
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with human subjects.
19

---

Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if' applicable), such as the institution conducting the review.
16. Declaration of LLM usage
Does the paper describe the usage of LLMs if is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, or formatting purposes and does not impact the core methodology, scientific rigorousness, originality of the research, declaration is not required.
Question:
Answer: [NA]
Justification: LLMs were not used for method development or experiments.
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs as any important, original, or non-standard components.
Please refer to our LLM policy httpp:////eerrps..ccco/////eee/e for what should or should not be described.
20

---

A Additional Details on SGATs
A.1 SGAT Architecture
The SGAT model begins with a lightweight initializer module that transforms the input variable assignment into hidden embedding. This module is implemented single-layer MLP:
init(x) = ( + b)
where x E [ the initial assignment (usually z; ~ Uniform (0. 1)), a a sigmoid activation, and W learned weight matrix mapping from dimension I to the hidden dimension d.
The purpose of the initializer is to project scalar input values into a richer embedding space before message passing begins. This allows the attention mechanism in subsequent SGAT blocks to operate over informative feature vectors rather than raw values.
Empirically, this step contributes to faster convergence and higher clause satisfaction, especially during early training. The initializer is shared across all variables and does not depend on graph structure, ensuring a consistent embedding style for all inputs.
On the other hand, outputs are simply averaged, essentially making the final assignment of variables a vote over all hidden dimensions.
A.2 Early Stopping and Random Restarts for LS-GNN
During the search we combine per-instance early stopping with controlled variable perturbation and occasional random restarts to avoid local optima. Each instance maintains its own carly-stopping counter and patience, which is adaptively increased when significant improvements are observed; when the counter triggers, we do not fully reinitialize the assignment. Instead a binary mask / is sampled by thresholding uniform distribution at per-instance probability p (the probabilities cycle through a schedule such as {0.1, 0.2, 0.3, 0.5, 1.0] on successive triggers). New random values A sampled and used to replace only the subset of variables selected by 3. preserving useful partial assignments while injecting diversity. Occasionally, when prolonged stagnation occurs, we perform full random restart. This adaptive combination of targeted perturbation and occasional restarts balances local exploitation and global exploration, improving the solver's ability to escape local minima while retaining promising partial solutions.
B GNN Architectures
Table 2: Training configurations for GNN baselines. All models were trained for 100 epochs with early stopping and learning rate scheduling. The MS-ESFG configuration was manually added for comparison.
Model
Graph
Iterations
Hidden Dim
LR
Weight Decay
GGNN 14
VCG
32
64
0.002
1 x 10-8
NeuroS AT 22
LCG
32
128
0.002
1 x 10-8
MS-ESFG 17
VCG
20
128
2 10-5
x 10-10
GGNN 14]
A gated graph neural network architecture that uses GRU-style updates to propagate information over graph nodes. has been commonly used for reasoning tasks due its recurrent structure.
message passing neural network designed for satisfiability problems, using symmetric updates over literals and clauses on the LCG (literal-clause graph).
NeuroSAT 22
MS-ESFG [17]: A GNN architecture proposed by Liu et al. [17] for learning solve MaxSAT. It uses edge-splitting factor graphs (ESFG) with a transformer-style encoder and was evaluated on synthetic MaxSAT benchmarks.
VCG and LCG VCG (Variable-Clause Graph) a bipartite graph representation where nodes correspond variables and clauses, with edges indicating the inclusion of a variable (or its negation)
21

---

LCG*
VCG
Figure 6: Visual comparison between VCG and LCG representations, shown in
13
in clause. Polarity (positive or negative) is often encoded as edge features. LCG (Literal-Claus Graph), used in NeuroSAT, instead treats each literal (i.e., 2; and -x;) as separate node, resulting in more fine-grained graph with symmetric updates between literal and clause nodes (see Figure (
To implement all GNNs above, including GGNN, NeuroSAT, and MS-ESFG, utilized the open- source G4SATBench framework [15]. which provides standardized model definitions, training procedures, and evaluation protocols for GNN-based SAT solvers. This ensures consistency across implementations and allows for fair comparison under unified training and evaluation settings. Additionally, modified the evaluation routine calculate Clause Satisfaction, as defined and used in the main paper shown in Section 5.]
B.1 Unsupervised Loss Function
All models were trained using the unsupervised loss function originally proposed by Ozolins et al. 19 Let o(x;) E [0, 1] denote the valuation assigned to variable T;. The loss defined as
-
= E log CEo
II (1-v(z;)) II o(x:)) 2,EC+
aCEC-
where C+ and C' denote the sets of variables appearing positively and negatively in clause C, respectively. This formulation provides smooth and fully differentiable estimate of clause valuations. allowing effective training without ground-trute labels.
Algorithm 2:
SLS solver with SGAT-Based initialization
Input AT instance F, timeout
Output: : Best solution found Whest and its cost Chest-
Thest 0, Chest = +00
while elapsed time < do
I SSAA_IIniiia [nii_Innniaaa((])
while Restart condition not reached do
C = cost(r)
if C Obez then Bbest = I, Obest = C
end
1 - SelectVariabled
Flip(x,11
end
12 end
return Pbest: Chest
22

---

Algorithm 3: SGAT-Based Initialization
Input :axSAT instance F.
Output: Initial assignment I:.
v(a:)0 Randomkssignment/ u(z) SGAT(F, v(x)))
3 foreach variable in F do
Uniform(()) 0, 1) < vz)); SGAT then
24
else
24 0
end
end
10 return 2
C
SGATs as Initialization Heuristics
C.1 Stochastic Local Search with SGAT
We propose SLS-SGAT (Stochastic Local Search with SGAT), a solver that integrates SGAT pre- dictions as initialization heuristics for state-of- of-the-art SLS solvers, shown in Algorithms 2 and 3] This builds on prior work that uses GNN predictions for heuristic guidance in SAT solvers 31], but introduces novel variable assignment scheme based entirely on SGAT predictions. Specifically, each variable is initialized based on thresholding its predicted value, enabling the solver to take full advantage of the inductive biases learned by SGATss
In principle, this approach can be applied to any SLS solver that relies on random initialization. In this paper, we evaluate this technique by modifying four SOTA solvers to follow the SGAT-based initialization scheme shown in Algorithm
C.2 Experiments
In this experiment, we evaluate whether SGAT predictions can serve as effective initialization heuristics for four state-of-thh-ar SLS solvers: SPB 33, NuWLS 5), BandHS 332. and SATLike3.0
[2] These solvers represent the cop-perfrriing incomplete MaxSAT solvers from recent MaxSAT Evaluations, with NuWLS and SPB featured in winning entries from 2022 to 2024.
Each solver was modified to incorporate the SGAT-based initialization strategy described in Algo- rithms 2 and 3
To ensure fair comparison, SGAT inference time was included in the overall solver
timeout.
Table 3: Average Incomplete Score for each SLS solver and our proposed modification, evaluated on unweighted and weighted benchmark instances. Bold shows the best score, and underlined shows the second best score.
60s timeout
300s timeout
Solvers
2020
2021
2022
2023
2024
2020
2021
2022
2023
2024
SPB
0.8964
0.9175
0.9159 0.8862
0.7699
0.9050
0.9206
0.9215 0.8907
0.7820
+ SLS-SGAT
0.9045
0.9220
0.9200
0.8955 0.7845
0.9178
0.9258 0.9335
0.8998
0.7914
NuWLS
0.8932
0.9143 0.9155
0.8807
0.8885
0.9045
0.9213 0.9177 0.8907
"090533
+ SLS-SGAT
0.9049
0,9209 0.9217 0,8944 0.9036
0,9175
0,9280 0.9327 0.8988
0.9134
BBndHS
0.8563
0.8754 0.3630 0.8696
6.7442
0.8751
0.8903 0.864T 0.8810
70.391
SLS-SGAT
0.8616 0.8813 0.8634 0.8783 0.7557 0.8785
0.8924 0.8827 0.8888
0.7747
SATLike3.0
0.8327
0.8474 0.8193
0.8582 0.7393
0.8479
0.8628 0.8295 0.8718
0.7543
SLS-SGAT
0.8388
0.8640
0.8093 0.8707
0.7492
0.8521
0.8754
0.8367
0.8781 0.7671
23

---

incomplete Scores (all)
Incomplete Scores (all)
0.8
0.8
NUWLS+ (0.9096)
NUNLS + (0.9189)
NuWLS (0. 8993)
NUWIL 10.9085)
0.6
0.6
SPB+SGAT (0.8916)
SPB SGAT 9002)
SPB (0.9638)
SPB (0.8905)
0.4
0.4
B (0.8518)
BandHS (0.8684)
Dandlis (0 0466)
Dandlii (0 (0.06355)
0.2
SATLike3.0 (0. 8307)
0.2
5ATLike3.0 SGATT (0.8462)
SATLIRe3.0 (0.8238)
SATLIKe3.0 (0.8378)
100
200
300
400
500
0
100
200
300
400
500
Benchmarks
#Benchmarks
(a) Cactus plot at 60s timeout.
(b) Cactus plot at 300s timeout.
Figure 7: Cactus plots comparing incomplete solvers before and after SGAT-based initialization. Y-axis shows the score achieved, and X-axis shows the number of benchmark instances. Higher is better.
C.2.1 Results
Table
presents the average incomplete across benchmark from 2020 2024. All solvers consistently benefited from SGAT-hassdd initialization, with hybrid versions of NuWLS and SPB achieving state-of-the-art results. Notably, NuWLS showed average improvement of 0.008-coo compa-comparable to or greater than the score margin separating first and second place in recent MaxSAT Evaluation tracks.
While minor regressions were observed in isolated cases (e.g., NuWLS on 2022), the consistent overall improvements demonstrate the utility of SGATs in guiding local search. These gains suggest that SGATs effectively prune the search space by providing better starting points.
Figure illustrates these results as cactus plots, showing the number of benchmark instances solved across a range of score thresholds. SGAT-enhanced solvers consistently improve upon their vanilla counterparts under both 60s and 300s timeouts.
D
Additional Experimental Details
All code for experiments can be found in: http:///hthhuuccoooooo//2//33///
Evaluation Environment. All experiments were done machine with AMD Ryzen Threadripper PRO 3975WX 32-Cores and two NVIDIA RTX A6000 GPUs.
D.1 Benchmark Instances
Table 4: The number of benchmark instances used from each year of the MaxSAT evaluations
Year
Unweighted
Weighted
MaxSAT 2020
75
57
MaxSAT 2021
55
60
MaxSAT 2022
50
36
MaxSAT 2023
30
49
MaxSAT 2024
39
34
We particularly performed experiments on the non-partial weighted and unweighted benchmark instances that were used throughout each year's competitions. The number of instances per year is shown Table The train/test splits for MaxSAT 2018 is given in the repository.
24

---

Table 5: Effect of number of SGAT blocks on Weighted Satisfaction Ratio (WSR).
Metric
1
2
3
5
7
8
9
10
WSR
83.57
83.78
84.20
84.29
84.04
84.38
84.46
84.42
84.52
84.56
D.2
Effect of number of layers
The number of SGAT blocks used in the model was chosen empirically. While increasing the number of blocks tends to improve model performance during training as shown in Table larger models increase the runtime of the optimization procedure (Algorithm I and require more memory. After sweeping the number of blocks we found that performance improved up to point and then leveled off or degraded due to these practical costs. We therefore use 6 blocks as our default, which we found to be the best trade-off between performance and resource cost in our experiments.
Incomplete Scores (all)
Incomplete Scores (all)
L5-5GAT (0.4640)
LS-SGAT (0.4800)
MIXSAI (0.4211]
MIXSAI (0.42/9)
0.8
L5-GAT (0.3345)
FourerSAT (0.3687)
FourlerSAT (0.3242)
LS (..3643)
0.6
Mixing (0.2973)
0.6
Mixing (0.2952)
0.0
0.0
#Benchmarks
#Benchmarks
(a) 60 s timcout (unweighted).
300 timcout (unweighted).
Incomplete Scores (all)
Incomplete Scores (all)
0.8
0.6
LS-SGAT (0.8368)
0.6
LS SGAT (0.8306)
(0.7105)
(0.7686)
Sou (0.2507)
FourierSAT (0.2533)
0.2
0.0
0.0
50
150
200
50
150
200
WBecchaarks
Benchmarks
(c) 60 timeout (weighted).
(d) 300 timeout (weighted).
Figure 8: Cactus plots of continuous MaxSAT solvers. The r-axis shows the number of benchmark instances, and the y-axis shows the incomplete scores achieved. LS-SGAT and LS-GAT consistently outperform classical solvers such as FourierSAT, and this advantage holds across both unweighted and weighted benchmarks.
D.3 Cactus Plots of Continuous Solvers
Figures Sa 8b Sc and 8d present cactus plots that compare continuous MaxSAT solvers on both unweighted and weighted benchmarks. These results focus exclusively on continuous approaches such as LS-SGAT, LS-GAT, AT, MIXSAT, and Mixing. LS-SGAT consistently achieves the best performance across all settings, with LS-GAT also outperforming traditional baselines. These trends highlight the superior performance and robustness of SGAT-based methods continuous optimization frameworks for MaxSAT.
25

---

Trainalle Perametee Count SAT-GNN Models
483.441
Scalability Comparison of Models
COAR
Execution Time 15)
107
Size (MB)
10
(a) Scalability SGAT's on increasing problem sizes
SGAT
NeureSAT
GGW
MS-23FG
compared to neural-basse architectures.
(b) Parameter count comparison across architectures.
Figure 9: Comparison of SGAT scalability and parameter efficiency.
D.4
Scalability Analysis
Scaba hate
(a) Solved-rate vs. size (unweighted instances).
(b) Solved-rate vs. size (weighted instances).
Figure 10: Scalability analysis for continuous MaxSAT solvers based on the proportion instances solved within logarithmic size bins. A point 100 MB the y-axis means the solver succeeded on all test instances whose DIMACS file is between 64MB and 128MB. LS-SGAT retains a 100% solve ratio across every bin, while LS-GAT remains competitive up to 200MB. Classical continuous baselines AT, MIXSAT, Mixing) degrade sharply beyond few megabytes.
Figure 9 compares the scalability and parameter efficiency of SGATs with prior neural SAT solvers. The right subfigure shows that SGAT uses orders of magnitude fewer parameters compared to NeuroSAT, GGNN, and MS-ESFG (with only 898 parameters). This reflects the architectural simplicity of SGATs, which rely on fixed attention structures and minimal trainable components.
In contrast, prior models utilize deep multi-layer networks with complex gating or transformer-basee components, leading to parameter counts exceeding 400K. Even with orders-of-magnitude fewer parameters, the left subfigure shows that SGAT maintains superior scalability: execution time grows slowly with problem size, and SGAT is the only model that remains tractable on problems exceeding 100MB. Models like NeuroSAT and GGNN begin fail around 30MB, while MS-ESFG fails around 36MB.
These results highlight SGAT's suitability for large-scale SAT solving, where both inference speed and memory footprint are critical. By combining low parameter count with favorable runtime scaling, SGATs enable efficient reasoning on real-world datasets that challenge conventional architectures.
Figure 10 complements this view by showing the solved-rate curves: LS-SGAT maintains a near 100% solve ratio across every size bin, highlighting its robustness on very large weighted and unweighted instances, compared to continuous baselines like Fou MIXSAT, and Mixing.
26

---

Algorithm 4: Polarity-Majoricy Assignment
Input: CNF F (C.,.... Cm) with Cyyl = k; variables #1,..... In
Output: E {0,
// Count positive/negative occurrences per variable
for i 1, .....,,, do
pos; - 0, neg. +
end
for jorj=1, I...... m do
foreach literal & Cj do
f = 2, then pos; f pos; + if f 22 then neg, f- neg,
end end
// Assign by literal majority
10
for i = ,,..., do
pos, neg, then
12
4 6-
13
else
14
i4 <- 0
15
end
end
17 return 2
E Theoretical Analysis of SGATs
We show that a one-layer SGAT with fixed parameters realizes the polarit--maorrity assignment algorithm on unweighted Max-EASAT and therefore attains deterministic --approximation
Theorem 1 (Polarity-majority assignment achieves half-approximation Max-EkSAT), Let F (C Cm } be a k- CNF formula (every clause has exactly k literals). Then, the assignment produced by Algorithm 4 satisfies least m/2 clauses.
Proof. Give each literal weight that every clause carries total mass k. Let pos, and neg; be the positive and negative occurrence counts tracked by Algorithm { and define
W+ Σ (pos, neg.).
W Σ
(ios, neg.).
By construction W 2 W Moreover, for each variable Fy. the term max/pos,, neg, min(pos,, neg,) simplifies to pos; + neg, Summing over i therefore gives
W+ + w Σ (pos, + neg,) = mk;
because every clause contributes exactly h literal occurrences. For instance, if variable appears twice positively and once negatively, it contributes 1 = 3 units of weight in total, matching the three literals that mention it.
Let U be the number of unsatisfied clauses under the assignment returned by Algorithm In any
unsatisfied clause, each literal disagrees with the assignment on its variable. Since the algorithm picks the majority polarity for each variable, disagreeing literals belong to the minority side and therefore each contributes to W Consequently W > kU. Combining this with W+ 2 W and W+ W mkk yields
W W mk
AU S W <
so I m/2. Hence at least m 2 m/2 clauses are satisfied.
27

---

Theorem 2 (One-block SGAT realizes Algorithm 4. There exists SGATss with one SGAT block, Gödel
t-norm, one attention head, and hidden dimension d=1 (scalars on nodes), using fixed parameters, that produces exactly the assignment of Algorithm on any unweighted Max-EkSAT instance.
Proof. We employ the initializer module to output (x,) = for every variable. With the Gödel t-norm Tg computing clause valuations, each clause obtains vG(C,) 3.2 The SGAT update message m = 0 (z:) + (1 va (C)) therefore yields m 1 on positive literal edges and m on negative ones. Using a single attention head with all parameters set to zero makes the variable-side softmax uniform; with hidden dimension d-1, node features are scalars and the post-aggregation
valuation becomes (I,) pos,/ (pos; neg.). We then directly threshold (x;) at 1/2 to set x, iff pos, 2 neg, This matches Algorithm exactly.
E.1 Polarity-Majority Assignment (PMA) vs SGAT Predictions
To better understand how the Polarity-Majority Assignment (PMA) algorithm performs in comparison with the learned SGAT predictor, evaluated both the unweighted benchmark sets from MaxSAT evaluations (2020-2024). For each year we report: the win counts (how many problems each method achieved strictly higher clause satisfaction on), and the mean clause satisfaction across the test set for each method.
Table 6: Summary comparison between Polarity-Maoority Assignment (PMA) and learned SGAT predictions.
Metric
Solver
2020
2021
2022
2023
2024
PMA
0.7113
0.7025
0.5276
0.8032
0.7742
Clause satisfaction
SGAT
0.9216
0.9335
0.9230
0.9862
0.9910
PMA
0
0
Wins
SGAT
75
55
50
30
39
The results shown in Table iindicate that the learned SGAT predictor consistently outperforms the deterministic Polarity-Majorias Assignment (PMA) algorithm across all evaluated years, both in per-problem wins and clause satisfaction. PMA fails to win in any benchmarks in this comparison, underscoring our claim that SGATs can at least realize the PMA algorithm.
F
Limitations
While SGATs demonstrate strong empirical performance across multiple MaxSAT benchmarks, there several limitations that warrant discussion. First, our framework currently does not support partial MaxSAT, where some clauses must be satisfied (hard clauses). Extending SGAT's to explicitly distinguish and satisfy hard constraints remains an open challenge, particularly due to the soft nature of our t-norm-based loss formulation. Second, although SGATs generalize well across diverse datasets, their performance may still depend the diversity and representativennss of training instances. Handling highly domain-specific or adversarially structured formulas is not guaranteed. Lastly, while theoretical results do not cover weighted MaxSAT, they apply to general (non- (hon-partial) MaxSAT without clause weights. Extending these guarantees to handle weighted clauses or partial MaxSAT settings remains an open direction.
G Broader Impact
The proposed SGAT architecture introduces differentiable framework for MaxSAT solving, with potential implications in both academic and applied settings. On the positive side, SGATs provide a viable tool for integrating symbolic reasoning into neural systems, enabling end-to-end training for complex constraint-driver tasks. This could benefit domains such as autonomous driving and explainable AI, where the ability to make transparent, constraint-aware decisions is critical. In particular, our work contributes to the growing field of neuro-symbolic AI, which seeks to integrate symbolic reasoning with neural learning systems for improved interpretability and performance in
28

---

safety-critice environments. However, the integration of neural reasoning into maainng pipelines must be approached with caution. As our method does enforee global optimality or fair- ness constraints, its deployment in sensitive applications-suee as law, finance, or healthcare-shout be carefully monitored. Moreover, as with many machine learning systems, there is risk that SGATs inherit biases from their training data. Transparency and rigorous evaluation remain essential for safe use.
29


Reviews:
[{"review_id": "TpGh97uGGJ", "reviewer": "Reviewer_E9ST", "summary": "This paper introduces a new neural network for solving the (weighted) MaxSAT problem. Having converted a MaxSAT problem to an appropriate graph representation, the architecture consists of 3 parts: (i) T-norm Aggregation, (ii) SGAT layers, (iii) A normalization layer. The model is then be used in a local search framework to complete the approach. The authors include ablations to confirm their design choice of using SGAT (vs GAT) and the T-norm and for testing different T-norms. The authors provide results on two MaxSAT datasets, comparing the approach with previous SAT or MaxSAT architectures. Their model produces favorable results.", "questions": "Please refer to the strengths and weaknesses.", "limitations": "I think the limitations could be discussed in more detail - please see weaknesses.", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strengths\n* Favorable results when compared with existing neural network SAT solvers \n* Nice ablations\n\nWeaknesses\n* Contribution: Like several other papers in this direction of research (combinatorial optimization with neural networks), I feel this work does not convince me that using neural networks is necessary or even helpful here. The proposed approach aligns very closely with greedy distributed local search (as clearly stated by the authors - which I appreciate), and I am not sure what it contributes on top:\n* So firstly: CBLM and an appropriate greedy local search should be included as a baseline. The proposed model should outperform these baselines to justify itself. \n* Secondly: As far as I can tell with this approach there is not much transfer of knowledge between training and testing. Each problem instance essentially has to be solved separately. Perhaps the authors could elaborate on what knowledge they expect the model weights to be able to learn which can be transferred between problem instances. I would appreciate some intuition here to motivate the approach. To stress this point further, the update messages passed between nodes represent the value in which the clause wants the variable to be updated, rather than some more complex embeddings that somehow represent the structure/topology of the problem instance, which could be transferable between problem instances. I'm happy to receive pushback on this if the authors do not agree with my intuition. \n\nQuestions\n* Is the average clause satisfaction the standard metric here? I would have expected that the variables would be rounded (binarized) first, and then the (weighted) number of satisfied clauses calculated.", "was_revised": true, "final_justification": "My main concerns were resolved, hence the positive score.", "rebuttal": "We thank the reviewer for positive comments regarding our results and ablations, as well as for insightful comments and suggestions to improve our paper. We have carefully addressed the concerns raised in the review as follows:\n\n> [W1] The proposed approach aligns very closely with greedy distributed local search (as clearly stated by the authors - which I appreciate), and I am not sure what it contributes on top.\n\nOur model has been developed by aligning with greedy distributed local search, and based on it the proposed approach has come with a number of contributions and advantages:\n- **Novelty**: To learn solving MaxSAT problems, we employ a novel GNN with attention for greedy distributed local search, an approach that has never been proposed before in the literature. \n- **Performance**: As shown with multiple experiments, our model outperforms existing neural models, showing that it can effectively learn how to solve MaxSAT problems in general, as opposed to overfitting to a specific problem type. Furthermore, when used with our proposed local search algorithm, our model outperforms existing (non-neural) continuous optimization baselines, demonstrating our model's efficiency in continuous MaxSAT solving.\n- **Scalability**: Even though we were able to gain high performance, our model architecture is a still a fraction of the size of existing models (Appendix D.4). As scalability is generally a bottleneck within neuro-symbolic methods, our model can be effectively used in a variety of settings.\n\nWhile these are not the only advantages, we believe our proposed architecture contributes largely to multiple fields including neuro-symbolic, as well as MaxSAT solving.\n\n\n\n> [W2.1] CBLM should be included as a baseline.\n\nIn the table below, we show additional results that compare our pretrained model's one-shot output performance with the CBLM algorithm on MaxSAT Evaluation benchmark instances. As the CBLM algorithm only supports non-weighted instances, we have tested on all non-weighted instances from the MaxSAT Evaluation 2020 to 2024, as shown in Table 4. The table below shows the number of instances where each solver found better solutions than the other, with SGAT being used in a one-shot prediction setting.\n\nThe results show that our model finds better solutions than CBLM for _almost all (98%)_ instances. This demonstrates the superiority of our model architecture, empirically supporting our theoretical study regarding our model's capability of learning solving strategies.\nWe feel that this is a strong contribution of our work, and will make sure to include these results in the final version of the paper, if space allows.\n\n|Clause Satisfaction Win Count| 2020 | 2021 | 2022 | 2023 | 2024 | Total |\n|----------|------|------|------|------|------|------|\n| **CBLM** |   1  |   1  |   1  |  1   |  1   | 5   |\n| **SGAT** |  93  |  54  |  49  | 29   | 38   | 262 |\n\n\n\n> [W2.2] Greedy local search algorithms should be included as a baseline.\n\nDue to space constraints, we were not able to include full comparisons with state-of-the-art local search solvers in the main text. However,\nas shown in L306 and Appendix C, we have proposed to integrate our model as initialization heuristics for multiple state-of-the-art local search solvers, and compared them to the original solvers' initialization mechanisms. The results in table 3 shows that our proposed method outperforms the original, leading to state-of-the-art results on benchmark instances from 2020 to 2024.\nWe believe that this demonstrates the potential of our work and model in the broader context of MaxSAT solving.\n\n\n\n> [W3.1] As far as I can tell with this approach there is not much transfer of knowledge between training and testing. Each problem instance essentially has to be solved separately. Perhaps the authors could elaborate on what knowledge they expect the model weights to be able to learn which can be transferred between problem instances. I would appreciate some intuition here to motivate the approach.\n\nFirstly, we would like to clarify that our model is pretrained on dataset MS2018(2MB). Our algorithm then takes a copy of the pretrained model, and optimizes it to solve a specific problem instance, with no model parameters being shared between testing runs.\n\nDuring pretraining, the model learns in general what types of clauses the variables should focus on when solving any type of MaxSAT problem, and during testing, the model refines this knowledge to solve specific instances.\nIntuitively, we can regard this as learning a general heuristic that can be applied to a variety of MaxSAT problems, and then refining this heuristic to solve a specific problem instance.\n\nSpecifically, there are parameters within the model that requires learning, such as $\\mathbf{a}$, $\\mathbf{W}$ and $\\mathbf{W}_e$ shown in the equation at L180.\nThese parameters are used to compute the attention values, which in turn represents which clauses the variable should focus on satisfying.\nWe can regard the parameters as heuristics for performing greedy distributed local search.\n\nEmpirically, we have observed a significant decrease in performance when the model is used without pretraining, further supporting our claim that knowledge transfer is indeed present.\n\n> [W3.2] To stress this point further, the update messages passed between nodes represent the value in which the clause wants the variable to be updated, rather than some more complex embeddings that somehow represent the structure/topology of the problem instance, which could be transferable between problem instances.\n\nIn Graph Neural Networks (GNNs), the structure/toplogy of graphs gets represented as embeddings by the weights of the model. While our embeddings are in the form of fuzzy logic values, these too, get computed with the weights of the model. Thus, we believe that the structure/topology of the problem instance is indeed captured by our model, and that the embeddings are not simply just values for updating assignments.\n\n> [Q1] Is the average clause satisfaction the standard metric here? I would have expected that the variables would be rounded (binarized) first, and then the (weighted) number of satisfied clauses calculated.\n\nOur metric indeed agrees with the reviewer's expectation regarding how the clause satisfactions should be computed. In our current setting, we use Gödel t-norms to evaluate the satisfaction of each clause. In this case, rounding the clause values afterwards does not change the outcome to when the variables are binarized first. However, we now feel that the terminology of \"average clause satisfaction\" is misleading, and should be called \"(average) clause weight\", and so we will make sure to revise this in a final version of the paper."}, {"review_id": "PEU3bfyJOB", "reviewer": "Reviewer_xFG8", "summary": "The authors propose SGAT, a graph attention network architecture specifically designed to solve the MaxSAT problem, which is claimed to be the first GNNs to handle weighted MaxSAT problems. The technical contributions include the t-norm based attention and SGAT layer, an approximation of greedy distributed local search. SGAT is demonstrated to achieve better solutions compared with existing GNN models on MaxSAT problems from both randomly generated and competition benchmarks. Moreover, by integrating SGAT with a local search framework, the proposed algorithm outperforms other continuous optimisation algorithms in runtime on weighted MaxSAT Evaluation benchmarks.", "questions": "- Has a comparison been made with traditional discrete search solvers? If so, does SGAT-based local search have any advantages?\n- How was the choice made to have 6 SGAT blocks in the model, and what effects would setting more or fewer layers have on the results?\n- According to my knowledge, some weighted MaxSAT benchmarks in MaxSAT Evaluations have more than 100,000 variables. How can such large graphs be loaded onto the GPUs for training?", "limitations": "Yes", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "### Strengths\n- The proposed SGAT is novel and efficient, which is the first GNN model to work on weighted MaxSAT instances, a critical problem of various domains in CS&AI.\n- The t-norm attention and SGAT layer are well-motivated, and ablation studies have demonstrated their effectiveness and stability.\n- Experiments on MaxSAT Evaluation benchmarks are promising, which have shown the ability of NN-based approach on these challenging practical problems.\n- The manuscript is generally well-organised and easy to follow.\n\n### Weaknesses\n- Readers may find the term \"t-norm attention\" confusing, as it is not explained until Section 4.2. Explaining it when first mentioned would improve the clarity.\n- It should be clarified that Algorithm 1 can solve weighted MaxSAT instances to strengthen the contribution.\n- There is no meaningful conclusion from Section 4.6.", "was_revised": true, "final_justification": "Keep the score", "rebuttal": "We thank the reviewer for positive comments regarding the novelty and motivation of our SGAT model, as well as on our experimental results. We also thank the reviewer for suggestions to improve the clarity of our paper, and have carefully addressed the concerns raised in the review as follows:\n\n> [W1] Readers may find the term ”t-norm attention” confusing, as it is not explained until Section 4.2. Explaining it when first mentioned would improve the clarity.\n\nWhile we currently do have a brief explanation of how we incorporate t-norms and attention mechanisms in our model in L38, we agree that the term \"t-norm based attention\" may be confusing to the general reader.\nWe will make sure to clarify the connection, by rewriting the sentence at L38 to:\n\n\n\"SGATs are composed of GNN layers with novel t-norm based attention, which are attention mechanisms that operate on values computed using t-norms.\"\n\n\n> [W2] It should be clarified that Algorithm 1 can solve weighted MaxSAT instances to strengthen the contribution.\n\nWe thank the reviewer for pointing this out. We completely agree that this is a key contribution of our work to clarify, and will make sure to revise the paper to explicitly state that Algorithm 1 can be applied to weighted MaxSAT instances.\n\n\n> [W3] There is no meaningful conclusion from Section 4.6.\n\nDue to the limit in space, we were not able to include a detailed discussion of the theoretical results in Section 4.6, and thus most of the results are shown in Appendix E.\nIn this section, we have theoretically analyzed that our model has capabilities of learning a solving algorithm that can guarantee satisfying at least 1/2 of the maximum satisfiable clauses, which we believe to be meaningful.\nWe will make sure to revise the paper to include a brief discussion of the theoretical results in Section 4.6, and hope that this will help clarify the significance of our theoretical results.\n\n\n> [Q1] Has a comparison been made with traditional discrete search solvers? If so, does SGAT-based local search have any advantages?\n\nYes, we have made comparisons with traditional discrete search solvers.\nHowever, due to space constraints, we were not able to include full comparisons in the main text.\nAs shown in L306 and Appendix C, we have proposed to integrate our model as initialization heuristics for multiple state-of-the-art local search solvers, and compared them to the original solvers' initialization mechanisms.\nThe results in table 3 shows that our proposed method outperforms the original, achieving state-of-the-art results on benchmark instances from 2020 to 2024.\nThese results indicate that our model can be effectively used as heuristics for local search solvers, making it an interesting direction for future works as well.\n\n> [Q2] How was the choice made to have 6 SGAT blocks in the model, and what effects would setting more or fewer layers have on the results?\n\nIn our experiments, the number of blocks were decided empirically.\nWhile increasing the number of blocks lead to an increase in model performance during training, having large models will make the optimization procedure in Algorithm 1 take longer, as well as require more memory.\nAs this generally leads to degrading performance, we have decided to use 6 blocks, the setting that we found to be optimal.\n\n| Blocks | 1     | 2     | 3     | 4     | 5     | 6     | 7     | 8     | 9     | 10    |\n|--------|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|\n| Average Clause Satisfaction | 83.57 | 83.78 | 84.20 | 84.29 | 84.04 | 84.38 | 84.46 | 84.42 | 84.52 | 84.56 |\n\n\n> [Q3] According to my knowledge, some weighted MaxSAT benchmarks in MaxSAT Evaluations have more than 100,000 variables. How can such large graphs be loaded onto the GPUs for training?\n\nWe confirm that some instances have up to a million variables, and these huge instances are indeed not usable during training. Therefore, during our training phase, we only use instances that have file sizes below 2MB as stated in L243. Furthermore, for existing models, we set a batch size of 1, as larger batch sizes were not feasible even in this setting. In contrast, our model uses batch sizes of 4, which was possible due to the lightweight nature of our model, which we have discussed in Appendix D.4.\n\n> Formatting concerns of mixed citation formats, and dots in titles of sections where unnecessary.\n\nWe thank the reviewer for pointing out the formatting issues, and will make sure to address them in the final version of the paper if accepted."}, {"review_id": "uVCTFC5jvd", "reviewer": "Reviewer_2ENR", "summary": "The paper proposes a solver based on a graph neural network. The authors present the architecture and how the model is the use for solving MaxSAT problems. \n\nAfter the model and algorithm presentation the authors show the performance on standard MaxSAT instances and how the proposed approach works with ablation study on architecture choices.", "questions": "It isr elated to the weakeness point: would it be possible to define a different local search? Could you elaborate? there is part in the ANNEX that extend, could you spring something in the main text?\n\n\nIn algorithm 1 is not clear what \\alpha refers to, since there is the \\alpha of the attention, but this is not a scalar\n\nIn general, it is not clear what is learned and how it is learned. \n\nIt would also be nice to see where the approach is with respect to more mature solvers: \"MaxSAT Evaluation 2023: Summary of Unweighted Exact Track\"\n(https://maxsat-evaluations.github.io/2023/results/exact/unweighted/summary.html) or any other source.", "limitations": "yes, in the annex", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths \n1. clear presentation of the architecture and the separation of the role of the network and the algorithm\n2. Experiments that highlight the performance and the role of the architecture choices.  \n\nI personally like that the bipartite graph, the transformation from variable to clause is base on the T-norm. \n\nWeaknesses\n1. I would have like to see the analysis with other heuristics", "was_revised": true, "final_justification": "The authors left out some important information on the method (which parameters are trained in particular, and the distinction of the training and testing phases), but the approach is sound and the performance promising.\n\nI am keeping my score.", "rebuttal": "We thank the reviewer for positive comments regarding the novelty and motivation of our SGAT model, as well as on our experimental results. We also thank the reviewer for suggestions to improve the clarity of our paper, and have carefully addressed the concerns raised in the review as follows:\n\n> [W1] I would have liked to see analysis with other heuristics\n\nCurrently, we have already have done multiple comparisons with existing heuristics. Firstly, in L306, Appendix C, we have proposed to integrate our model as initialization heuristics for multiple state-of-the-art local search solvers, and compared them to the original solvers' initialization mechanisms.\nThe results in table 3 shows that our proposed method outperforms the original, leading to state-of-the-art results on benchmark instances from 2020 to 2024.\nThese results indicate that our model can be effectively used as heuristics for local search solvers, and even achieve state-of-the-art results on benchmark instances.\n\nFurthermore, we can regard the Mixing method as a heuristic. The MIXSAT solvers uses the Mixing method as a heuristic, performing branch-and-bound to find solutions for MaxSAT problems. As we had compared to this approach, we can essentially claim that our algorithm is being compared with existing heuristic methods, and outperforming them.\n\nIn terms of direct comparisons with algorithms, we have results comparing our model with the CBLM algorithm, a novel algorithm with theoretical guarantees that we show is learnable by the SGAT model (Appendix E). The results shown in the table below show how many instances each solver was able to satisfy more clauses than the other on, with SGATs being used in a one-shot prediction setting.\nThe results show that our model is able to outperform CBLM on almost all (98%) benchmark instances, demonstrating that our model is as good as CBLM in terms of learning to solve MaxSAT problems. \n\n|Clause Satisfaction Win Count| 2020 | 2021 | 2022 | 2023 | 2024 | Total |\n|----------|------|------|------|------|------|------|\n| **CBLM** |   1  |   1  |   1  |  1   |  1   | 5   |\n| **SGAT** |  92  |  54  |  49  | 29   | 38   | 262 |\n\n\nFinally, we feel that the comparison of our model with more prominent heuristics such as variable selection heuristics in local search algorithms are a promising direction for future work. We will make sure to include a brief discussion of this as future work, if accepted.\n\n\n> [Q1] It is related to the weakeness point: would it be possible to define a different local search? Could you elaborate? there is part in the ANNEX that extend, could you spring something in the main text?\n\nYes, a different local search algorithm to Algorithm 1 definitely can be defined on top of SGATs. One clear method is as initialization heuristics for existing solvers (Algorithm 2,3), as we have described in `[W1]`. While the reliance of SGATs in this method is lower, the positive results demonstrate its potential in various settings and algorithms.\nFurthermore, we feel that the development of such algorithms is a promising direction for future research, and so we will make sure to include a brief discussion of this in the final version of the paper, if accepted.\n\n\n> [Q2] In Algorithm 1, it is not clear what $\\alpha$ refers to, since there is the $\\alpha$ of the attention\n\nIn Algorithm 1, $\\alpha$ refers to the current assignment of the variables, a standard notation in the literature of MaxSAT solving. On the other hand, $\\alpha$ introduced in Section 3.2 refers to the attention values, which is also the standard notation used in works regarding attention for GNNs. However, we do agree that this may be confusing, and so we will make sure to either rename the variable in Algorithm 1 or Section 3.2, or clarify the notation when the variables are introduced.\n\n\n> [Q3] In general, it is not clear what is learned and how it is learned.\n\nDuring pretraining, the model learns in general what types of clauses the variables should focus on when solving any type of MaxSAT problem, and during testing, the model refines this knowledge to solve specific instances.\nIntuitively, we can regard this as learning a general heuristic that can be applied to a variety of MaxSAT problems, and then refining this heuristic to solve a specific problem instance.\n\nSpecifically, there are parameters within the model that requires learning, such as $\\mathbf{a}$, $\\mathbf{W}$ and $\\mathbf{W}_e$ shown in the equation at L180.\nThese parameters are used to compute the attention values, which in turn represents which clauses the variable should focus on satisfying.\nWe can regard the parameters as heuristics for performing greedy distributed local search.\n\nIn our model, the main parameters that get learned are the weights used in the attention mechanisms (such as $a$, $W$ and $W_e$ shown in the equation at L180).\nThese weights are used to compute the attention values, which in turn represents which clauses the variable should focus on satisfying. \nIntuitively, attention values represent the heuristics for greedy distributed local search that this model approximates, indicating that our model essentially learns heuristics for solving MaxSAT problems. \n\nAs for how we train, we first convert problems into graphs, then predict the assignment of the variables, and compute the loss based on the predicted assignment and the ground truth assignment. These are done on benchmark instances, as shown in Section 5.1.\n\n> [Q4] It would also be nice to see where the approach is with respect to more mature solvers: \"MaxSAT Evaluation 2023: Summary of Unweighted Exact Track\" (https://maxsat-evaluations.github.io/2023/results/exact/unweighted/summary.html), or any other source.\n\nAs stated in `[W1]` and `[Q1]`, our model has been integrated into state-of-the-art local search based MaxSAT solvers as initialization heuristics, where we achieved state-of-the-art on benchmark instances from 2020 to 2024 (Table 3). We feel that that similar integrations can be accomplished for exact solvers as well, and that this will have similar merits as the local search solvers. We will make sure to include a discussion of this in the final version of the paper, if accepted."}, {"review_id": "6Zz525Wd0x", "reviewer": "Reviewer_nviw", "summary": "This paper proposes SGAT, a novel Graph Neural Network architecture, designed specifically to address (Weighted) MaxSAT problems. SGAT incorporates a t-norm-based attention and message passing mechanism that approximates greedy distributed local search in a differentiable framework. The authors also introduce LS-GNN, a local search solver leveraging SGATs. The proposed method significantly outperforms existing GNN architectures and continuous optimisation baselines such as Mixing, MIXSAT, and FourierSAT on multiple MaxSAT benchmarks. Additional experiments demonstrate the importance of SGAT's components, and highlight its potential to provide high-quality initial assignments for integration with existing SOTA solvers.", "questions": "- In Algorithm 1, is the local search within the while loop executed in parallel? Is it possible to assign multiple random assignments to $\\alpha$ simultaneously, conduct local search in parallel, and then choose the one with the best cost? If the process executes with a single $\\alpha$, is parallelisation feasible, and could it lead to performance improvements?\n- In Figure 4, the test performance is generally better when models are trained on the synthetic dataset SR(U(40,200)) rather than the benchmark MS2018(2MB). This seems counter-intuitive. Could the authors provide an explanation for this phenomenon?\n- In the formula for Average Clause Satisfaction (Line 244), why is the round function applied to the clause satisfaction value? It seems possible to compute a meaningful average without rounding. What is the rationale for this choice?\n- In Table 1, some baseline solvers perform worse under a 300-second timeout than under a 60-second timeout in certain years. Could the authors explain why longer time limits would degrade performance in these cases?", "limitations": "The main limitations of this work are those already acknowledged by the authors. First, SGAT has not yet been extended to handle partial MaxSAT problems, where satisfying hard clauses is mandatory. Second, while the method shows strong performance on standard MaxSAT benchmarks, it has not been tested in broader neuro-symbolic reasoning tasks or real-world domains beyond SAT-style formulations. These limitations are rather natural next steps for future exploration. Given the flexibility of the proposed architecture and its compatibility with existing solvers, these extensions seem feasible and promising.", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 4, "significance": 4, "originality": 3, "strengths_and_weaknesses": "Strengths\n---\n- The definitions of the target problems (SAT, MaxSAT, Weighted MaxSAT) are clearly and precisely explained. The mathematical formulations provided throughout the paper are well-defined, making the paper highly readable and accessible.\n- The proposed GAT-based architecture, SGAT, is systematically well-structured and clearly explained. The roles of all variables in the equations are explicitly defined, and the message passing mechanism and optimisation objectives are well-formulated.\n- SGAT significantly outperforms baseline GNN architectures such as NeuroSAT, GGNN, and MS-ESFG in experimental results. Moreover, the LS-GNN algorithm, built on SGAT, exhibits superior performance compared to continuous MaxSAT solver baselines like Mixing, MIXSAT, and FourierSAT.\n- A well-constructed ablation study clearly shows that each component of SGAT (SGAT Layer, T-norm Layer, T-norm type) plays a crucial role in its high performance.\n- SGAT demonstrates practical utility when used as an initialisation heuristic for existing SOTA Weighted MaxSAT solvers. The experimental report suggests that integrating SGAT can improve solver performance, indicating the high potential of SGAT in real-world solver integration.\n\nWeaknesses\n---\n- In Algorithm 1 (LS-GNN), it is unclear how $\\Delta$ in Step 18 is defined. A brief explanation of \"early stopping\" variable would be appreciated. In the while loop, $\\alpha$ is repeatedly re-initialised with a random assignment in Step 4, and it remains unsure to me how the update in Step 18 is contributing to the process.\n- In Lines 224–225, the paper mentions an analysis of the approximation ratio of SGATs. It would be also appreciated to provide some concrete numbers or at least a summary (better or worse than prior methods) regarding this ratio, even if full theoretical guarantees are difficult.", "was_revised": true, "final_justification": "The rebuttal has effectively addressed most of my questions. The authors have clarified experimental concerns and ambiguities in the algorithm, and I am confident that these will be revised accordingly. I adjust the rating, and look forward to reading the updated version of the paper.", "rebuttal": "We thank the reviewer for positive comments regarding the novelty and motivation of our SGAT model, as well as strong experimental results. We also thank the reviewer for suggestions to improve the clarity of our paper, and have carefully addressed the concerns raised in the review as follows:\n\n\n> [W1.1] In Algorithm 1 (LS-GNN), it is unclear how $\\Delta$ in Step 18 is defined. Also, a brief explanation of \"early stopping\" variable would be appreciated.\n\nWe apologize for not being able to include a full explanation of the parameters associated with the algorithm in the main text due to space constraints.\nAs described in Appendix A.2, $\\Delta$ is a set of randomly generated values in the range $[0, 1]$, used to essentially replace (break) part of the current assignment with a random assignment.\nSimilarly, the early stopping variable is a parameter for deciding when to stop the continuous optimization process, and restart from a different assignment.\nWe will make sure to include brief explanations of these parameters in the main text, and hope that this will help clarify the algorithm.\n\n\n> [W1.2] In the while loop, $\\alpha$ is repeatedly re-initialised with a random assignment in Step 4, and it remains unsure to me how the update in Step 18 is contributing to the process.\n\nWe thank the reviewer for pointing out this issue. The random assignment of $\\alpha$ should only be done once before the while loop starts, i.e, before Step 2. We will make sure to revise the algorithm, and we apologize for the confusion caused by this mistake.\n\n\n> [W2] In Lines 224–225, the paper mentions an analysis of the approximation ratio of SGATs. It would be also appreciated to provide some concrete numbers or at least a summary (better or worse than prior methods) regarding this ratio, even if full theoretical guarantees are difficult.\n\nDue to the limit in space, we were not able to include a detailed discussion of the theoretical results in Section 4.6, and thus most of the results are shown in Appendix E.\nFrom our analysis, we have found that our model has capabilities of learning a solving algorithm that can guarantee satisfying at least 1/2 of the maximum satisfiable clauses. We will make sure to revise the paper to include the findings as well as a brief discussion of the theoretical results in Section 4.6, and hope that this will help clarify the significance of this result.\n\n\n> [Q1] In Algorithm 1, is the local search within the while loop executed in parallel? Is it possible to assign multiple random assignments to $\\alpha$ simultaneously, conduct local search in parallel, and then choose the one with the best cost? If the process executes with a single $\\alpha$, is parallelisation feasible, and could it lead to performance improvements?\n\nImplementation-wise, yes. We have already supported partial parallelization, by simply passing multiple instances of the problem and assignment batched together. \nHowever, as this requires a single model to find solutions from multiple different initial assignments, we have observed that there is a clear trade-off between efficiency and performance.\nNevertheless, this is a very under-explored area of our work, and we will make sure to include a discussion of this in the paper, as well as refer to this as future work on this topic.\n\n\n> [Q2] In Figure 4, the test performance is generally better when models are trained on the synthetic dataset SR(U(40,200)) rather than the benchmark MS2018(2MB). This seems counter-intuitive. Could the authors provide an explanation for this phenomenon?\n\nWe agree that this is an interesting phenomenon. We think that one reason for this occuring, is that the MS2018(2MB) dataset contains large instances, leading us to use a batch size of 1 during training for models other than SGATs. This leads to the model not being able to learn from multiple instances at once, degrading the overall performance of the model.\n\nAnother reason we think this occurs, is due to the variety of problem types provided in the MS2018(2MB) dataset. As the dataset contains a wide range of structured problem types (5 types to be exact), it becomes harder to train -- especially with single-instance batches. On the other hand, our model is very lightweight, and is capable of handling larger batch sizes. We feel that this is one main factor that leads to the performance of SGATs being better than existing models on both datasets as well.\n\n\n> [Q3] In the formula for Average Clause Satisfaction (Line 244), why is the round function applied to the clause satisfaction value? It seems possible to compute a meaningful average without rounding. What is the rationale for this choice?\n\nAs the reviewer has pointed out, it is possible to compute a meaningful average without rounding.\nHowever, in our setting, the purpose of rounding was to align the performance metric of models with how MaxSAT solvers are typically evaluated. \nAs our final goal is to find a solution that satisfies as many clauses as possible with regards to weight, the formula (L244) is designed to compute the average weights of all satisfied clauses.\n\n\n\n> [Q4] In Table 1, some baseline solvers perform worse under a 300-second timeout than under a 60-second timeout in certain years. Could the authors explain why longer time limits would degrade performance in these cases?\n\nThis is mainly due to how we evaluate the incomplete scores. The incomplete scores use the best scores found by all solvers, and thus if any of the other solvers in the same timeout set find a better solution, the other solvers' scores will worsen even if they had the exact same solution as before.\nHowever, we do agree that this may be confusing, and will make sure that the best scores are computed from all solvers regardless of timeout, so as to keep the scores comparable."}, {"review_id": "Olidh50MSb", "reviewer": "Reviewer_y3nh", "summary": "This paper presents SAT-based Graph Attention Networks (SGATs), a novel class of Graph Neural Networks (GNNs) designed to solve (weighted) MaxSAT problems via continuous optimization. SGATs integrate t-norm based attention and message-passing mechanisms to approximate greedy distributed local search. A local search solver, LS-GNN, is developed to leverage SGATs iteratively.", "questions": "1. Why were the ontinuous optimization baselines restricted to pre-2020 methods? Have more recent MaxSAT solvers been considered?\n\n2. While the ablation studies on MS2018 are informative, could the authors clarify whether similar analyses were attempted on more recent benchmarks? It would help understand whether the observed component-wise benefits generalize beyond the training domain.", "limitations": "Yes.", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths:\n\n+ The local search framework LS-GNN is simple yet effective, and fits naturally with the design of SGATs.\n+ The paper includes ablation studies and theoretical analysis (approximation ratio) that enhance its technical credibility.\n\nWeaknesses:\n\n+ The continuous optimization baselines (Mixing from 2019, MIXSAT from 2017, FourierSAT from 2020) are relatively outdated. The paper would be more convincing if compared against more recent local search-based MaxSAT solvers.\n+ While the proposed SGAT architecture is novel, the motivation for using GNNs over conventional solvers could be made more explicit.", "was_revised": true, "final_justification": "The authors have clarified my comments, so I maintain my positive rating.", "rebuttal": "We thank the reviewer for positive comments regarding the theoretical findings and simple algorithm, as well as suggestions for improving the clarity of our paper. We have carefully addressed the concerns raised in the review as follows:\n\n> [W1.1/Q1] The continuous optimization baselines (Mixing from 2019, MIXSAT from 2017, FourierSAT from 2020) are relatively outdated.\n\nRegarding the continuous optimization baselines, the solvers raised in the paper are the related works that we were able to find open source implementations for.\nAs for FourierSAT, newer versions were presented more recently, but we opted to use the original version as we found that newer implementations were not adaptable to the weighted MaxSAT setting. As having support for weighted MaxSAT is extremely important for performing comparisons, we have opted to use the original FourierSAT solver, the only version that supports weighted MaxSAT.\n\n\n> [W1.2/Q1] The paper would be more convincing if compared against more recent local search-based MaxSAT solvers.\n\nDue to the limit in space, we were not able to include full comparisons with state-of-the-art local search solvers in the main text.\nHowever, as stated in L306 and Appendix C, we have investigated the effect of using SGATs as initialization heuristics for state-of-the-art incomplete MaxSAT solvers. The results in Table 3 show that we constantly outperform the variant without heuristics, achieving state-of-the-art results on benchmark instances from 2020 to 2024, even with the overhead of producing SGAT predictions. These results highlight the power of SGATs in providing high-quality approximations for MaxSAT problems, and we feel that this is a key contribution of our work.\n\n\n> [W2] While the proposed SGAT architecture is novel, the motivation for using GNNs over conventional solvers could be made more explicit.\n\nCurrently, our main goal is to provide methods that complement conventional solvers, and not to replace them. We state below two motivating reasons behind the use of GNNs (or neural networks in general):\n\n1. **As heuristics**: While there exists highly tuned solvers that can solve MaxSAT problems efficiently, these solvers often rely on the use of heuristics that require expert knowledge. In such scenarios, neural models such as SGATs can be used to provide heuristics for performance increase, effectively reducing the cost of hand crafting these heuristics. \n1. **For neuro-symbolic integration**: In the field of neuro-symbolic research, there is a general need for symbolic solvers that align well with continuous outputs of neural models. Solving models like ours could be used in such situations, making it crucial towards developing high performing models that align well with solvers.\n\nLastly, as shown by many existing works, SAT problems can be naturally represented as graphs (as shown in Figure 6), supporting our choice of using GNNs over ordinary neural networks for MaxSAT. This choice is further supported in many of SAT related works, which have also shown GNNs to be effective as heuristics, supporting our first point above.\n\n\n\n\n> [Q2] While the ablation studies on MS2018 are informative, could the authors clarify whether similar analyses were attempted on more recent benchmarks? It would help understand whether the observed component-wise benefits generalize beyond the training domain.\n\nYes. From our analysis, we have observed that our model does indeed perform similarly on more recent benchmarks, when performing similar ablation studies. While there are differences in the overall clause satisfaction, the tendency of the results closely match those shown in Figure 5, ensuring that the model performs well regardless of the dataset used."}]

Author rebuttal:

Meta-review: The submission introduces a GNN architecture for differentiable MaxSAT solving, incorporating t-norm–based attention mechanisms and message passing inspired by greedy distributed local search. A key original contribution is the design of a GNN that could be applied effectively to weighted MaxSAT.

The reviewers unanimously supported acceptance. The contributions were seen as both novel and technically sound, and the results compelling. SGATs outperform several neural and continuous optimization baselines across standard MaxSAT benchmarks, and show excellent performance when integrated into state-of-the-art local search solvers. Reviewers highlighted the clarity of the problem formulation, the soundness of the SGAT architecture, and the practical utility of using SGATs as initialization heuristics for existing solvers.

The rebuttal was effective in addressing all key concerns, including a clearer explanation of the learning process and heuristic used. Important points such as notation ambiguity, missing runtime baselines, and theoretical insights on approximation were also clarified or promised to be revised.

Reviewers encourage the authors to include missing technical details,  which had been omitted in the original version but discussed extensively in rebuttal discussion, in the final version.

I recommend to accept this paper.
Decision: Accept (spotlight)