# Using deep learning to construct stochastic local search SAT solvers with performance bounds

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 14 of its 64 references that are in the map.
- First posted on arXiv 20 Sep 2023.

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

- [Layer Normalization](https://mlsanity.com/paper/1607.06450/) (2016)
- [Relational inductive biases, deep learning, and graph networks](https://mlsanity.com/paper/1806.01261/) (2018)
- [Interaction Networks for Learning about Objects, Relations and Physics](https://mlsanity.com/paper/1612.00222/) (2016)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Solving Mixed Integer Programs Using Neural Networks](https://mlsanity.com/paper/2012.13349/) (2020)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [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)
- [NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks](https://mlsanity.com/paper/2110.14053/) (2021)
- [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)
- [Neural heuristics for SAT solving](https://mlsanity.com/paper/2005.13406/) (2020)
- [On preparing ground states of gapped Hamiltonians: An efficient Quantum Lov'asz Local Lemma](https://mlsanity.com/paper/1611.08571/) (2016)

## Abstract (arXiv)

The Boolean Satisfiability problem (SAT), as the prototypical mathsfNP-complete problem, is crucial in both theoretical computer science and practical applications. To address this problem, stochastic local search (SLS) algorithms, which iteratively and randomly update candidate assignments, present an important and theoretically well-studied class of solvers. Recent theoretical advancements have identified conditions under which SLS solvers efficiently solve SAT instances, provided they have access to suitable ``oracles'', i.e., instance-specific distribution samples. We propose leveraging machine learning models, particularly graph neural networks (GNN), as oracles to enhance the performance of SLS solvers. Our approach, evaluated on random and pseudo-industrial SAT instances, demonstrates a significant performance improvement regarding step counts and solved instances. Our work bridges theoretical results and practical applications, highlighting the potential of purpose-trained SAT solvers with performance guarantees.