Toward a Formally Verified Optimality Certificate for OGR(29): A SAT-Encoding Methods Note with Small-Case Demos
Abstract
A Golomb ruler of order~n is an integer set {a0<a1<⋯<an−1} whose binomn2 pairwise differences aj−ai (i<j) are all distinct. The optimal Golomb ruler problem asks for OGR(n)=min{an−1−a0} and is a classical combinatorial benchmark. The values OGR(2),…,OGR(28) are settled through distributed volunteer search (the Distributed.net OGR project); OGR(29) is in active computation, with verification expected in late 2026 or early 2027. The recent upper bound OGR(29)≤ 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 GR(n,L) (``is there a Golomb ruler of order~n with length exactly~L?'') with O(n2 L) clauses, together with a small-case verification sweep that emits machine-checkable LRAT certificates of optimality for OGR(n) at n≤ 12. We then give closed-form encoding-size estimates for 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 OGR(n) value beyond the trivial n≤ 5 would be a first in the field.
Related
- Consecutive integers coalesce with density one under the Collatz map: a formally verified proof of a conjecture of Gao
- On Minimax Optimality and Uniqueness of Fixed-Step First-Order Methods for Smooth Convex Optimization
- Stability for a formally determined Lorentzian inverse problem
- Genus of quaternion algebras over formally real fields
- Rigidity for formally determined point source scattering for an anisotropic acoustic medium
BibTeX
@misc{niu2026toward,
title = {{Toward a Formally Verified Optimality Certificate for OGR(29): A SAT-Encoding Methods Note with Small-Case Demos}},
author = {Tong Niu},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.05421},
eprint = {2609.05421},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.05421},
}
RIS
TY - UNPB
TI - Toward a Formally Verified Optimality Certificate for OGR(29): A SAT-Encoding Methods Note with Small-Case Demos
AU - Tong Niu
PY - 2026
DA - 2026/09/01
PB - arXiv
DO - 10.48550/arxiv.2609.05421
UR - https://arxiv.org/abs/2609.05421
AB - A Golomb ruler of order~n is an integer set {a_0<a_1<⋯<a_n−1} whose binomn2 pairwise differences a_j−a_i (i<j) are all distinct. The optimal Golomb ruler problem asks for OGR(n)=min{a_n−1−a_0} and is a classical combinatorial benchmark. The values OGR(2),…,OGR(28) are settled through distributed volunteer search (the Distributed.net OGR project); OGR(29) is in active computation, with verification expected in late 2026 or early 2027. The recent upper bound OGR(29)≤ 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 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 OGR(n) at n≤ 12. We then give closed-form encoding-size estimates for 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 OGR(n) value beyond the trivial n≤ 5 would be a first in the field.
ER -