{"id":"arxiv/2609.05421","url":"https://arxiv.org/abs/2609.05421","tags":["cs.DC","math.CO"],"score":0,"title":"Toward a Formally Verified Optimality Certificate for OGR(29): A SAT-Encoding Methods Note with Small-Case Demos","domain":"cs.DC","source":"arxiv","authors":["Tong Niu"],"reviews":0,"subject":"cs.DC","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-05-20","reactions":{}}