# Machine Learning Methods in Solving the Boolean Satisfiability Problem

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

## Key facts

- Cited by 22 papers in the map (data through 14 Oct 2026).
- Builds on 22 of its 114 references that are in the map.
- First posted on arXiv 2 Mar 2022.

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

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Inductive Representation Learning on Large Graphs](https://mlsanity.com/paper/1706.02216/) (2017)
- [Graph Neural Networks: A Review of Methods and Applications](https://mlsanity.com/paper/1812.08434/) (2018)
- [Pointer Networks](https://mlsanity.com/paper/1506.03134/) (2015)
- [Link Prediction Based on Graph Neural Networks](https://mlsanity.com/paper/1802.09691/) (2018)
- [Machine Learning for Combinatorial Optimization: a Methodological Tour d'Horizon](https://mlsanity.com/paper/1811.06128/) (2018)
- [Learning Combinatorial Optimization Algorithms over Graphs](https://mlsanity.com/paper/1704.01665/) (2017)
- [A Critical Review of Recurrent Neural Networks for Sequence Learning](https://mlsanity.com/paper/1506.00019/) (2015)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Deep Models of Interactions Across Sets](https://mlsanity.com/paper/1803.02879/) (2018)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [On Joint Learning for Solving Placement and Routing in Chip Design](https://mlsanity.com/paper/2111.00234/) (2021)
- [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)
- [G2SAT: Learning to Generate SAT Formulas](https://mlsanity.com/paper/1910.13445/) (2019)
- [Symbolic Logic meets Machine Learning: A Brief Survey in Infinite Domains](https://mlsanity.com/paper/2006.08480/) (2020)
- [Enhancing SAT solvers with glue variable predictions](https://mlsanity.com/paper/2007.02559/) (2020)
- [Graph Neural Networks and Boolean Satisfiability](https://mlsanity.com/paper/1702.03592/) (2017)
- [The Resolution of Keller's Conjecture](https://mlsanity.com/paper/1910.03740/) (2019)
- [Neural heuristics for SAT solving](https://mlsanity.com/paper/2005.13406/) (2020)
- [Improve SAT-solving with Machine Learning](https://mlsanity.com/paper/1710.11204/) (2017)

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

- [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)
- [LinSATNet: The Positive Linear Satisfiability Neural Networks](https://mlsanity.com/paper/2407.13917/) (2024)
- [SATformer: Transformer-Based UNSAT Core Learning](https://mlsanity.com/paper/2209.00953/) (2022)
- [HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline](https://mlsanity.com/paper/2302.02104/) (2023)
- [Machine Learning Insides OptVerse AI Solver: Design Principles and Applications](https://mlsanity.com/paper/2401.05960/) (2024)
- [Circuit Transformer: A Transformer That Preserves Logical Equivalence](https://mlsanity.com/paper/2403.13838/) (2024)
- [GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection](https://mlsanity.com/paper/2405.11024/) (2024)
- [W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs](https://mlsanity.com/paper/2302.00272/) (2023)
- [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)
- [Structure based SAT dataset for analysing GNN generalisation](https://mlsanity.com/paper/2502.11410/) (2025)
- [HyperSAT: Unsupervised Hypergraph Neural Networks for Weighted MaxSAT Problems](https://mlsanity.com/paper/2504.11885/) (2025)
- [MILP-SAT-GNN: Yet Another Neural SAT Solver](https://mlsanity.com/paper/2507.01825/) (2025)
- [TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System](https://mlsanity.com/paper/2511.07737/) (2025)
- [BDD2Seq: Enabling Scalable Reversible-Circuit Synthesis via Graph-to-Sequence Learning](https://mlsanity.com/paper/2511.08315/) (2025)
- [On the Expressive Power of GNNs for Boolean Satisfiability](https://mlsanity.com/paper/2602.08745/) (2026)
- [Learning Interpretable Heuristics for WalkSAT](https://mlsanity.com/paper/2307.04608/) (2023)
- [Automatic Algorithm Selection for Pseudo-Boolean Optimization with Given Computational Time Limits](https://mlsanity.com/paper/2309.03924/) (2023)
- [Using deep learning to construct stochastic local search SAT solvers with performance bounds](https://mlsanity.com/paper/2309.11452/) (2023)
- [A Novel Differentiable Loss Function for Unsupervised Graph Neural Networks in Graph Partitioning](https://mlsanity.com/paper/2312.06877/) (2023)
- [Hypergraph Neural Networks Accelerate MUS Enumeration](https://mlsanity.com/paper/2604.09001/) (2026)

## Abstract (arXiv)

This paper reviews the recent literature on solving the Boolean satisfiability problem (SAT), an archetypal NP-complete problem, with the help of machine learning techniques. Despite the great success of modern SAT solvers to solve large industrial instances, the design of handcrafted heuristics is time-consuming and empirical. Under the circumstances, the flexible and expressive machine learning methods provide a proper alternative to solve this long-standing problem. We examine the evolving ML-SAT solvers from naive classifiers with handcrafted features to the emerging end-to-end SAT solvers such as NeuroSAT, as well as recent progress on combinations of existing CDCL and local search solvers with machine learning methods. Overall, solving SAT with machine learning is a promising yet challenging research topic. We conclude the limitations of current works and suggest possible future directions.