TheoremDB

Problem packetResearch packetR479

R479Executable evidence

Exact 11-block Held-Karp construction

View replayOpen source ↗
Link to a section

Authored summary

Standard-library Python generates the target set, extracts its required-edge paths, solves the 11-block merge exactly, and verifies the 94-bit result.

Executable material is recorded. Successful replay is a separate check.

Recorded status: available

Recorded scope: the 30 binary Lyndon words of length 8 and superstrings formed by merging their 11 maximal required-edge path spells as indivisible blocks

Complete recorded scope and conditions
{
  "kind": "bounded",
  "statement": "the 30 binary Lyndon words of length 8 and superstrings formed by merging their 11 maximal required-edge path spells as indivisible blocks",
  "bounds": {
    "required_words": {
      "min": 30,
      "max": 30
    },
    "required_edge_components": {
      "min": 11,
      "max": 11
    },
    "held_karp_states_upper_bound": {
      "min": 22528,
      "max": 22528
    },
    "optimal_block_preserving_length": {
      "min": 94,
      "max": 94
    }
  },
  "exhaustive": true
}

Originating problem: Shortest superstring of the binary Lyndon words of length eight

Recorded relationships: The certified interval is 49 to 94

Authored record and scope
Authored title
Exact 11-block Held-Karp construction
Record type
artifact
Stored status
available
Evidence grade
executable
Recorded scope data
{ "kind": "bounded", "statement": "the 30 binary Lyndon words of length 8 and superstrings formed by merging their 11 maximal required-edge path spells as indivisible blocks", "bounds": { "required_words": { "min": 30, "max": 30 }, "required_edge_components": { "min": 11, "max": 11 }, "held_karp_states_upper_bound": { "min": 22528, "max": 22528 }, "optimal_block_preserving_length": { "min": 94, "max": 94 } }, "exhaustive": true }
Linked research record IDs
R482

2Authored explanation

A length-eight word \(a_1\cdots a_8\) is represented by the directed edge \[ a_1\cdots a_7\longrightarrow a_2\cdots a_8. \] For this target set, each required vertex has at most one required outgoing edge. Starting at every required tail that is not also a required head therefore recovers all 11 maximal paths. Their spells are \[ \begin{gathered} 00000001111111,\ 000001011111,\ 0000100111,\ 00001101111,\\ 0001010111,\ 00011001,\ 000111011,\ 00100101,\\ 001011011,\ 00110101,\ 00111101. \end{gathered} \]

The dynamic program stores the shortest merge ending in block \(i\) for every pair \((S,i)\), where \(S\) is a subset of the 11 blocks. A transition appends block \(j\) after deleting its longest prefix equal to a suffix of block \(i\). Every permutation of the blocks appears in the recurrence, so the value 94 is exact for this restricted family.

The resulting word has SHA-256 digest `3d898b0878cfa058b136a3d1c24244e3154d38a8c30bce767c3fbef686978de0`. Direct substring tests confirm that it contains all 30 generated Lyndon words.

Files and source

