A new best-known dominating set for the twelfth Fibonacci cube, and a month-long solver run that returned no answer

The question#

Picture a network of points joined by links, and suppose you want to place guards on as few points as possible so that every point either has a guard or is linked to a point that does. A set of guarded points like that is called a dominating set, and the question is how small it can be.

The network here is the twelfth Fibonacci cube. Each of its points is a string of twelve 0s and 1s with no two 1s next to each other, and two points are linked when their strings differ in exactly one place. It has 377 points and 1,308 links. A 2018 paper by Azarija, Klavžar, Rho and Sim showed that any dominating set needs at least 54 points, and found one with 61. The OEIS (the Online Encyclopedia of Integer Sequences, a public database of number sequences) records that range in entry A291295.

A smaller covering set#

In August 2026, Claude, the AI model I work with, ran a solver search that found a dominating set of 59 points. Before trusting it, I had it checked by a separate program written directly from the definition, sharing no code with the search, and it covers every point. That set is now listed in A291295 as the best known, so the range is 54 to 59. This is the main result. The search that found it did not find anything smaller, and a separate attempt at 57 points was cut off before it finished.

The month-long run#

The bottom of the range is harder. The solvers used in that August search, an integer-programming solver (SCIP) and Google's CP-SAT, report a rising lower bound as they work, but their best lower bound stopped climbing at about 51, below the 54 that was already published. So I tried a different approach: ask a SAT solver, a program that settles yes-or-no logic puzzles, the single question "is there a dominating set of at most 54 points?" A yes would have settled the problem at 54. A proven no would have narrowed the range to 55 to 59. There are more than 10^66 ways to choose 54 of the 377 points, so checking them one by one was never an option.

The run started on August 21, 2026, on one core of my laptop. Run the way I ran it, the solver printed nothing until it had an answer, so there was no way to tell how close it was.

On September 3, a Claude agent doing a read-only audit of my project records flagged that the run had no rule for when to stop. I set day 21, September 11, as the point to decide. On that day an agent laid out the options for me (stop, keep going, or restart in a form that could resume after a crash), none with a reliable time estimate. I chose to keep going and asked for everything about the run to be recorded. Because the solver kept all its progress in memory, a reboot would have lost every hour of it, so the exact question was saved and a small watcher program was attached to capture any answer the moment the solver stopped. No reboot happened.

On September 20, 2026, after 29 days 22 hours 32 minutes, the solver had still printed nothing, and I ended the run and asked for everything we had to be published. The watcher confirmed it stopped without an answer.

What the run did and did not show#

A solver stopped before it answers proves nothing, however long it ran. The run did not show that 54 points are impossible, and its length is not evidence either way. The range is still 54 to 59.

What I now decide before a long run#

Three things should be settled before a long job starts: when to stop, how progress gets saved, and whether the program keeps a proof log, so that a final "no" comes with a proof anyone can check rather than the solver's word for it. Only the stopping rule can be added once the job is running. In this run it was added weeks in, and the other two were missing throughout. The plan written up for a next attempt fixes both: it splits the question into many small pieces, saves each piece's answer to disk as soon as it is found, and logs a proof, so a crash would cost one piece instead of a month.

What I published#

The same night the run ended, everything needed to check or repeat the work went into a public repository: the 59-point set with its own checker, the exact question the solver was given, the run record, and the plan for a next attempt. It is archived on Zenodo with a DOI (a permanent, citable identifier): 10.5281/zenodo.22985212. Its README describes it the same way this post does: a documented attempt that changes no bound, whose result is the verified set.

For specialists#

First round (August 2026): OR-Tools CP-SAT minimization and SCIP ILP, with reversal symmetry breaking, reproduced A291295 for n = 1 to 10 with optimality proved by both routes; on Γ_12 the best solver lower bound stalled near 51 and the incumbent reached 59 (a size-≤59 feasibility run); the CP-SAT run that found it found nothing smaller, and a size-57 push was cut off by the environment's background-job limit. An independent 2-packing gives only γ ≥ 41.

Encoding of the decision run: closed-neighborhood covering clauses over the 377 vertex variables, PySAT's seqcounter cardinality encoding for at most 54 chosen vertices, and lex-leader symmetry breaking on the bit-reversal involution. The symmetry breaking is sound for UNSAT because every solution orbit retains its lex-leader. The instance has 18,183 variables and 37,713 clauses, as stated in its DIMACS header and printed by the process at launch. (An earlier planning note quotes larger figures; they describe an encoding that was replaced before launch.) It was regenerated from the encoder twice after launch, byte-identical both times, and its SHA-256 hash is stored beside it in the deposit. As a launch-night check, the same encoder at k = 70 returned SAT in 33^▲ seconds and the witness was verified as dominating; the witness file itself was not kept, and the deposit says so.

Solver: CaDiCaL 1.9.5 through PySAT, one process, one core, no proof log, no checkpoint (learned clauses live in memory only). Started 2026-08-21, terminated by SIGTERM on 2026-09-20 at the author's instruction; the last process-table line shows 29 days 22 hours 32 minutes elapsed and 710.4 CPU-hours. The watcher recorded no answer file. Without DRAT output even an UNSAT verdict would have been the solver's report rather than a checkable proof. The follow-up method in the deposit is cube-and-conquer with DRAT logging: a lookahead splitter divides the instance into cubes, each cube's verdict is appended to disk as found, and an UNSAT result becomes checkable with drat-trim.

The deposit holds 24 files: the 59-set with a verifier sharing no code with the search, the k = 54 CNF with its hash and the script that regenerates it, the run record, saved copies of the OEIS entry and the source paper (Azarija, Klavžar, Rho, Sim, "On domination-type invariants of Fibonacci cubes and hypercubes", Ars Mathematica Contemporanea 14 (2018) 387-395, Table 3), a manifest, and a script that rechecks all of it on a fresh clone. Code under the MIT license; data and text under an open license.

@misc{orden2026thirtydaysnoanswer,
  author       = {Tyler Satchel Orden},
  title        = {A new best-known dominating set for the twelfth Fibonacci cube, and a month-long solver run that returned no answer},
  year         = {2026},
  howpublished = {Cyborg Mathematics},
  url    = {https://cyborgmathematics.com/writing/thirty-days-no-answer}
}