# DeepSAT: An EDA-Driven Learning Framework for SAT

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

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 29 references that are in the map.
- First posted on arXiv 27 May 2022.

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

- [Prototypical Networks for Few-shot Learning](https://mlsanity.com/paper/1703.05175/) (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)
- [Conditional Image Generation with PixelCNN Decoders](https://mlsanity.com/paper/1606.05328/) (2016)
- [Learning Combinatorial Optimization Algorithms over Graphs](https://mlsanity.com/paper/1704.01665/) (2017)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Directed Acyclic Graph Neural Networks](https://mlsanity.com/paper/2101.07965/) (2021)
- [Graph Neural Network Guided Local Search for the Traveling Salesperson Problem](https://mlsanity.com/paper/2110.05291/) (2021)
- [DeepGate: Learning Neural Representations of Logic Gates](https://mlsanity.com/paper/2111.14616/) (2021)
- [NLocalSAT: Boosting Local Search with Solution Prediction](https://mlsanity.com/paper/2001.09398/) (2020)
- [Augment with Care: Contrastive Learning for Combinatorial Problems](https://mlsanity.com/paper/2202.08396/) (2022)
- [Implementing Efficient All Solutions SAT Solvers](https://mlsanity.com/paper/1510.00523/) (2015)

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

- [DeepGate3: Towards Scalable Circuit Representation Learning](https://mlsanity.com/paper/2407.11095/) (2024)
- [G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks](https://mlsanity.com/paper/2309.16941/) (2023)
- [Autonomous Code Evolution Meets NP-Completeness](https://mlsanity.com/paper/2509.07367/) (2025)
- [DeepGate4: Efficient and Effective Representation Learning for Circuit Design at Scale](https://mlsanity.com/paper/2502.01681/) (2025)
- [DeepSeq2: Enhanced Sequential Circuit Learning with Disentangled Representations](https://mlsanity.com/paper/2411.00530/) (2024)
- [General Method for Solving Four Types of SAT Problems](https://mlsanity.com/paper/2312.16423/) (2023)
- [MILP-SAT-GNN: Yet Another Neural SAT Solver](https://mlsanity.com/paper/2507.01825/) (2025)
- [TRACE: Learning to Compute on Circuit Graphs](https://mlsanity.com/paper/2509.21886/) (2025)
- [Unsat Core Prediction through Polarity-Aware Representation Learning over Clause-Literal Hypergraphs](https://mlsanity.com/paper/2605.04819/) (2026)
- [Beyond Flat Netlist: Hierarchical Graph Representation Learning for Scalable Analysis of Sequential Circuits](https://mlsanity.com/paper/2608.28188/) (2026)
- [LevelSyn: Physical-Aware Logic Synthesis via Level-Asynchronous Graph Neural Networks](https://mlsanity.com/paper/2609.03594/) (2026)

## Abstract (arXiv)

We present DeepSAT, a novel end-to-end learning framework for the Boolean satisfiability (SAT) problem. Unlike existing solutions trained on random SAT instances with relatively weak supervision, we propose applying the knowledge of the well-developed electronic design automation (EDA) field for SAT solving. Specifically, we first resort to logic synthesis algorithms to pre-process SAT instances into optimized and-inverter graphs (AIGs). By doing so, the distribution diversity among various SAT instances can be dramatically reduced, which facilitates improving the generalization capability of the learned model. Next, we regard the distribution of SAT solutions being a product of conditional Bernoulli distributions. Based on this observation, we approximate the SAT solving procedure with a conditional generative model, leveraging a novel directed acyclic graph neural network (DAGNN) with two polarity prototypes for conditional SAT modeling. To effectively train the generative model, with the help of logic simulation tools, we obtain the probabilities of nodes in the AIG being logic `1' as rich supervision. We conduct comprehensive experiments on various SAT problems. Our results show that, DeepSAT achieves significant accuracy improvements over state-of-the-art learning-based SAT solutions, especially when generalized to SAT instances that are relatively large or with diverse distributions.