Planted-solution SAT and Ising benchmarks from integer factorization
Provides scalable, verifiable benchmarks for SAT and Ising solvers, addressing the need for structured test instances with known ground truth.
The paper introduces a family of planted-solution SAT and Ising benchmarks derived from integer factorization, where the number of carry contractions scales as O(d^4) for d-bit primes. Empirical results show median SAT solver runtime grows exponentially with factor bit-length.
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 \times 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 $d^4$. 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.