# Planted-solution SAT and Ising benchmarks from integer factorization

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Apr 2026.

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

- [Implicit Binarization via Complex Phase Dynamics in Combinatorial Optimization](https://mlsanity.com/paper/2605.24502/) (2026)

## Abstract (arXiv)

We present a family of planted-solution benchmark instances for satisfiability (SAT) solvers and Ising optimization derived from integer factorization. Given two primes p and q, the construction encodes the arithmetic constraints of N = p × q as a conjunctive normal form (CNF) formula whose satisfying assignments correspond to valid factorizations of~N. The known pair (p,q) serves as a built-in ground truth, enabling unambiguous verification of solver output. We show that for two d-bit primes the total number of carry contractions is on the order of d4. Empirical benchmarks with SAT solvers show that median runtime grows exponentially in the bit-length of the factors over the range tested. The construction provides a scalable, structured, and verifiable benchmark family controlled by a single parameter, accompanied by open-source generation software.