{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R480",
  "content_hash": null,
  "slug": "lyndon8-artifact-unsat-at-48",
  "type": "artifact",
  "title": "Boolean unsatisfiability certificate at length 48",
  "summary": "A direct encoding of every possible target placement is unsatisfiable under Z3 5.0.0.",
  "relevance": "For Shortest superstring of the binary Lyndon words of length eight, record lyndon8-artifact-unsat-at-48 (“Boolean unsatisfiability certificate at length 48”) supplies evidence or a replay used to check the packet. The record states: A direct encoding of every possible target placement is unsatisfiable under Z3 5.0.0.",
  "relevance_source": "recorded",
  "body": "The encoding has 48 Boolean variables \\(b_0,\\ldots,b_{47}\\). For every target word \\(w\\), it asserts\n\\[\n\\bigvee_{p=0}^{40}\\ \\bigwedge_{j=0}^{7}(b_{p+j}=w_j).\n\\]\nThere are 30 target constraints, 1,230 placement terms, and 9,840 bit equalities before internal solver simplification. Any satisfying assignment directly spells a 48-bit common superstring. Conversely, every such superstring supplies a satisfying assignment. The solver returns `unsat`.\n\nThis is a solver-assisted exhaustive result. The artifact regenerates the 30 targets and the full formula, so it does not depend on a stored target list or a heuristic search. A separately checkable DRAT or LFSC proof was not retained.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all binary words of length 48 tested as possible common superstrings through an equisatisfiable Boolean formula",
    "bounds": {
      "proposed_superstring_length": {
        "min": 48,
        "max": 48
      },
      "Boolean_variables": {
        "min": 48,
        "max": 48
      },
      "target_placement_terms": {
        "min": 1230,
        "max": 1230
      },
      "bit_equalities": {
        "min": 9840,
        "max": 9840
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_solver_computation",
    "entrypoint": "Join source_lines with LF characters and execute the resulting Python program",
    "runtime": "CPython 3 with z3-solver 5.0.0",
    "citation": {
      "url": "https://github.com/Z3Prover/z3/tree/1c899374739f7c1cdbe6ba72dd61aa1d7daaee27",
      "locator": "Direct Z3 5.0.0 computation executed by TheoremDB entry research on 2026-07-25"
    },
    "inline_source": [
      "from hashlib import sha256",
      "from itertools import product",
      "from json import dumps",
      "import z3",
      "",
      "length = 48",
      "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",
      "bits = [z3.Bool(f'b{i}') for i in range(length)]",
      "solver = z3.Solver()",
      "for word in words:",
      "    placements = []",
      "    for start in range(length - 7):",
      "        placements.append(z3.And(*[",
      "            bits[start + j] if digit == '1' else z3.Not(bits[start + j])",
      "            for j, digit in enumerate(word)]))",
      "    solver.add(z3.Or(*placements))",
      "assert len(solver.assertions()) == 30",
      "result = solver.check()",
      "assert result == z3.unsat",
      "report = {",
      "    'bit_equalities': len(words) * (length - 7) * 8,",
      "    'certified_lower_bound': length + 1,",
      "    'checked_length': length,",
      "    'lyndon_count': len(words),",
      "    'placement_terms': len(words) * (length - 7),",
      "    'result': str(result),",
      "}",
      "payload = dumps(report, sort_keys=True, separators=(',', ':'))",
      "assert sha256(payload.encode()).hexdigest() == ('0c19ebaa2cfa2cfe'",
      "                                               '1ea326c14b975e6c'",
      "                                               '55e6920bb280ffc0'",
      "                                               'd7209a528770d7b6')",
      "print(payload)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://github.com/Z3Prover/z3/tree/1c899374739f7c1cdbe6ba72dd61aa1d7daaee27",
    "locator": "Direct Z3 5.0.0 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"
    }
  ]
}