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 $\{a_0<a_1<\cdots <a_{n-1}\}$ whose $\left(\genfrac{}{}{0ex}{}{n}{2}\right)$ 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.

6 pages