Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2604.09837 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915931831140352 |
|---|---|
| author | Hen, Itay |
| author_facet | Hen, Itay |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_09837 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Planted-solution SAT and Ising benchmarks from integer factorization Hen, Itay Quantum Physics Logic in Computer Science 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. |
| title | Planted-solution SAT and Ising benchmarks from integer factorization |
| topic | Quantum Physics Logic in Computer Science |
| url | https://arxiv.org/abs/2604.09837 |