{
  "abstract": "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.",
  "abstract_shown": true,
  "affiliations": [],
  "article_type": null,
  "arxiv": "2609.05421",
  "author_total": 1,
  "authors": [
    {
      "name": "Tong Niu"
    }
  ],
  "bibtex": "https://research.draconitic.com/paper/62cvy477ey71b.bib",
  "cited_by": 0,
  "doi": "10.48550/arxiv.2609.05421",
  "fulltext_url": null,
  "id": "62cvy477ey71b",
  "issns": [],
  "landing_url": "https://arxiv.org/abs/2609.05421",
  "language": null,
  "licence": "LicenseRef-arXiv-nonexclusive-1.0",
  "licence_label": "arXiv licence",
  "licence_source": "article",
  "licence_url": "http://arxiv.org/licenses/nonexclusive-distrib/1.0/",
  "metadata_licence": "CC0-1.0",
  "native_subjects": [
    [
      "arxiv",
      "cs.DC"
    ],
    [
      "arxiv",
      "math.CO"
    ],
    [
      "openalex",
      "1705|Constraint Satisfaction and Optimization"
    ]
  ],
  "openalex": "W7212058836",
  "pdf_url": "https://arxiv.org/pdf/2609.05421",
  "pmcid": null,
  "pmid": null,
  "published": "2026-09-01",
  "publisher": null,
  "ris": "https://research.draconitic.com/paper/62cvy477ey71b.ris",
  "sources": [
    {
      "first_seen": "2026-10-30T12:19:58Z",
      "native_id": "2609.05421",
      "source": "arxiv",
      "url": "https://arxiv.org/abs/2609.05421"
    }
  ],
  "subjects": [
    {
      "field": "mathematics",
      "origin": "arxiv:math.CO",
      "subfield": "combinatorics"
    }
  ],
  "title": "Toward a Formally Verified Optimality Certificate for OGR(29): A SAT-Encoding Methods Note with Small-Case Demos",
  "title_text": "Toward a Formally Verified Optimality Certificate for OGR(29): A SAT-Encoding Methods Note with Small-Case Demos",
  "type": "preprint",
  "updated_at": "2026-10-30T12:19:58Z",
  "url": "https://research.draconitic.com/paper/62cvy477ey71b",
  "venue": "arXiv",
  "versions": []
}