Attn-JGNN: Attention Enhanced Join-Graph Neural Networks

TL;DR

Attn-JGNN tackles #SAT model counting by marrying IJGP-inspired join-graph propagation with a hierarchical attention mechanism over clusters from tree decomposition. The method uses two Graph Attention Network layers and an MLP to learn partition-function estimates, enabling efficient, approximate inference of log-counts. Key contributions include a per-cluster attention design that reduces complexity to O(k w^2), a dynamic head mechanism for training efficiency, and a constraint-aware loss to bias toward satisfiable clauses. Experimental results on BIRD and SATLIB show Attn-JGNN outperforming neural baselines and remaining competitive with state-of-the-art solvers, highlighting practical impact for scalable probabilistic inference on CNF formulas.

Abstract

We propose an Attention Enhanced Join-Graph Neural Networks(Attn-JGNN) model for solving #SAT problems, which significantly improves the solving accuracy. Inspired by the Iterative Join Graph Propagation (IJGP) algorithm, Attn-JGNN uses tree decomposition to encode the CNF formula into a join-graph, then performs iterative message passing on the join-graph, and finally approximates the model number by learning partition functions. In order to further improve the accuracy of the solution, we apply the attention mechanism in and between clusters of the join-graphs, which makes Attn-JGNN pay more attention to the key variables and clusters in probabilistic inference, and reduces the redundant calculation. Finally, our experiments show that our Attn-JGNN model achieves better results than other neural network methods.

Figures (3)

• Figure 1: For the #SAT problem, our model uses two Graph Attention Network (GAT) layers for message passing and a Multi-Layer Perceptron (MLP) layer to estimate the partition function, serving as an approximate solver. A pooling layer compresses the processed variable and clause node features into a global representation, which is fed into the MLP layer.
• Figure 2: In the picture A,B,C... representing variables(Clause nodes are hidden, and clause nodes cannot appear on edges),the shared variables between the two clusters act as edge-lable. the same factor graph can be decomposed into different tree decomposition forms, figure (a) shows a low tree width but with poor accuracy, while figure (b) shows a high tree width, featuring high complexity but high accuracy
• Figure 3: (a) is RMSE between estimated log countings and ground truth for each solver on the BIRD benchmark;(b) is Scatter plot comparing the estimated log countings against the ground truth for each solver on the BIRD benchmark