# Goal-Aware Neural SAT Solver

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

## Key facts

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

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

- [Machine Learning for Combinatorial Optimization: a Methodological Tour d'Horizon](https://mlsanity.com/paper/1811.06128/) (2018)
- [Learning to learn by gradient descent by gradient descent](https://mlsanity.com/paper/1606.04474/) (2016)
- [PairNorm: Tackling Oversmoothing in GNNs](https://mlsanity.com/paper/1909.12223/) (2019)
- [AdaBelief Optimizer: Adapting Stepsizes by the Belief in Observed Gradients](https://mlsanity.com/paper/2010.07468/) (2020)
- [Combinatorial optimization and reasoning with graph neural networks](https://mlsanity.com/paper/2102.09544/) (2021)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Recurrent Relational Networks](https://mlsanity.com/paper/1711.08028/) (2017)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [CLN2INV: Learning Loop Invariants with Continuous Logic Networks](https://mlsanity.com/paper/1909.11542/) (2019)
- [PDP: A General Neural Framework for Learning Constraint Satisfaction Solvers](https://mlsanity.com/paper/1903.01969/) (2019)
- [FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints](https://mlsanity.com/paper/1912.01032/) (2019)
- [Can Q-Learning with Graph Networks Learn a Generalizable Branching Heuristic for a SAT Solver?](https://mlsanity.com/paper/1909.11830/) (2019)
- [NNgSAT: Neural Network guided SAT Attack on Logic Locked Complex Structures](https://mlsanity.com/paper/2009.02208/) (2020)
- [Graph Neural Reasoning May Fail in Certifying Boolean Unsatisfiability](https://mlsanity.com/paper/1909.11588/) (2019)

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

- [Machine Learning Methods in Solving the Boolean Satisfiability Problem](https://mlsanity.com/paper/2203.04755/) (2022)
- [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)
- [Are Graph Neural Networks Optimal Approximation Algorithms?](https://mlsanity.com/paper/2310.00526/) (2023)
- [Self-Supervised Transformers as Iterative Solution Improvers for Constraint Satisfaction](https://mlsanity.com/paper/2502.15794/) (2025)
- [Generating Symbolic Reasoning Problems with Transformer GANs](https://mlsanity.com/paper/2110.10054/) (2021)
- [Denoising Diffusion for Sampling SAT Solutions](https://mlsanity.com/paper/2212.00121/) (2022)
- [Geometric Algorithms for Neural Combinatorial Optimization with Constraints](https://mlsanity.com/paper/2510.24039/) (2025)
- [Addressing Variable Dependency in GNN-based SAT Solving](https://mlsanity.com/paper/2304.08738/) (2023)
- [Neural Approaches to SAT Solving: Design Choices and Interpretability](https://mlsanity.com/paper/2504.01173/) (2025)
- [Learning to Decode in Parallel: Self-Coordinating Neural Network for Real-Time Quantum Error Correction](https://mlsanity.com/paper/2601.09921/) (2026)
- [Benchmarking Graph Neural Networks in Solving Hard Constraint Satisfaction Problems](https://mlsanity.com/paper/2602.18419/) (2026)
- [Discrete Denoising Diffusion Approach to Integer Factorization](https://mlsanity.com/paper/2309.05295/) (2023)
- [Learning Better Representations From Less Data For Propositional Satisfiability](https://mlsanity.com/paper/2402.08365/) (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)
- [On the Expressive Power of GNNs for Boolean Satisfiability](https://mlsanity.com/paper/2602.08745/) (2026)
- [Machine Learning for SAT: Restricted Heuristics and New Graph Representations](https://mlsanity.com/paper/2307.09141/) (2023)
- [Using deep learning to construct stochastic local search SAT solvers with performance bounds](https://mlsanity.com/paper/2309.11452/) (2023)
- [A short review on the maximum clique problem algorithms with classical, AI, and quantum methods](https://mlsanity.com/paper/2403.09742/) (2024)
- [A Geometric Perspective on the Difficulties of Learning GNN-based SAT Solvers](https://mlsanity.com/paper/2508.21513/) (2025)
- [Attn-JGNN: Attention Enhanced Join-Graph Neural Networks](https://mlsanity.com/paper/2510.15583/) (2025)
- [Target-Aware Data Augmentation for SAT Prediction](https://mlsanity.com/paper/2605.06931/) (2026)
- [Tiny Recursive Message Passing](https://mlsanity.com/paper/2610.18649/) (2026)

## Abstract (arXiv)

Modern neural networks obtain information about the problem and calculate the output solely from the input values. We argue that it is not always optimal, and the network's performance can be significantly improved by augmenting it with a query mechanism that allows the network at run time to make several solution trials and get feedback on the loss value on each trial. To demonstrate the capabilities of the query mechanism, we formulate an unsupervised (not depending on labels) loss function for Boolean Satisfiability Problem (SAT) and theoretically show that it allows the network to extract rich information about the problem. We then propose a neural SAT solver with a query mechanism called QuerySAT and show that it outperforms the neural baseline on a wide range of SAT tasks.