# SATformer: Transformer-Based UNSAT Core Learning

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

## Key facts

- Cited by 14 papers in the map (data through 14 Oct 2026).
- Builds on 13 of its 41 references that are in the map.
- First posted on arXiv 2 Sep 2022.

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

- [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)
- [An Image is Worth 16x16 Words: Transformers for Image Recognition at Scale](https://mlsanity.com/paper/2010.11929/) (2020)
- [Swin Transformer: Hierarchical Vision Transformer using Shifted Windows](https://mlsanity.com/paper/2103.14030/) (2021)
- [Feature Pyramid Networks for Object Detection](https://mlsanity.com/paper/1612.03144/) (2016)
- [Learning Deep Transformer Models for Machine Translation](https://mlsanity.com/paper/1906.01787/) (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)
- [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)
- [Machine Learning Methods in Solving the Boolean Satisfiability Problem](https://mlsanity.com/paper/2203.04755/) (2022)
- [ReadNet: A Hierarchical Transformer Framework for Web Article Readability Analysis](https://mlsanity.com/paper/2103.04083/) (2021)
- [Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis](https://mlsanity.com/paper/2107.07116/) (2021)

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

- [A Comprehensive Survey on Applications of Transformers for Deep Learning Tasks](https://mlsanity.com/paper/2306.07303/) (2023)
- [G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks](https://mlsanity.com/paper/2309.16941/) (2023)
- [Can Transformers Reason Logically? A Study in SAT Solving](https://mlsanity.com/paper/2410.07432/) (2024)
- [DiLA: Enhancing LLM Tool Learning with Differential Logic Layer](https://mlsanity.com/paper/2402.11903/) (2024)
- [Can Language Models Pretend Solvers? Logic Code Simulation with LLMs](https://mlsanity.com/paper/2403.16097/) (2024)
- [Benchmarking Graph Neural Networks in Solving Hard Constraint Satisfaction Problems](https://mlsanity.com/paper/2602.18419/) (2026)
- [Recursive Inference Machines for Neural Reasoning](https://mlsanity.com/paper/2603.05234/) (2026)
- [MILP-SAT-GNN: Yet Another Neural SAT Solver](https://mlsanity.com/paper/2507.01825/) (2025)
- [TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System](https://mlsanity.com/paper/2511.07737/) (2025)
- [On the Expressive Power of GNNs for Boolean Satisfiability](https://mlsanity.com/paper/2602.08745/) (2026)
- [Learning to Rank the Initial Branching Order of SAT Solvers](https://mlsanity.com/paper/2603.07176/) (2026)
- [Boolean Satisfiability via Imitation Learning](https://mlsanity.com/paper/2509.25411/) (2025)
- [GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra](https://mlsanity.com/paper/2603.28796/) (2026)
- [Unsat Core Prediction through Polarity-Aware Representation Learning over Clause-Literal Hypergraphs](https://mlsanity.com/paper/2605.04819/) (2026)

## Abstract (arXiv)

This paper introduces SATformer, a novel Transformer-based approach for the Boolean Satisfiability (SAT) problem. Rather than solving the problem directly, SATformer approaches the problem from the opposite direction by focusing on unsatisfiability. Specifically, it models clause interactions to identify any unsatisfiable sub-problems. Using a graph neural network, we convert clauses into clause embeddings and employ a hierarchical Transformer-based model to understand clause correlation. SATformer is trained through a multi-task learning approach, using the single-bit satisfiability result and the minimal unsatisfiable core (MUC) for UNSAT problems as clause supervision. As an end-to-end learning-based satisfiability classifier, the performance of SATformer surpasses that of NeuroSAT significantly. Furthermore, we integrate the clause predictions made by SATformer into modern heuristic-based SAT solvers and validate our approach with a logic equivalence checking task. Experimental results show that our SATformer can decrease the runtime of existing solvers by an average of 21.33%.