AI 中文总结
本文提出一种紧凑的SAT编码和证书流水线，用于形式化验证最优Golomb尺问题，并针对OGR(29)给出规模估计和并行分解方案，有望首次实现非平凡情形下的形式化最优性证明。
AI 中文摘要
一个阶为 $n$ 的Golomb尺是一个整数集合 $\{a_0<a_1<\cdots<a_{n-1}\}$，其 $\binom{n}{2}$ 个两两差值 $a_j-a_i$（$i<j$）均互不相同。最优Golomb尺问题要求计算 $\mathrm{OGR}(n)=\min\{a_{n-1}-a_0\}$，这是一个经典的组合基准问题。$\mathrm{OGR}(2)$ 到 $\mathrm{OGR}(28)$ 的值已通过分布式志愿计算（即 this http URL 的 OGR 项目）确定；$\mathrm{OGR}(29)$ 正在积极计算中，预计在2026年底或2027年初完成验证。Lee、Park 和 Kim 最近给出的上界 $\mathrm{OGR}(29)\le 757$（arXiv:2510.0122，2025年10月）收紧了搜索窗口。本笔记描述了一个紧凑的 CNF 编码，用于决策问题 $\mathrm{GR}(n,L)$（“是否存在阶为 $n$、长度恰好为 $L$ 的Golomb尺？”），其子句数为 $O(n^2 L)$，并附带一个小规模验证扫描，为 $n\le 12$ 的 $\mathrm{OGR}(n)$ 生成机器可检查的 LRAT 最优性证书。随后，我们给出了 $\mathrm{OGR}(29, L=757)$ 的闭式编码规模估计，并提出了一种 cube-and-conquer 分解，旨在商品多核硬件上进行 Mallob 风格的并行运行。证书流水线（使用 --lrat=true 的 CaDiCaL、结构健全性检查，然后由 drat-trim 或 cake_lpr 进行形式化验证）是端到端的。对于任何超过平凡 $n\le 5$ 的单个 $\mathrm{OGR}(n)$ 值，形式化验证的最优性证明将是该领域的首次。
英文摘要
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.
Comments6 pages
