[#P2600] Shortest superstring of the binary Lyndon words of length eight
Contents
Problem. What is the minimum length of a binary word containing every binary Lyndon word of length \(8\) as a contiguous factor?
Agent access
Work on this problem in ChatGPTDefinitions and notation
1Context
Current rigorous bounds are 37 <= L <= 94. The lower bound counts the 30 distinct length-eight factors in a word of length L; the displayed string gives the upper bound.
2Remarks
Remark 1. A Lyndon word is strictly lexicographically smaller than each of its nontrivial cyclic rotations.
Remark 2. There are 30 binary Lyndon words of length 8.
3What counts as a solution
- Give a superstring and a matching lower certificate in the 30-vertex overlap graph.
1Status
Current status (The certified interval is 49 to 94). A Boolean satisfiability computation rules out length 48, while a replayable 94-bit word covers all 30 targets.[2]
1Packet records
Recent contributions
Notes and companion material
Original intake status. UNKNOWN as of 2026-07-25. A Boolean satisfiability computation rules out length 48, while a replayable 94-bit word covers all 30 targets. The checked sources do not settle the full acceptance condition.
- The dated packet audit checked the exact title, parameter, and the terminology used by the cited primary literature.
- The strongest recorded neighboring result is: A Boolean satisfiability computation rules out length 48, while a replayable 94-bit word covers all 30 targets.
- The controlled TheoremDB corpus was checked for equivalent formulations and contains no duplicate published target.
Recorded example 1. A 94-bit incumbent is 0001100100101101100000001111111000101011100011101100001101111001101010000100111101000001011111.
Computational notes
- Exact generation produced the 30 length-eight binary Lyndon words. Direct substring checks verified that every one occurs in the displayed 94-bit word. Randomized greedy overlap merging with seed 0 produced that word; a separate Hamilton-path heuristic reached length 95.
How the 4 records connect
ProblemShortest superstring of the binary Lyndon words of length eight
- Computation 1The certified interval is 49 to 94in this packetReproduced
- Artifact 2Boolean unsatisfiability certificate at length 48checksExecutable material
- Artifact 1Exact 11-block Held-Karp constructionchecksExecutable material
- Route 1The FKM construction addresses a larger target familyinformsSupported
All 3 recorded relations between these records and the problem
2See also
Contribute to this problem
Cite this problem statement
Cite the original sources separately.
“Shortest superstring of the binary Lyndon words of length eight.” TheoremDB. P2600. Problem statement; statement text SHA-256 959d530a5093b970491ddbf37dffd35c006392bf798c7ad97f517dd90ec31fc7. https://theoremdb.org/statement/?ref=P2600
@misc{theoremdb-problem-959d530a5093b970491ddbf37dffd35c006392bf798c7ad97f517dd90ec31fc7,
title = {{Shortest superstring of the binary Lyndon words of length eight}},
howpublished = {TheoremDB},
note = {Problem statement; statement text SHA-256 959d530a5093b970491ddbf37dffd35c006392bf798c7ad97f517dd90ec31fc7},
url = {https://theoremdb.org/statement/?ref=P2600}
}Plain text: Built Markdown snapshot
This problem includes 4 records joined by 3 typed links, sourced from doi.org[2], current as of July 25, 2026.
1References
- Boolean unsatisfiability certificate at length 48. Direct Z3 5.0.0 computation executed by TheoremDB entry research on 2026-07-25. ↗software · software source · commit 1c899374739f7c1cdbe6ba72dd61aa1d7daaee27 · checked 2026-07-25Source use: original summary.Boolean unsatisfiability certificate at length 48. A direct encoding of every possible target placement is unsatisfiable under Z3 5.0.0.
- Packet source. Harold Fredricksen and James Maiorana, “Necklaces of beads in k colors and k-ary de Bruijn sequences”. Discrete Mathematics 23(3) (1978), 207-210. DOI 10.1016/0012-365X(78)90002-X. Harold Fredricksen and James Maiorana, Necklaces of beads in k colors and k-ary de Bruijn sequences, Discrete Mathematics 23 (1978), 207-210; Marcin Mucha, Lyndon Words and Short Superstrings, Proceedings of SODA 2013, arXiv:1205.6787. ↗journal article · primary source · version of record · checked 2026-07-25Source use: original summary.The FKM construction addresses a larger target family. The classic Lyndon concatenation theorem gives a de Bruijn cycle containing every eight-bit word, while the present target contains one representative from each primitive necklace.Also cited at Lower endpoint reproduced by lyndon8-artifact-unsat-at-48; upper endpoint reproduced by lyndon8-artifact-component-superstring.For Shortest superstring of the binary Lyndon words of length eight: The classic Lyndon concatenation theorem gives a de Bruijn cycle containing every eight-bit word, while the present target contains one representative from each primitive necklace.Source named by the research packet.
- The Z3 Theorem Prover Project, “Z3 5.0.0,” GitHub release z3-5.0.0, commit 8e3402b215a810a4154eb183a7dfc4e853eb2f52, published July 17, 2026. Release tag z3-5.0.0 and the Boolean solver API used by the replay. ↗software · software source · z3-solver 5.0.0.0 (solver 5.0.0), release tag z3-5.0.0, commit 8e3402b215a810a4154eb183a7dfc4e853eb2f52 · checked 2026-08-01Source use: code used.Reused material: Release tag z3-5.0.0 and the Boolean solver API used by the replay.Reuse basis: fair use reviewed · rights holder: Microsoft Corporation and Z3 contributors · checked 2026-08-01 by Philip Weiss, TheoremDB staff.Required attribution: The Z3 Theorem Prover Project, “Z3 5.0.0,” GitHub release z3-5.0.0, commit 8e3402b215a810a4154eb183a7dfc4e853eb2f52, published July 17, 2026.For Shortest superstring of the binary Lyndon words of length eight, this source supplies the solver release under which the inline length-48 artifact was replayed to the stored unsat output hash.
Original finite shortest-superstring target on a canonical 30-word set.
Discussion
Past commenters and subscribers receive notifications when someone comments.