# NSNet: A General Neural Probabilistic Framework for Satisfiability Problems

arXiv: https://arxiv.org/abs/2211.03880 · HTML: https://mlsanity.com/paper/2211.03880/

## Key facts

- Cited by 18 papers in the map (data through 14 Oct 2026).
- Builds on 18 of its 50 references that are in the map.
- First posted on arXiv 7 Nov 2022.

## Builds on (most cited first, 18 of 18)

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Fast Graph Representation Learning with PyTorch Geometric](https://mlsanity.com/paper/1903.02428/) (2019)
- [Gated Graph Sequence Neural Networks](https://mlsanity.com/paper/1511.05493/) (2015)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [Neural Enhanced Belief Propagation on Factor Graphs](https://mlsanity.com/paper/2003.01998/) (2020)
- [Inference in Probabilistic Graphical Models by Graph Neural Networks](https://mlsanity.com/paper/1803.07710/) (2018)
- [Belief Propagation Neural Networks](https://mlsanity.com/paper/2007.00295/) (2020)
- [Goal-Aware Neural SAT Solver](https://mlsanity.com/paper/2106.07162/) (2021)
- [NLocalSAT: Boosting Local Search with Solution Prediction](https://mlsanity.com/paper/2001.09398/) (2020)
- [Machine Learning Methods in Solving the Boolean Satisfiability Problem](https://mlsanity.com/paper/2203.04755/) (2022)
- [A Scalable Approximate Model Counter](https://mlsanity.com/paper/1306.5726/) (2013)
- [PDP: A General Neural Framework for Learning Constraint Satisfaction Solvers](https://mlsanity.com/paper/1903.01969/) (2019)
- [Learning Branching Heuristics for Propositional Model Counting](https://mlsanity.com/paper/2007.03204/) (2020)
- [Neural heuristics for SAT solving](https://mlsanity.com/paper/2005.13406/) (2020)
- [Implementing Efficient All Solutions SAT Solvers](https://mlsanity.com/paper/1510.00523/) (2015)
- [Equivariant Neural Network for Factor Graphs](https://mlsanity.com/paper/2109.14218/) (2021)

## Built on by (most cited first, 18 of 18)

- [G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks](https://mlsanity.com/paper/2309.16941/) (2023)
- [AutoSAT: Automatically Optimize SAT Solvers via Large Language Models](https://mlsanity.com/paper/2402.10705/) (2024)
- [DISCO: Efficient Diffusion Solver for Large-Scale Combinatorial Optimization Problems](https://mlsanity.com/paper/2406.19705/) (2024)
- [A Unified Framework for Combinatorial Optimization Based on Graph Neural Networks](https://mlsanity.com/paper/2406.13125/) (2024)
- [torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem](https://mlsanity.com/paper/2402.03640/) (2024)
- [Graph Pruning for Enumeration of Minimal Unsatisfiable Subsets](https://mlsanity.com/paper/2402.15524/) (2024)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [Unrealized Expectations: Comparing AI Methods vs Classical Algorithms for Maximum Independent Set](https://mlsanity.com/paper/2502.03669/) (2025)
- [Gradient-Based Optimization on G"odel Logic as Discrete Local Search](https://mlsanity.com/paper/2503.01817/) (2025)
- [Neural Approaches to SAT Solving: Design Choices and Interpretability](https://mlsanity.com/paper/2504.01173/) (2025)
- [Generalizable Reasoning through Compositional Energy Minimization](https://mlsanity.com/paper/2510.20607/) (2025)
- [Benchmarking Graph Neural Networks in Solving Hard Constraint Satisfaction Problems](https://mlsanity.com/paper/2602.18419/) (2026)
- [Structure based SAT dataset for analysing GNN generalisation](https://mlsanity.com/paper/2502.11410/) (2025)
- [MILP-SAT-GNN: Yet Another Neural SAT Solver](https://mlsanity.com/paper/2507.01825/) (2025)
- [Attn-JGNN: Attention Enhanced Join-Graph Neural Networks](https://mlsanity.com/paper/2510.15583/) (2025)
- [Hypergraph Neural Networks Accelerate MUS Enumeration](https://mlsanity.com/paper/2604.09001/) (2026)
- [Unsat Core Prediction through Polarity-Aware Representation Learning over Clause-Literal Hypergraphs](https://mlsanity.com/paper/2605.04819/) (2026)
- [Convex Compositional Reasoning Models](https://mlsanity.com/paper/2605.23395/) (2026)

## Abstract (arXiv)

We present the Neural Satisfiability Network (NSNet), a general neural framework that models satisfiability problems as probabilistic inference and meanwhile exhibits proper explainability. Inspired by the Belief Propagation (BP), NSNet uses a novel graph neural network (GNN) to parameterize BP in the latent space, where its hidden representations maintain the same probabilistic interpretation as BP. NSNet can be flexibly configured to solve both SAT and #SAT problems by applying different learning objectives. For SAT, instead of directly predicting a satisfying assignment, NSNet performs marginal inference among all satisfying solutions, which we empirically find is more feasible for neural networks to learn. With the estimated marginals, a satisfying assignment can be efficiently generated by rounding and executing a stochastic local search. For #SAT, NSNet performs approximate model counting by learning the Bethe approximation of the partition function. Our evaluations show that NSNet achieves competitive results in terms of inference accuracy and time efficiency on multiple SAT and #SAT datasets.