# P2600: Shortest superstring of the binary Lyndon words of length eight

- ID: `P2600`
- Reference: `length-eight-lyndon-superstring`
- Page: https://theoremdb.org/statements/P2600
- Record maturity: Reviewed problem with recorded work

## Problem

What is the minimum length of a binary word containing every binary Lyndon word of length \(8\) as a contiguous factor?

### Remarks

- **Remark.** A Lyndon word is strictly lexicographically smaller than each of its nontrivial cyclic rotations.
- **Remark.** There are 30 binary Lyndon words of length 8.

### What counts as a solution

- Give a superstring and a matching lower certificate in the 30-vertex overlap graph.

## Status

A Boolean satisfiability computation rules out length 48, while a replayable 94-bit word covers all 30 targets. [1](#reference-1)

## Work

### Evidence for the current status

**Computation 1 (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.

Let \(L_8\) be the set of the 30 binary Lyndon words of length eight, and let \(m\) be the minimum length of a word containing every member of \(L_8\). The current certificates give
\[
49\leq m\leq94.
\]

For the lower endpoint, fix a proposed length \(N\). Introduce one Boolean variable for each position of the proposed superstring. For every \(w\in L_8\), assert a disjunction over its \(N-7\) possible starting positions, with eight bit equalities in each disjunct. This formula is satisfiable exactly when a length-\(N\) common superstring exists. Z3 5.0.0 returns `unsat` at \(N=48\), which also rules out every shorter length because a shorter superstring can be padded to length 48.

For the upper endpoint, view each required word as an edge in the order-seven binary de Bruijn graph. The 30 required edges form 11 weak components, each a directed path. Spelling those paths gives blocks of lengths
\[
14,12,10,11,10,8,9,8,9,8,8.
\]
An exact Held-Karp computation over these 11 blocks finds a shortest block-preserving merge of length 94. One such word is
\[
\texttt{0000000111111100000101111100001001111010000110111100010101110001100100101101100011101100110101}.
\]
The artifact regenerates all targets and checks every containment directly. The interval remains open. In particular, the 94-bit construction is optimal only within the stated block-preserving family.

### Background and intake notes

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.

- Original intake status: Status unknown. The Fredricksen-Kessler-Maiorana construction and universal-cycle literature may settle this exact variant.
- View each required eight-bit word as a directed edge whose tail is its seven-bit prefix and whose head is its seven-bit suffix in the order-7 binary de Bruijn graph. The target becomes a directed rural-postman path covering 30 required edges.
- A flow relaxation can balance required-edge degree deficits, while branch-and-bound chooses connecting paths between components. This avoids the 30 times 2^30 subset table.

- Recorded example: A 94-bit incumbent is 0001100100101101100000001111111000101011100011101100001101111001101010000100111101000001011111.

### Prior approaches

- **Route 1** (supported): 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. [1](#reference-1)

### Runnable artifacts

- **Artifact 1** (reproduced): Standard-library Python generates the target set, extracts its required-edge paths, solves the 11-block merge exactly, and verifies the 94-bit result.
- **Artifact 2** (reproduced): A direct encoding of every possible target placement is unsatisfiable under Z3 5.0.0. [3](#reference-3)

### 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.

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `length-eight-lyndon-superstring`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome.

## References

1 entry has incomplete source metadata. Each affected row names the fields that still need editorial review.

1. <a id="reference-1"></a>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 https://doi.org/10.1016/0012-365X(78)90002-X
   - Also cited at Lower endpoint reproduced by lyndon8-artifact-unsat-at-48; upper endpoint reproduced by lyndon8-artifact-component-superstring
   - journal_article; primary source; version of record; checked 2026-08-01
   - Source use: original_summary
   - 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.
2. <a id="reference-2"></a>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 https://github.com/Z3Prover/z3/tree/8e3402b215a810a4154eb183a7dfc4e853eb2f52
   - software; software source; z3-solver 5.0.0.0 (solver 5.0.0), release tag z3-5.0.0, commit 8e3402b215a810a4154eb183a7dfc4e853eb2f52; checked 2026-08-01
   - Source 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.
3. <a id="reference-3"></a>https://github.com/Z3Prover/z3/tree/1c899374739f7c1cdbe6ba72dd61aa1d7daaee27
   - software; software source; commit 1c899374739f7c1cdbe6ba72dd61aa1d7daaee27; checked 2026-07-25
   - Source metadata incomplete: publication-style citation, exact locator, relevance note, source-use mode.