PaperlayerView exact revision on arXiv

Source-linked AI summary

Toward a Formally Verified Optimality Certificate for OGR(29): A SAT-Encoding Methods Note with Small-Case Demos

Tong Niu

arXiv:2609.05421v1cs.DCmath.CO

TL;DR

The note addresses the lack of machine-checkable optimality proofs for Golomb rulers by developing a SAT-certification pipeline and testing it on small cases. It estimates the OGR(29) encoding and proposes cube-and-conquer parallelism, with reported results indicating a months-scale rather than years-scale run on a moderate cluster.

  • Problem

    Existing Distributed.net searches provide witnesses but no machine-checkable optimality certificates, motivating a SAT-based proof pipeline for Golomb-ruler optimality.

    Source: §1.2 · p. 1

  • Method

    The paper develops a v2 ladder SAT encoding with symmetry breaking, validates it on small cases, and proposes Mallob-style cube-and-conquer for OGR(29).

    Source: §1.2 · p. 1, §2 · p. 2, §2.3 · p. 3

  • Results

    The v2 encoding cuts clause count by 2.5–3× and roughly halves UNSAT time at n = 11; OGR(29, L = 757) has approximately 672k variables and 115M clauses.

    Source: §6 · p. 5

  • Takeaways & Limitations

    A formally verified OGR(29) optimality proof would be the first machine-checkable optimality certificate for any non-trivial optimal Golomb ruler.

    Source: §6 · p. 5

Abstract

from arXiv · show

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.

1 Introduction

The note frames Golomb-ruler optimality as a search problem lacking machine-checkable proof certificates, and proposes SAT certification as a narrower, verifiable alternative for OGR(29).

  • OGR(n) minimizes ruler length among ordered integer rulers whose pairwise differences are all distinct.Source: §1.1 · p. 1
  • Distributed.net verified OGR(28) = 585, while OGR(29) remains in active search.Source: §1.1 · p. 1
  • Distributed.net supplies witnesses but no machine-checkable optimality proof, whereas SAT can emit DRAT or LRAT certificates for external validation.Source: §1.2 · p. 1
  • The note builds the encoding, validates small cases, and outlines parallel decomposition intended to make OGR(29) certification feasible.Source: §1.2 · p. 1
  • Related work includes volunteer OGR computation, a bound OGR(29) ≤757 with a SUN heuristic, orbitopal fixing, and cube-and-conquer infrastructure.Source: §1.3 · p. 2

2 SAT encoding

The v2 SAT encoding combines position and ladder variables with difference constraints, fixed endpoints, ordering, and symmetry breaking to represent Golomb-ruler feasibility compactly.

  • The v2 order-encoding refinement reduces clause count by 2.5–3× and roughly halves UNSAT time at n = 11.Source: §2 · p. 2
  • Primary variables encode mark positions, ladder variables encode prefix occupancy, and auxiliary variables record which pair realizes each difference.Source: §2.1 · p. 2
  • Channel, ordering, endpoint, and per-position at-most-one constraints ensure marks occupy valid strictly ordered positions.Source: §2.2 · p. 2
  • Difference implications and per-difference at-most-one constraints enforce that all realized pairwise differences are distinct.Source: §2.2 · p. 2

Why this breaks all symmetries

  • The reflective break complements fixed-origin and ordering constraints to eliminate translation, relabelling, and orientation symmetries.Source: §2.2 · p. 3, §2.3 · p. 3

Encoding size

  • For OGR(29, L = 757), the DIMACS encoding is approximately 3.3 GB.Source: Table 1 · p. 3

3 Small-case verification

The small-case sweep used the v2 encoder, CaDiCaL, and LRAT emission on one MacBook M-series core, recovering witnesses matching canonical OGR entries.

  • The sweep ran with the v2 encoder, CaDiCaL 3.0.0, and LRAT proof emission on a single MacBook M-series core.Source: §3 · p. 3
  • Witnesses from the last two rows matched the canonical OGR table entries.Source: §3 · p. 3

4 Estimating OGR(29) runtime

The projected UNSAT cost for OGR(29) is far beyond a monolithic run, so the note proposes cube-and-conquer, Mallob-style parallelism, and certificate stitching and validation.

Runtime estimate

  • t29 ∼10^17 seconds under naive extrapolation, making a monolithic CDCL run out of reach.Source: §4 · p. 3
  • The GR(n, L∗−1) search tree is estimated at roughly 10^40 for n = 29, L = 756, before aggressive pruning.Source: §4 · p. 3

Cube-and-conquer

  • Splitting on a1 ∈[1, 30] and a27 ∈[L −30, L −1] yields approximately 900 sub-instances, each typically ∼10^-2 the monolithic cost.Source: §4 · p. 4

Mallob-style parallelism

  • A 256-core cluster running 30 days provides ∼180k core-hours and could match a cube depth of ∼17 at OGR(29, 757).Source: §4 · p. 4

Certification workflow

  • The proposed workflow launches SAT at L = 757, decomposes UNSAT at L = 756, stitches per-cube proofs, and validates the combined certificate with cake_lpr.Source: §4 · p. 4

5 Witness verification

The witness-verification step decodes satisfying assignments into ruler positions and checks both Golomb distinctness and boundary conditions. These checks are machine-checkable in O(n^2) time and can accompany formal certificates.

  • The decoder recovers every mark position from a satisfying assignment and verifies that all pairwise differences are distinct.Source: §5 · p. 5
  • The verifier checks the boundary conditions a0 = 0 and a_{n−1} = L alongside the Golomb property.Source: §5 · p. 5
  • O(n^2) machine-checkable checks can be packaged with the LRAT certificate for end-to-end verification.The same checks can be expressed in three lines of Lean 4, Coq, or Isabelle.Source: §5 · p. 5

6 Conclusions

The conclusions establish small-case end-to-end certification, estimate that the OGR(29) encoding is feasible for parallel SAT, and identify a formally verified OGR(29) proof as a field-first outcome.

  • n ≤11 is fully end-to-end on commodity hardware, while v2 reduces clause count by 2.5–3× and roughly halves runtime versus v1.Source: §6 · p. 5
  • ∼672k variables and ∼115M clauses define the OGR(29, L = 757) encoding, with parallel runtime estimated in months rather than years.Source: §6 · p. 5
  • A formally verified optimality proof for OGR(29) would be the first machine-checkable optimality certificate for any non-trivial optimal Golomb ruler.The proposed proof could independently verify or follow Distributed.net’s candidate ruler publication.Source: §6 · p. 5

Reproducibility

The supplementary repository provides the code, CNF instances, LRAT proofs, and closed-form size table needed to reproduce the encoding and certificate workflow.

Loading 2609.05421v1…