# Self-Satisfied: An end-to-end framework for SAT generation and prediction

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 18 of its 38 references that are in the map.
- First posted on arXiv 18 Oct 2024.

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

- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [An Image is Worth 16x16 Words: Transformers for Image Recognition at Scale](https://mlsanity.com/paper/2010.11929/) (2020)
- [Feature Pyramid Networks for Object Detection](https://mlsanity.com/paper/1612.03144/) (2016)
- [Pyramid Scene Parsing Network](https://mlsanity.com/paper/1612.01105/) (2016)
- [Pyramid Vision Transformer: A Versatile Backbone for Dense Prediction without Convolutions](https://mlsanity.com/paper/2102.12122/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Rethinking Spatial Dimensions of Vision Transformers](https://mlsanity.com/paper/2103.16302/) (2021)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Funnel-Transformer: Filtering out Sequential Redundancy for Efficient Language Processing](https://mlsanity.com/paper/2006.03236/) (2020)
- [Scalable Vision Transformers with Hierarchical Pooling](https://mlsanity.com/paper/2103.10619/) (2021)
- [Length-Adaptive Transformer: Train Once with Length Drop, Use Anytime with Search](https://mlsanity.com/paper/2010.07003/) (2020)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [Pooling Methods in Deep Neural Networks, a Review](https://mlsanity.com/paper/2009.07485/) (2020)
- [TR-BERT: Dynamic Token Reduction for Accelerating BERT Inference](https://mlsanity.com/paper/2105.11618/) (2021)
- [Centroid Transformers: Learning to Abstract with Attention](https://mlsanity.com/paper/2102.08606/) (2021)
- [Pyramid-BERT: Reducing Complexity via Successive Core-set based Token Selection](https://mlsanity.com/paper/2203.14380/) (2022)
- [Sparsifying Transformer Models with Trainable Representation Pooling](https://mlsanity.com/paper/2009.05169/) (2020)
- [W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs](https://mlsanity.com/paper/2302.00272/) (2023)

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

- [Target-Aware Data Augmentation for SAT Prediction](https://mlsanity.com/paper/2605.06931/) (2026)

## Abstract (arXiv)

The boolean satisfiability (SAT) problem asks whether there exists an assignment of boolean values to the variables of an arbitrary boolean formula making the formula evaluate to True. It is well-known that all NP-problems can be coded as SAT problems and therefore SAT is important both practically and theoretically. From both of these perspectives, better understanding the patterns and structure implicit in SAT data is of significant value. In this paper, we describe several advances that we believe will help open the door to such understanding: we introduce hardware accelerated algorithms for fast SAT problem generation, a geometric SAT encoding that enables the use of transformer architectures typically applied to vision tasks, and a simple yet effective technique we term head slicing for reducing sequence length representation inside transformer architectures. These advances allow us to scale our approach to SAT problems with thousands of variables and tens of thousands of clauses. We validate our architecture, termed Satisfiability Transformer (SaT), on the SAT prediction task with data from the SAT Competition (SATComp) 2022 problem sets. Prior related work either leveraged a pure machine learning approach, but could not handle SATComp-sized problems, or was hybrid in the sense of integrating a machine learning component in a standard SAT solving tool. Our pure machine learning approach achieves prediction accuracies comparable to recent work, but on problems that are an order of magnitude larger than previously demonstrated. A fundamental aspect of our work concerns the very nature of SAT data and its suitability for training machine learning models. We both describe experimental results that probe the landscape of where SAT data can be successfully used for learning and position these results within the broader context of complexity and learning.