# Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis

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

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 32 references that are in the map.
- First posted on arXiv 15 Jul 2021.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Graph Attention Networks](https://mlsanity.com/paper/1710.10903/) (2017)
- [Layer Normalization](https://mlsanity.com/paper/1607.06450/) (2016)
- [Fast Graph Representation Learning with PyTorch Geometric](https://mlsanity.com/paper/1903.02428/) (2019)
- [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)
- [PDP: A General Neural Framework for Learning Constraint Satisfaction Solvers](https://mlsanity.com/paper/1903.01969/) (2019)

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

- [A Comprehensive Survey on Applications of Transformers for Deep Learning Tasks](https://mlsanity.com/paper/2306.07303/) (2023)
- [Linear algebra with transformers](https://mlsanity.com/paper/2112.01898/) (2021)
- [Learning the greatest common divisor: explaining transformer predictions](https://mlsanity.com/paper/2308.15594/) (2023)
- [SALSA: Attacking Lattice Cryptography with Transformers](https://mlsanity.com/paper/2207.04785/) (2022)
- [SATformer: Transformer-Based UNSAT Core Learning](https://mlsanity.com/paper/2209.00953/) (2022)
- [Addressing Variable Dependency in GNN-based SAT Solving](https://mlsanity.com/paper/2304.08738/) (2023)
- [Studying number theory with deep learning: a case study with the M"obius and squarefree indicator functions](https://mlsanity.com/paper/2502.10335/) (2025)
- [Can Transformers Learn to Verify During Backtracking Search?](https://mlsanity.com/paper/2605.22221/) (2026)
- [Learning Linear Temporal Specifications from Demonstrations with Uncertainty](https://mlsanity.com/paper/2607.10918/) (2026)

## Abstract (arXiv)

CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. The increasing popularity of these constraint problems in electronic design automation encourages studies on different SAT problems and their properties for further computational efficiency. There has been both theoretical and practical success of modern Conflict-driven clause learning SAT solvers, which allows solving very large industrial instances in a relatively short amount of time. Recently, machine learning approaches provide a new dimension to solving this challenging problem. Neural symbolic models could serve as generic solvers that can be specialized for specific domains based on data without any changes to the structure of the model. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem, which is the optimization version of SAT where the goal is to satisfy the maximum number of clauses. Our model has a scale-free structure which could process varying size of instances. We use meta-path and self-attention mechanism to capture interactions among homogeneous nodes. We adopt cross-attention mechanisms on the bipartite graph to capture interactions among heterogeneous nodes. We further apply an iterative algorithm to our model to satisfy additional clauses, enabling a solution approaching that of an exact-SAT problem. The attention mechanisms leverage the parallelism for speedup. Our evaluation indicates improved speedup compared to heuristic approaches and improved completion rate compared to machine learning approaches.