Files embedded in this record. Matching a file hash confirms its identity.

  • R479.txt2,648 bytes · No SHA-256 recorded
    Preview R479.txt
    from hashlib import sha256
    from itertools import product
    from json import dumps
    
    words = [''.join(bits) for bits in product('01', repeat=8)
             if all(''.join(bits) < ''.join(bits)[i:] + ''.join(bits)[:i]
                    for i in range(1, 8))]
    assert len(words) == 30
    
    outgoing = {word[:-1]: word for word in words}
    heads = {word[1:] for word in words}
    components = []
    for word in [word for word in words if word[:-1] not in heads]:
        text = word
        vertex = word[1:]
        while vertex in outgoing:
            word = outgoing[vertex]
            text += word[-1]
            vertex = word[1:]
        components.append(text)
    assert components == [
        '00000001111111', '000001011111', '0000100111',
        '00001101111', '0001010111', '00011001', '000111011',
        '00100101', '001011011', '00110101', '00111101']
    
    def overlap(a, b):
        return max([0] + [k for k in range(1, min(len(a), len(b)) + 1)
                          if a[-k:] == b[:k]])
    
    n = len(components)
    dp = {(1 << i, i): (len(components[i]), (i,)) for i in range(n)}
    for mask in range(1, 1 << n):
        for i in range(n):
            state = dp.get((mask, i))
            if state is None:
                continue
            cost, path = state
            for j in range(n):
                if mask >> j & 1:
                    continue
                candidate = (cost + len(components[j])
                             - overlap(components[i], components[j]),
                             path + (j,))
                key = (mask | 1 << j, j)
                if key not in dp or candidate < dp[key]:
                    dp[key] = candidate
    
    optimum, path = min(dp[((1 << n) - 1, i)] for i in range(n))
    superstring = components[path[0]]
    for i, j in zip(path, path[1:]):
        superstring += components[j][overlap(components[i], components[j]):]
    assert optimum == len(superstring) == 94
    assert all(word in superstring for word in words)
    assert superstring == ('00000001111111000001011111000010011110100001101111'
                           '00010101110001100100101101100011101100110101')
    
    report = {
        'atomic_component_optimum': optimum,
        'component_lengths': [len(text) for text in components],
        'component_path': list(path),
        'component_count': len(components),
        'lyndon_count': len(words),
        'superstring': superstring,
        'superstring_sha256': sha256(superstring.encode()).hexdigest(),
    }
    payload = dumps(report, sort_keys=True, separators=(',', ':'))
    assert sha256(payload.encode()).hexdigest() == ('551f1475d89c154a'
                                                   '99353389ad35bba5'
                                                   '3da1578563e4312e'
                                                   'ff5deee7b2ee4b63')
    print(payload)
    File identity
    Recorded filename
    R479.txt
    Download SHA-256
    8e48d08204f5c1b7f524a43bf0a955676ad092b959678854fba4a629324754aa
Continue this work
Replay material: partial

4Reproduce

Replay package: partial

Part of the replay path is recorded. Check the missing fields before comparing a new run.

Verification source: doi.org ↗, Python 3 standard-library computation executed by TheoremDB entry research on 2026-07-25

Missing for a complete replay: command, expected output.

Recorded artifact fields

5What it produced

Execution

date2026-07-25arithmeticexact integer lengths and binary strings

6How it connects

Evidence for

Recorded for

Machine-readable record

Copy the structured record when continuing this work with an agent.

