Planted-solution SAT and Ising benchmarks from integer factorization

• URL: http://arxiv.org/abs/2604.09837v1
• Date: Fri, 10 Apr 2026 19:09:24 GMT
• Title: Planted-solution SAT and Ising benchmarks from integer factorization
• Abstract summary: Given two primes $p$ and $q$, the construction encodes the arithmetic constraints of $N = p times q$ as a conjunctive normal form (CNF) formula.<n>We show that for two $d$-bit primes the total number of carry contractions is on the order of $d4$.<n>The construction provides a scalable, structured, and verifiable benchmark family controlled by a single parameter, accompanied by open-source generation software.
• Score: 0.06768558752130309
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• A Sharp Barrier for Consistent Submodular Maximization: Any Improvement over $2-\sqrt{2}$ Entails Exponential Queries or Linear Recourse [50.69285844345291]
  We study tradeoff between solution quality and stability when elements arrive over time.<n>Our algorithm has a future implementation for rational oracle$ with $O(varepsilon-1)$ recourse and separate the existence of universal-price certificates from their efficient algorithms.
  arXiv  Detail & Related papers  (2026-09-09T10:13:43Z)
• SSTQ:Privacy-Preserving Vector Quantization via Subsampled Stochastic TurboQuant [79.24089819400126]
  Subsampled TurboQuant (SSTQ) is a framework that combines overcomplete equal-width tight frames, coordinate subsampling, and privacy-aware quantization.<n>SSTQ achieves mean squared error scaling while using only $lceil log N il + b$ bits per client, where $N = (d)$ is the frame size.<n>We also derive a surrogate privacy-aware codebook objective that reduces the codebook-dependent MSE scaling from $O(4b)$ to $O(2b)$.
  arXiv  Detail & Related papers  (2026-08-05T17:51:25Z)
• Orthologic for SAT Solving [0.0]
  We introduce a family of synthetic SAT benchmarks based on the observation that, for any formula $$, the equivalence $leftrightarrow mathrmNF_mathrmOL()$ is a tautology.<n>We show that using orthologic normalization as a preprocessing step can improve SAT solving time on some hard problems.
  arXiv  Detail & Related papers  (2026-05-14T13:05:57Z)
• Fault-Tolerant Resource Comparison of Qudit and Qubit Encodings for Diagonal Quadratic Operators [36.94429692322632]
  Finite local Hilbert-space truncations arise naturally in quantum simulations of lattice field theories and motivate qudit encodings.<n>We compare the non-Clifford cost of implementing diagonal evolutions, exemplified by $U=e-it_x2$ in a uniform field-amplitude discretization of a real scalar field, using either one logical $d$-level qudit or $n_b=eil log drceil$ logical qubits.
  arXiv  Detail & Related papers  (2026-04-29T15:25:08Z)
• Quantum Algorithms for Gowers Norm Estimation, Polynomial Testing, and Arithmetic Progression Counting over Finite Abelian Groups [0.0]
  We propose a family of quantum algorithms for estimating Gowers norms $ Uk $ over finite abelian groups.<n>These algorithms leverage recent inverse theorems for Gowers norms, together with amplitude estimation, to reveal higher-order correlations.
  arXiv  Detail & Related papers  (2025-08-02T06:58:12Z)
• Provable Scaling Laws for the Test-Time Compute of Large Language Models [84.00141420901038]
  We propose two algorithms that enjoy provable scaling laws for the test-time compute of large language models.<n>One is a two-stage knockout-style algorithm, where each candidate is evaluated by its average win rate against multiple opponents.<n>The other is a two-stage league-style algorithm, where each candidate is evaluated by its average win rate against multiple opponents.
  arXiv  Detail & Related papers  (2024-11-29T05:29:47Z)
• Obtaining Lower Query Complexities through Lightweight Zeroth-Order Proximal Gradient Algorithms [65.42376001308064]
  We propose two variance reduced ZO estimators for complex gradient problems. We improve the state-of-the-art function complexities from $mathcalOleft(minfracdn1/2epsilon2, fracdepsilon3right)$ to $tildecalOleft(fracdepsilon2right)$.
  arXiv  Detail & Related papers  (2024-10-03T15:04:01Z)
• SAT and Lattice Reduction for Integer Factorization [5.035245337299788]
  We describe a new hybrid SAT and computer algebra approach to solve random leaked-bit factorization problems. Our implementation solves random leaked-bit factorization problems significantly faster than either a pure SAT or pure computer algebra approach.
  arXiv  Detail & Related papers  (2024-06-28T17:30:20Z)
• Variance-Reduced Fast Krasnoselkii-Mann Methods for Finite-Sum Root-Finding Problems [8.0153031008486]
  We propose a new class of fast Krasnoselkii--Mann methods with variance reduction to solve a finite-sum co-coercive equation $Gx = 0$.<n>Our algorithm is single-loop and leverages a new family of unbiased variance-reduced estimators specifically designed for a wider class of root-finding algorithms.<n> numerical experiments validate our algorithms and demonstrate their promising performance compared to state-of-the-art methods.
  arXiv  Detail & Related papers  (2024-06-04T15:23:29Z)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  We introduce the notion of decomposition hardness (d-hardness) We show that the d-hardness expresses an estimate of the hardness of $C$ w.r.t.
  arXiv  Detail & Related papers  (2023-12-16T12:44:36Z)
• (1+1) Genetic Programming With Functionally Complete Instruction Sets Can Evolve Boolean Conjunctions and Disjunctions with Arbitrarily Small Error [16.075339182916128]
  GP systems can evolve a conjunction of $n$ variables if they are equipped with the minimal required components. We show that a GP system can evolve the exact target function in $O(ell n log2 n)$ in expectation, where $ell geq is a limit on the size of any accepted tree.
  arXiv  Detail & Related papers  (2023-03-13T20:24:21Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
  arXiv  Detail & Related papers  (2022-10-04T09:19:13Z)
• Quantum Goemans-Williamson Algorithm with the Hadamard Test and Approximate Amplitude Constraints [62.72309460291971]
  We introduce a variational quantum algorithm for Goemans-Williamson algorithm that uses only $n+1$ qubits. Efficient optimization is achieved by encoding the objective matrix as a properly parameterized unitary conditioned on an auxilary qubit. We demonstrate the effectiveness of our protocol by devising an efficient quantum implementation of the Goemans-Williamson algorithm for various NP-hard problems.
  arXiv  Detail & Related papers  (2022-06-30T03:15:23Z)
• Higher-order Derivatives of Weighted Finite-state Machines [68.43084108204741]
  This work examines the computation of higher-order derivatives with respect to the normalization constant for weighted finite-state machines. We provide a general algorithm for evaluating derivatives of all orders, which has not been previously described in the literature. Our algorithm is significantly faster than prior algorithms.
  arXiv  Detail & Related papers  (2021-06-01T19:51:55Z)
• Superposition for Lambda-Free Higher-Order Logic [62.997667081978825]
  We introduce refutationally complete superposition calculi for intentional and extensional clausal $lambda$-free higher-order logic. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the $lambda$-free higher-order lexicographic path and Knuth-Bendix orders.
  arXiv  Detail & Related papers  (2020-05-05T12:10:21Z)
• Determining the Multiplicative Complexity of Boolean Functions using SAT [1.4902915966744057]
  We present a constructive SAT-based algorithm to determine the multiplicative complexity of a Boolean function. Our algorithm is capable to find all optimum XAGs for representatives of all 5-input affine-equivalent classes.
  arXiv  Detail & Related papers  (2020-05-04T18:29:48Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.