An exact sparse-ruler solver at parity with Robison's lost 2014 computation, and why length 213 is still the frontier

The question

A sparse ruler of length L is a set A of integers with 0 and L in A such that every distance 1, 2, …, L is the difference of two elements of A. F(L) is the smallest possible |A|. Erdős and Gál asked in 1948 how F(L) grows; the quantity is lim F(L)/√L, and Erdős problem #170 asks for its value. Leech (1956) and Wichmann (1963) pinned it between √2.434 and √3, and Pegg's excess conjecture (2019) says F(L) − round(√(3L + 9/4)) is always 0 or 1, which would make the limit √3.

What was known

• Exact values F(L) are proven for L ≤ 213 (OEIS A046693). They come from Arch Robison's 2014 program "Parallel Computation of Sparse Rulers" (Intel Developer Zone, read from the web.archive.org copy), a recursive search run for months on a 256-core SGI UV. His longest single run, enumerating all 25-mark rulers of length 208, took 51 hours on the 256 cores. Only the counts of rulers survive; the rulers themselves were lost (Pegg, Wolfram Blog, 2020-02-12).
• A004137 gives the longest complete ruler with n marks: 213 for n = 25, and lists 232 for n = 26. The entry page itself was not reachable from this session, only the b-file, so the provenance of the 26-mark term was not checked.
• Wichmann's construction W(r,s) = 1^r, r+1, (2r+1)^r, (4r+3)^s, (2r+2)^(r+1), 1^r (a gap sequence; a^b means b gaps of a) has length 4r(r+s+2) + 3(s+1) and 4r+s+3 marks. Pegg proved by construction, with 2069 such recipes, that the excess is at most 1 for every L; whether it is ever negative is the open half of his conjecture.
• F is not monotone: F(137) = 20 < F(136) = 21, and similar dips precede each Wichmann length (Robison's "gap" observation).

What we did

We wrote an exact decision procedure in Rust (standard library only): given L and M, does a complete ruler with M marks exist? F(L) is the first M, counted up from the pigeonhole bound C(M,2) ≥ L, for which the answer is yes; the exhaustive refutation at F(L) − 1 is the proof and carries all the cost.

The solver is Robison's inward sweep, rebuilt from his article. Positions are decided from both ends inward: at depth w everything in [0, w] and [L−w, L] is settled, and the children at w+1 place a mark on the left, on the right, on both, or on neither. Three facts prune the tree. Every distance of at least L−w must already be covered, because every later mark lies strictly inside and only creates shorter distances. With p marks placed and k left, the new marks create at most k·p + C(k,2) pairs, so that many uncovered distances at most can remain. And while the partial ruler is mirror symmetric the right-only child is the reflection of the left-only one and is skipped, which removes the reflection symmetry exactly. Marks, their reflection and the covered distances are three 7-word bitsets, so placing a mark is two multiword shifts; the sweep runs at about 24 million nodes per second per thread on an i9-13900KF. Work is split by handing every node at a fixed mark depth to one of 8 threads.

A second, independently formulated solver (branch on the largest uncovered distance over the pairs that realise it, forbidding already-searched pairs as two-literal clauses) agrees with the sweep on every refutation tried up to L = 130 and visits about half as many nodes at 5–10 times the cost per node. Both agree with plain subset enumeration for every L ≤ 40. Several sharper bounds (a per-position pigeonhole, branching on the long distance with the fewest realising positions, a bound on distances that need two new marks) were measured at L = 110 and 120 and all cost more than they saved; the node histogram shows the tree's bulk at three to five remaining marks, right at the edge of the counting bound.

Witness rulers at F(L) come from the Wichmann family plus appended marks, truncations and a one-gap, one-mark repair step, which reaches F(L) at all but 30 lengths below 213; at those the sweep searches the witness itself (50 of the first 123 lengths, 3–45 CPU-seconds each).

The validation run sr fl 1 213 -t 8 is executing under nice -n 19 on a machine whose cores belong to another job, so wall times are noisy and CPU-seconds are the cost reported. At the time of writing it has completed L ≤ 123 and is working on L = 124.

What we found

Every F(L) for L ≤ 123 agrees with A046693. In that range the excess is 0 except at L = 51, 59, 69 and 113, where it is 1, matching Pegg's list (A308766); it is never negative. The ruler data in data/validation.csv are fresh witnesses for a range whose original witnesses were lost. The hardest refutation finished so far is L = 113, M = 18: 3,340,626,056 nodes, 139.68 CPU-seconds.

The cost is governed by the block starts, the first length L whose F exceeds M, where M must be refuted with the loosest pigeonhole; inside a block the cost falls about 1.4× per unit of L.

From M = 14 on the ratio between consecutive block starts rises by about 1.4 per extra mark (3.3, 4.4, 5.7, 7.1), so the tree grows like exp(c·M²), and the extrapolation below continues that rise. If the ratio levels off instead, the far rows shrink by up to an order of magnitude; the figures are estimates, with no tighter error than that.

Robison's 51 hours on 256 cores are 4.7·10⁷ core-seconds for the enumeration at L = 208, M = 25, and his block-start refutations at M = 24 and 25 were of the same order or larger. The extrapolated 3.6·10⁸ and 6.1·10⁹ CPU-seconds for the same mark counts, on cores several times faster than his, say that this solver is at parity with his program and gains only from hardware.

What it means and what it does not mean

• Proved here: F(L) for L ≤ 123, independently of Robison's data, by exhaustive search, with explicit rulers. The run continues and the repository's table will grow; nothing above L = 213 was searched.
• Settled by combining published results, not by new computation: A004137(25) = 213 (Robison) means no 25-mark ruler is longer than 213, so F(L) ≥ 26 for all L ≥ 214, and the constructions in the repository give 26-mark rulers at 214–223, 227, 228, 231, 232. So F(L) = 26 at those lengths, with excess 1 at 214 and 215 and 0 at the others. A046693 stops at 213 and does not list them.
• Heuristic: the exp(c·M²) growth and every number in the extrapolation table.
• Nothing here bears on the limit lim F(L)/√L or on the sign of the excess beyond L = 213. This recovers part of a lost dataset and measures how far exact search can go; it settles nothing new about the problem Erdős asked.

What is left

The first lengths where F is genuinely open are 224, 225, 226, 229, 230 and 233: the best rulers known have 27 marks (28 from this family at 225 and 226, where Pegg's theorem guarantees 27), and proving F = 27 means refuting M = 26, at an estimated 10¹¹ CPU-seconds with this method. A week on 32 cores is 1.9·10⁷ CPU-seconds; with the measured curve it would finish every block through L = 178 and most of the single refutation at L = 179. Getting to 213, let alone past it, needs a pruning idea worth two to four orders of magnitude, and the measurements above say where it has to act: at three to six remaining marks, where positions look fine one at a time and only their mutual interference rules them out.

Reproduce it

cd /neptune/sparse-rulers
cargo build --release
./target/release/sr brute 1 40                       # F(L) by subset enumeration
./target/release/sr fl 1 40                          # same values from the solver
./target/release/sr fl 1 213 -t 8 -o data/validation.csv
./target/release/sr solve 113 18                     # the hardest refutation above
./target/release/sr solve 113 18 -P                  # same answer from the pair-branching solver
./target/release/sr wichmann 300                     # W(L), excess and witness per length
python3 scripts/plot_growth.py cpu-vs-m.png
awk -F'[ ,]' 'NR==FNR{if($1!~/^#/)ref[$1]=$2;next} ($1 in ref)&&ref[$1]!=$2{print "mismatch",$1}' \
    data/a046693_bfile.txt data/validation.csv