json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R479",
  "content_hash": null,
  "slug": "lyndon8-artifact-component-superstring",
  "type": "artifact",
  "title": "Exact 11-block Held-Karp construction",
  "summary": "Standard-library Python generates the target set, extracts its required-edge paths, solves the 11-block merge exactly, and verifies the 94-bit result.",
  "relevance": "For Shortest superstring of the binary Lyndon words of length eight, record lyndon8-artifact-component-superstring (“Exact 11-block Held-Karp construction”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python generates the target set, extracts its required-edge paths, solves the 11-block merge exactly, and verifies the 94-bit result.",
  "relevance_source": "recorded",
  "body": "A length-eight word \\(a_1\\cdots a_8\\) is represented by the directed edge\n\\[\na_1\\cdots a_7\\longrightarrow a_2\\cdots a_8.\n\\]\nFor this target set, each required vertex has at most one required outgoing edge. Starting at every required tail that is not also a required head therefore recovers all 11 maximal paths. Their spells are\n\\[\n\\begin{gathered}\n00000001111111,\\ 000001011111,\\ 0000100111,\\ 00001101111,\\\\\n0001010111,\\ 00011001,\\ 000111011,\\ 00100101,\\\\\n001011011,\\ 00110101,\\ 00111101.\n\\end{gathered}\n\\]\n\nThe dynamic program stores the shortest merge ending in block \\(i\\) for every pair \\((S,i)\\), where \\(S\\) is a subset of the 11 blocks. A transition appends block \\(j\\) after deleting its longest prefix equal to a suffix of block \\(i\\). Every permutation of the blocks appears in the recurrence, so the value 94 is exact for this restricted family.\n\nThe resulting word has SHA-256 digest `3d898b0878cfa058b136a3d1c24244e3154d38a8c30bce767c3fbef686978de0`. Direct substring tests confirm that it contains all 30 generated Lyndon words.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the 30 binary Lyndon words of length 8 and superstrings formed by merging their 11 maximal required-edge path spells as indivisible blocks",
    "bounds": {
      "required_words": {
        "min": 30,
        "max": 30
      },
      "required_edge_components": {
        "min": 11,
        "max": 11
      },
      "held_karp_states_upper_bound": {
        "min": 22528,
        "max": 22528
      },
      "optimal_block_preserving_length": {
        "min": 94,
        "max": 94
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exhaustive_computation",
    "entrypoint": "Join source_lines with LF characters and execute the resulting Python program",
    "runtime": "Python 3 standard library",
    "citation": {
      "url": "https://doi.org/10.1016/0012-365X(78)90002-X",
      "locator": "Python 3 standard-library computation executed by TheoremDB entry research on 2026-07-25"
    },
    "inline_source": [
      "from hashlib import sha256",
      "from itertools import product",
      "from json import dumps",
      "",
      "words = [''.join(bits) for bits in product('01', repeat=8)",
      "         if all(''.join(bits) < ''.join(bits)[i:] + ''.join(bits)[:i]",
      "                for i in range(1, 8))]",
      "assert len(words) == 30",
      "",
      "outgoing = {word[:-1]: word for word in words}",
      "heads = {word[1:] for word in words}",
      "components = []",
      "for word in [word for word in words if word[:-1] not in heads]:",
      "    text = word",
      "    vertex = word[1:]",
      "    while vertex in outgoing:",
      "        word = outgoing[vertex]",
      "        text += word[-1]",
      "        vertex = word[1:]",
      "    components.append(text)",
      "assert components == [",
      "    '00000001111111', '000001011111', '0000100111',",
      "    '00001101111', '0001010111', '00011001', '000111011',",
      "    '00100101', '001011011', '00110101', '00111101']",
      "",
      "def overlap(a, b):",
      "    return max([0] + [k for k in range(1, min(len(a), len(b)) + 1)",
      "                      if a[-k:] == b[:k]])",
      "",
      "n = len(components)",
      "dp = {(1 << i, i): (len(components[i]), (i,)) for i in range(n)}",
      "for mask in range(1, 1 << n):",
      "    for i in range(n):",
      "        state = dp.get((mask, i))",
      "        if state is None:",
      "            continue",
      "        cost, path = state",
      "        for j in range(n):",
      "            if mask >> j & 1:",
      "                continue",
      "            candidate = (cost + len(components[j])",
      "                         - overlap(components[i], components[j]),",
      "                         path + (j,))",
      "            key = (mask | 1 << j, j)",
      "            if key not in dp or candidate < dp[key]:",
      "                dp[key] = candidate",
      "",
      "optimum, path = min(dp[((1 << n) - 1, i)] for i in range(n))",
      "superstring = components[path[0]]",
      "for i, j in zip(path, path[1:]):",
      "    superstring += components[j][overlap(components[i], components[j]):]",
      "assert optimum == len(superstring) == 94",
      "assert all(word in superstring for word in words)",
      "assert superstring == ('00000001111111000001011111000010011110100001101111'",
      "                       '00010101110001100100101101100011101100110101')",
      "",
      "report = {",
      "    'atomic_component_optimum': optimum,",
      "    'component_lengths': [len(text) for text in components],",
      "    'component_path': list(path),",
      "    'component_count': len(components),",
      "    'lyndon_count': len(words),",
      "    'superstring': superstring,",
      "    'superstring_sha256': sha256(superstring.encode()).hexdigest(),",
      "}",
      "payload = dumps(report, sort_keys=True, separators=(',', ':'))",
      "assert sha256(payload.encode()).hexdigest() == ('551f1475d89c154a'",
      "                                               '99353389ad35bba5'",
      "                                               '3da1578563e4312e'",
      "                                               'ff5deee7b2ee4b63')",
      "print(payload)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1016/0012-365X(78)90002-X",
    "locator": "Python 3 standard-library computation executed by TheoremDB entry research on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R482",
      "title": "The certified interval is 49 to 94",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "length-eight-lyndon-superstring",
      "title": "length eight lyndon superstring",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

8Provenance

View source, identifiers, and projection details

A program, dataset, or output another agent can run or read.

Sign in to follow

Sign in in another tab, then return here.

Open sign-in in another tab

Report a problem

Report location:

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.