Source-linked AI summary
Toward a Formally Verified Optimality Certificate for OGR(29): A SAT-Encoding Methods Note with Small-Case Demos
Tong Niu
TL;DR
The note addresses the lack of machine-checkable optimality proofs for Golomb rulers by developing a SAT-certification pipeline and testing it on small cases. It estimates the OGR(29) encoding and proposes cube-and-conquer parallelism, with reported results indicating a months-scale rather than years-scale run on a moderate cluster.
Problem
Existing Distributed.net searches provide witnesses but no machine-checkable optimality certificates, motivating a SAT-based proof pipeline for Golomb-ruler optimality.
Method
The paper develops a v2 ladder SAT encoding with symmetry breaking, validates it on small cases, and proposes Mallob-style cube-and-conquer for OGR(29).
Results
The v2 encoding cuts clause count by 2.5–3× and roughly halves UNSAT time at n = 11; OGR(29, L = 757) has approximately 672k variables and 115M clauses.
Takeaways & Limitations
A formally verified OGR(29) optimality proof would be the first machine-checkable optimality certificate for any non-trivial optimal Golomb ruler.
Abstract
from arXiv · showhide
A Golomb ruler of order~$n$ is an integer set $\{a_0<a_1<\cdots<a_{n-1}\}$ whose $\binom{n}{2}$ pairwise differences $a_j-a_i$ ($i<j$) are all distinct. The optimal Golomb ruler problem asks for $\mathrm{OGR}(n)=\min\{a_{n-1}-a_0\}$ and is a classical combinatorial benchmark. The values $\mathrm{OGR}(2),\dots,\mathrm{OGR}(28)$ are settled through distributed volunteer search (the Distributed.net OGR project); $\mathrm{OGR}(29)$ is in active computation, with verification expected in late 2026 or early 2027. The recent upper bound $\mathrm{OGR}(29)\le 757$ of Lee, Park, and Kim (arXiv:2510.0122, October~2025) tightens the search window. This note describes a compact CNF encoding of the decision problem $\mathrm{GR}(n,L)$ (``is there a Golomb ruler of order~$n$ with length exactly~$L$?'') with $O(n^2 L)$ clauses, together with a small-case verification sweep that emits machine-checkable LRAT certificates of optimality for $\mathrm{OGR}(n)$ at $n\le 12$. We then give closed-form encoding-size estimates for $\mathrm{OGR}(29, L=757)$ and propose a cube-and-conquer decomposition aimed at a Mallob-style parallel run on commodity multi-core hardware. The certificate pipeline (CaDiCaL with --lrat=true, a structural sanity-check, then formal validation by drat-trim or cake\_lpr) is end-to-end. A formally verified optimality proof for any single $\mathrm{OGR}(n)$ value beyond the trivial $n\le 5$ would be a first in the field.
1 Introduction
The note frames Golomb-ruler optimality as a search problem lacking machine-checkable proof certificates, and proposes SAT certification as a narrower, verifiable alternative for OGR(29).
- OGR(n) minimizes ruler length among ordered integer rulers whose pairwise differences are all distinct.
- Distributed.net verified OGR(28) = 585, while OGR(29) remains in active search.
- Distributed.net supplies witnesses but no machine-checkable optimality proof, whereas SAT can emit DRAT or LRAT certificates for external validation.
- The note builds the encoding, validates small cases, and outlines parallel decomposition intended to make OGR(29) certification feasible.
- Related work includes volunteer OGR computation, a bound OGR(29) ≤757 with a SUN heuristic, orbitopal fixing, and cube-and-conquer infrastructure.
2 SAT encoding
The v2 SAT encoding combines position and ladder variables with difference constraints, fixed endpoints, ordering, and symmetry breaking to represent Golomb-ruler feasibility compactly.
- The v2 order-encoding refinement reduces clause count by 2.5–3× and roughly halves UNSAT time at n = 11.
- Primary variables encode mark positions, ladder variables encode prefix occupancy, and auxiliary variables record which pair realizes each difference.
- Channel, ordering, endpoint, and per-position at-most-one constraints ensure marks occupy valid strictly ordered positions.
- Difference implications and per-difference at-most-one constraints enforce that all realized pairwise differences are distinct.
- Why this breaks all symmetries: The reflective break complements fixed-origin and ordering constraints to eliminate translation, relabelling, and orientation symmetries.
- Encoding size: For OGR(29, L = 757), the DIMACS encoding is approximately 3.3 GB.
3 Small-case verification
The small-case sweep used the v2 encoder, CaDiCaL, and LRAT emission on one MacBook M-series core, recovering witnesses matching canonical OGR entries.
- The sweep ran with the v2 encoder, CaDiCaL 3.0.0, and LRAT proof emission on a single MacBook M-series core.
- Witnesses from the last two rows matched the canonical OGR table entries.
4 Estimating OGR(29) runtime
The projected UNSAT cost for OGR(29) is far beyond a monolithic run, so the note proposes cube-and-conquer, Mallob-style parallelism, and certificate stitching and validation.
- Runtime estimate: t29 ∼10^17 seconds under naive extrapolation, making a monolithic CDCL run out of reach.
- Runtime estimate: The GR(n, L∗−1) search tree is estimated at roughly 10^40 for n = 29, L = 756, before aggressive pruning.
- Cube-and-conquer: Splitting on a1 ∈[1, 30] and a27 ∈[L −30, L −1] yields approximately 900 sub-instances, each typically ∼10^-2 the monolithic cost.
- Mallob-style parallelism: A 256-core cluster running 30 days provides ∼180k core-hours and could match a cube depth of ∼17 at OGR(29, 757).
- Certification workflow: The proposed workflow launches SAT at L = 757, decomposes UNSAT at L = 756, stitches per-cube proofs, and validates the combined certificate with cake_lpr.
5 Witness verification
The witness-verification step decodes satisfying assignments into ruler positions and checks both Golomb distinctness and boundary conditions. These checks are machine-checkable in O(n^2) time and can accompany formal certificates.
- The decoder recovers every mark position from a satisfying assignment and verifies that all pairwise differences are distinct.
- The verifier checks the boundary conditions a0 = 0 and a_{n−1} = L alongside the Golomb property.
- O(n^2) machine-checkable checks can be packaged with the LRAT certificate for end-to-end verification.The same checks can be expressed in three lines of Lean 4, Coq, or Isabelle.
6 Conclusions
The conclusions establish small-case end-to-end certification, estimate that the OGR(29) encoding is feasible for parallel SAT, and identify a formally verified OGR(29) proof as a field-first outcome.
- n ≤11 is fully end-to-end on commodity hardware, while v2 reduces clause count by 2.5–3× and roughly halves runtime versus v1.
- ∼672k variables and ∼115M clauses define the OGR(29, L = 757) encoding, with parallel runtime estimated in months rather than years.
- A formally verified optimality proof for OGR(29) would be the first machine-checkable optimality certificate for any non-trivial optimal Golomb ruler.The proposed proof could independently verify or follow Distributed.net’s candidate ruler publication.
Reproducibility
The supplementary repository provides the code, CNF instances, LRAT proofs, and closed-form size table needed to reproduce the encoding and certificate workflow.
- The supplementary repository contains all code, CNF instances, LRAT proofs, and the closed-form size table.
- The repository includes separate v1 pairwise and v2 ladder-plus-Sinz AMO encoders.
- A decoder verifies solutions as Golomb rulers.
- The certificate pipeline script runs the encoder, CaDiCaL, and LRAT processing.
- A structural LRAT sanity-check script is provided.
- A separate script generates the closed-form encoding-size table.