# Machine Learning for SAT: Restricted Heuristics and New Graph Representations

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 13 of its 37 references that are in the map.
- First posted on arXiv 18 Jul 2023.

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

- [Playing Atari with Deep Reinforcement Learning](https://mlsanity.com/paper/1312.5602/) (2013)
- [Deep Reinforcement Learning with Double Q-learning](https://mlsanity.com/paper/1509.06461/) (2015)
- [Relational inductive biases, deep learning, and graph networks](https://mlsanity.com/paper/1806.01261/) (2018)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [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)
- [Enhancing SAT solvers with glue variable predictions](https://mlsanity.com/paper/2007.02559/) (2020)
- [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)
- [Can Graph Neural Networks Learn to Solve MaxSAT Problem?](https://mlsanity.com/paper/2111.07568/) (2021)
- [Adaptive Restart and CEGAR-based Solver for Inverting Cryptographic Hash Functions](https://mlsanity.com/paper/1608.04720/) (2016)
- [From Gameplay to Symbolic Reasoning: Learning SAT Solver Heuristics in the Style of Alpha(Go) Zero](https://mlsanity.com/paper/1802.05340/) (2018)

## Abstract (arXiv)

Boolean satisfiability (SAT) is a fundamental NP-complete problem with many applications, including automated planning and scheduling. To solve large instances, SAT solvers have to rely on heuristics, e.g., choosing a branching variable in DPLL and CDCL solvers. Such heuristics can be improved with machine learning (ML) models; they can reduce the number of steps but usually hinder the running time because useful models are relatively large and slow. We suggest the strategy of making a few initial steps with a trained ML model and then releasing control to classical heuristics; this simplifies cold start for SAT solving and can decrease both the number of steps and overall runtime, but requires a separate decision of when to release control to the solver. Moreover, we introduce a modification of Graph-Q-SAT tailored to SAT problems converted from other domains, e.g., open shop scheduling problems. We validate the feasibility of our approach with random and industrial SAT problems.