# NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks

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

## Key facts

- Cited by 19 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 51 references that are in the map.
- First posted on arXiv 26 Oct 2021.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [An Image is Worth 16x16 Words: Transformers for Image Recognition at Scale](https://mlsanity.com/paper/2010.11929/) (2020)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Graph Attention Networks](https://mlsanity.com/paper/1710.10903/) (2017)
- [Inductive Representation Learning on Large Graphs](https://mlsanity.com/paper/1706.02216/) (2017)
- [Layer Normalization](https://mlsanity.com/paper/1607.06450/) (2016)
- [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)
- [A Comprehensive Survey on Graph Neural Networks](https://mlsanity.com/paper/1901.00596/) (2019)
- [Fast Graph Representation Learning with PyTorch Geometric](https://mlsanity.com/paper/1903.02428/) (2019)
- [Graph Neural Networks: A Review of Methods and Applications](https://mlsanity.com/paper/1812.08434/) (2018)
- [Relational inductive biases, deep learning, and graph networks](https://mlsanity.com/paper/1806.01261/) (2018)
- [A Comprehensive Survey on Transfer Learning](https://mlsanity.com/paper/1911.02685/) (2019)
- [Measuring and Relieving the Over-smoothing Problem for Graph Neural Networks from the Topological View](https://mlsanity.com/paper/1909.03211/) (2019)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [GraphiT: Encoding Graph Structure in Transformers](https://mlsanity.com/paper/2106.05667/) (2021)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [The Model Counting Competition 2020](https://mlsanity.com/paper/2012.01323/) (2020)
- [Enhancing SAT solvers with glue variable predictions](https://mlsanity.com/paper/2007.02559/) (2020)
- [Can Q-Learning with Graph Networks Learn a Generalizable Branching Heuristic for a SAT Solver?](https://mlsanity.com/paper/1909.11830/) (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, 19 of 19)

- [AutoSAT: Automatically Optimize SAT Solvers via Large Language Models](https://mlsanity.com/paper/2402.10705/) (2024)
- [Circuit Transformer: A Transformer That Preserves Logical Equivalence](https://mlsanity.com/paper/2403.13838/) (2024)
- [Benchmarking Graph Neural Networks in Solving Hard Constraint Satisfaction Problems](https://mlsanity.com/paper/2602.18419/) (2026)
- [Learning Better Representations From Less Data For Propositional Satisfiability](https://mlsanity.com/paper/2402.08365/) (2024)
- [Clone-Robust Weights in Metric Spaces: Handling Redundancy Bias for Benchmark Aggregation](https://mlsanity.com/paper/2502.03576/) (2025)
- [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)
- [TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System](https://mlsanity.com/paper/2511.07737/) (2025)
- [On the Expressive Power of GNNs for Boolean Satisfiability](https://mlsanity.com/paper/2602.08745/) (2026)
- [Learning to Rank the Initial Branching Order of SAT Solvers](https://mlsanity.com/paper/2603.07176/) (2026)
- [Using deep learning to construct stochastic local search SAT solvers with performance bounds](https://mlsanity.com/paper/2309.11452/) (2023)
- [Boolean Satisfiability via Imitation Learning](https://mlsanity.com/paper/2509.25411/) (2025)
- [MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering](https://mlsanity.com/paper/2603.04450/) (2026)
- [Hypergraph Neural Networks Accelerate MUS Enumeration](https://mlsanity.com/paper/2604.09001/) (2026)
- [Transfer Learning from Foundational Optimization Embeddings to Unsupervised SAT Representations](https://mlsanity.com/paper/2604.15448/) (2026)
- [Unsat Core Prediction through Polarity-Aware Representation Learning over Clause-Literal Hypergraphs](https://mlsanity.com/paper/2605.04819/) (2026)
- [Target-Aware Data Augmentation for SAT Prediction](https://mlsanity.com/paper/2605.06931/) (2026)
- [Anatomy of a Sound Neural Reasoner: One-Shot Amortization, First-Pass Poisoning, and Search Inertness in Clue-Rich Completion](https://mlsanity.com/paper/2607.19635/) (2026)
- [Verifying Neural Networks with Reinforcement Learning](https://mlsanity.com/paper/2609.34553/) (2026)

## Abstract (arXiv)

Propositional satisfiability (SAT) is an NP-complete problem that impacts many research fields, such as planning, verification, and security. Mainstream modern SAT solvers are based on the Conflict-Driven Clause Learning (CDCL) algorithm. Recent work aimed to enhance CDCL SAT solvers using Graph Neural Networks (GNNs). However, so far this approach either has not made solving more effective, or required substantial GPU resources for frequent online model inferences. Aiming to make GNN improvements practical, this paper proposes an approach called NeuroBack, which builds on two insights: (1) predicting phases (i.e., values) of variables appearing in the majority (or even all) of the satisfying assignments are essential for CDCL SAT solving, and (2) it is sufficient to query the neural model only once for the predictions before the SAT solving starts. Once trained, the offline model inference allows NeuroBack to execute exclusively on the CPU, removing its reliance on GPU resources. To train NeuroBack, a new dataset called DataBack containing 120,286 data samples is created. NeuroBack is implemented as an enhancement to a state-of-the-art SAT solver called Kissat. As a result, it allowed Kissat to solve up to 5.2% and 7.4% more problems on two recent SAT competition problem sets, SATCOMP-2022 and SATCOMP-2023, respectively. NeuroBack therefore shows how machine learning can be harnessed to improve SAT solving in an effective and practical manner.