# Guiding High-Performance SAT Solvers with Unsat-Core Predictions

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

## Key facts

- Cited by 62 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 Mar 2019.

## Built on by (most cited first, 30 of 62)

- [Combinatorial optimization and reasoning with graph neural networks](https://mlsanity.com/paper/2102.09544/) (2021)
- [Machine Learning for Electronic Design Automation: A Survey](https://mlsanity.com/paper/2102.03357/) (2021)
- [LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning](https://mlsanity.com/paper/2101.06223/) (2021)
- [Generalization of Neural Combinatorial Solvers Through the Lens of Adversarial Robustness](https://mlsanity.com/paper/2110.10942/) (2021)
- [Explaining the Explainers in Graph Neural Networks: a Comparative Study](https://mlsanity.com/paper/2210.15304/) (2022)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)
- [Goal-Aware Neural SAT Solver](https://mlsanity.com/paper/2106.07162/) (2021)
- [Augment with Care: Contrastive Learning for Combinatorial Problems](https://mlsanity.com/paper/2202.08396/) (2022)
- [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)
- [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)
- [Neural Circuit Synthesis from Specification Patterns](https://mlsanity.com/paper/2107.11864/) (2021)
- [AutoSAT: Automatically Optimize SAT Solvers via Large Language Models](https://mlsanity.com/paper/2402.10705/) (2024)
- [SATformer: Transformer-Based UNSAT Core Learning](https://mlsanity.com/paper/2209.00953/) (2022)
- [Are Graph Neural Networks Optimal Approximation Algorithms?](https://mlsanity.com/paper/2310.00526/) (2023)
- [Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis](https://mlsanity.com/paper/2107.07116/) (2021)
- [SeaPearl: A Constraint Programming Solver guided by Reinforcement Learning](https://mlsanity.com/paper/2102.09193/) (2021)
- [Generating Symbolic Reasoning Problems with Transformer GANs](https://mlsanity.com/paper/2110.10054/) (2021)
- [Can Graph Neural Networks Learn to Solve MaxSAT Problem?](https://mlsanity.com/paper/2111.07568/) (2021)
- [Learning to Configure Computer Networks with Neural Algorithmic Reasoning](https://mlsanity.com/paper/2211.01980/) (2022)
- [CoProver: A Recommender System for Proof Construction](https://mlsanity.com/paper/2304.10486/) (2023)
- [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)
- [Denoising Diffusion for Sampling SAT Solutions](https://mlsanity.com/paper/2212.00121/) (2022)
- [General Method for Solving Four Types of SAT Problems](https://mlsanity.com/paper/2312.16423/) (2023)
- [Towards graph neural networks for provably solving convex optimization problems](https://mlsanity.com/paper/2502.02446/) (2025)
- [Learning from Algorithm Feedback: One-Shot SAT Solver Guidance with GNNs](https://mlsanity.com/paper/2505.16053/) (2025)
- [Navigating by Old Maps: The Pitfalls of Static Mechanistic Localization in LLM Post-Training](https://mlsanity.com/paper/2605.06076/) (2026)
- [UNSAT Solver Synthesis via Monte Carlo Forest Search](https://mlsanity.com/paper/2211.12581/) (2022)

## Abstract (arXiv)

The NeuroSAT neural network architecture was recently introduced for predicting properties of propositional formulae. When trained to predict the satisfiability of toy problems, it was shown to find solutions and unsatisfiable cores on its own. However, the authors saw "no obvious path" to using the architecture to improve the state-of-the-art. In this work, we train a simplified NeuroSAT architecture to directly predict the unsatisfiable cores of real problems. We modify several high-performance SAT solvers to periodically replace their variable activity scores with NeuroSAT's prediction of how likely the variables are to appear in an unsatisfiable core. The modified MiniSat solves 10% more problems on SAT-COMP 2018 within the standard 5,000 second timeout than the original does. The modified Glucose solves 11% more problems than the original, while the modified Z3 solves 6% more. The gains are even greater when the training is specialized for a specific distribution of problems; on a benchmark of hard problems from a scheduling domain, the modified Glucose solves 20% more problems than the original does within a one-hour timeout. Our results demonstrate that NeuroSAT can provide effective guidance to high-performance SAT solvers on real problems.