# MILP-SAT-GNN: Yet Another Neural SAT Solver

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 25 of its 45 references that are in the map.
- First posted on arXiv 2 Jul 2025.

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

- [How Powerful are Graph Neural Networks?](https://mlsanity.com/paper/1810.00826/) (2018)
- [Neural Message Passing for Quantum Chemistry](https://mlsanity.com/paper/1704.01212/) (2017)
- [Weisfeiler and Leman Go Neural: Higher-order Graph Neural Networks](https://mlsanity.com/paper/1810.02244/) (2018)
- [Neural Probabilistic Logic Programming in DeepProbLog](https://mlsanity.com/paper/1907.08194/) (2019)
- [Exact Combinatorial Optimization with Graph Convolutional Neural Networks](https://mlsanity.com/paper/1906.01629/) (2019)
- [What graph neural networks cannot learn: depth vs width](https://mlsanity.com/paper/1907.03199/) (2019)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [The Surprising Power of Graph Neural Networks with Random Node Initialization](https://mlsanity.com/paper/2010.01179/) (2020)
- [Random Features Strengthen Graph Neural Networks](https://mlsanity.com/paper/2002.03155/) (2020)
- [Weisfeiler and Leman go Machine Learning: The Story so far](https://mlsanity.com/paper/2112.09992/) (2021)
- [The Logic of Graph Neural Networks](https://mlsanity.com/paper/2104.14624/) (2021)
- [From Statistical Relational to Neurosymbolic Artificial Intelligence: a Survey](https://mlsanity.com/paper/2108.11451/) (2021)
- [A Comprehensive Survey on Deep Graph Representation Learning](https://mlsanity.com/paper/2304.05055/) (2023)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [A Survey for Solving Mixed Integer Programming via Machine Learning](https://mlsanity.com/paper/2203.02878/) (2022)
- [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)
- [On Representing Mixed-Integer Linear Programs by Graph Neural Networks](https://mlsanity.com/paper/2210.10759/) (2022)
- [Machine Learning Methods in Solving the Boolean Satisfiability Problem](https://mlsanity.com/paper/2203.04755/) (2022)
- [The Power of the Weisfeiler-Leman Algorithm for Machine Learning with Graphs](https://mlsanity.com/paper/2105.05911/) (2021)
- [NSNet: A General Neural Probabilistic Framework for Satisfiability Problems](https://mlsanity.com/paper/2211.03880/) (2022)
- [G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks](https://mlsanity.com/paper/2309.16941/) (2023)
- [SATformer: Transformer-Based UNSAT Core Learning](https://mlsanity.com/paper/2209.00953/) (2022)
- [DeepSAT: An EDA-Driven Learning Framework for SAT](https://mlsanity.com/paper/2205.13745/) (2022)
- [Declarative Probabilistic Logic Programming in Discrete-Continuous Domains](https://mlsanity.com/paper/2302.10674/) (2023)

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

- [Target-Aware Data Augmentation for SAT Prediction](https://mlsanity.com/paper/2605.06931/) (2026)

## Abstract (arXiv)

We proposes a novel method that enables Graph Neural Networks (GNNs) to solve SAT problems by leveraging a technique developed for applying GNNs to Mixed Integer Linear Programming (MILP). Specifically, k-CNF formulae are mapped into MILP problems, which are then encoded as weighted bipartite graphs and subsequently fed into a GNN for training and testing. From a theoretical perspective: (i) we establish permutation and equivalence invariance results, demonstrating that the method produces outputs that are stable under reordering of clauses and variables; (ii) we identify a theoretical limitation, showing that for a class of formulae called foldable formulae, standard GNNs cannot always distinguish satisfiable from unsatisfiable instances; (iii) we prove a universal approximation theorem, establishing that with Random Node Initialization (RNI), the method can approximate SAT solving to arbitrary precision on finite datasets, that is, the GNN becomes approximately sound and complete on such datasets. Furthermore, we show that for unfoldable formulae, the same approximation guarantee can be achieved without the need for RNI. Finally, we conduct an experimental evaluation of our approach, which show that, despite the simplicity of the neural architecture, the method achieves promising results.