# Arbitrarily Large Labelled Random Satisfiability Formulas for Machine Learning Training

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 41 references that are in the map.
- First posted on arXiv 21 Nov 2022.

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

- [XGBoost: A Scalable Tree Boosting System](https://mlsanity.com/paper/1603.02754/) (2016)
- [TabNet: Attentive Interpretable Tabular Learning](https://mlsanity.com/paper/1908.07442/) (2019)
- [Machine Learning for Combinatorial Optimization: a Methodological Tour d'Horizon](https://mlsanity.com/paper/1811.06128/) (2018)
- [CatBoost: gradient boosting with categorical features support](https://mlsanity.com/paper/1810.11363/) (2018)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [FLAML: A Fast and Lightweight AutoML Library](https://mlsanity.com/paper/1911.04706/) (2019)
- [catch22: CAnonical Time-series CHaracteristics](https://mlsanity.com/paper/1901.10200/) (2019)
- [Deep Models of Interactions Across Sets](https://mlsanity.com/paper/1803.02879/) (2018)
- [A Bayesian Approach to Tackling Hard Computational Problems](https://mlsanity.com/paper/1301.2279/) (2013)

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

- [Benchmarking Graph Neural Networks in Solving Hard Constraint Satisfaction Problems](https://mlsanity.com/paper/2602.18419/) (2026)

## Abstract (arXiv)

Applying deep learning to solve real-life instances of hard combinatorial problems has tremendous potential. Research in this direction has focused on the Boolean satisfiability (SAT) problem, both because of its theoretical centrality and practical importance. A major roadblock faced, though, is that training sets are restricted to random formulas of size several orders of magnitude smaller than formulas of practical interest, raising serious concerns about generalization. This is because labeling random formulas of increasing size rapidly becomes intractable. By exploiting the probabilistic method in a fundamental way, we remove this roadblock entirely: we show how to generate correctly labeled random formulas of any desired size, without having to solve the underlying decision problem. Moreover, the difficulty of the classification task for the formulas produced by our generator is tunable by varying a simple scalar parameter. This opens up an entirely new level of sophistication for the machine learning methods that can be brought to bear on Satisfiability. Using our generator, we train existing state-of-the-art models for the task of predicting satisfiability on formulas with 10,000 variables. We find that they do no better than random guessing. As a first indication of what can be achieved with the new generator, we present a novel classifier that performs significantly better than random guessing 99% on the same datasets, for most difficulty levels. Crucially, unlike past approaches that learn based on syntactic features of a formula, our classifier performs its learning on a short prefix of a solver's computation, an approach that we expect to be of independent interest.