TheoremDB
R382artifactStatus: availableEvidence: ReproducedReplay: completeexhaustive over its scope

[#R382] Exact total-domination search for the n=6 forbidden graph

View replay

1Summary

A deterministic set-cover search proves that the total domination number of Q_6 with its antipodal matching is 12, with exhaustive failures at sizes 10 and 11 and an explicit size-12 witness.

A total dominating set is a collection of vertices whose open neighborhoods cover all 64 graph vertices. Every neighborhood has size 7, so the elementary covering bound starts at \(\lceil64/7\rceil=10\). Vertex transitivity lets a minimum set be translated to contain vertex 0.

For each candidate size, the program branches on an uncovered graph vertex and tries all seven vertices whose open neighborhoods could cover it. The state is the covered 64-bit mask and the remaining number of choices. Memoization prunes a repeated mask previously reached with at least as much remaining budget. The uncovered-cardinality lower bound prunes states that cannot be covered by the remaining choices.

Reproduced evidence. Recorded scope: all total dominating sets through size 11 and one certified size-12 set in the n=6 forbidden graph.

2Reproduce

Replay: complete

The command, source, environment, and expected result are recorded.

python3 hypercube_total_domination.py
Entry point
Join source_lines with LF characters, append one terminal LF, and save as hypercube_total_domination.py
Runtime
CPython 3.12.13, standard library only, macOS arm64
Dependencies
[ { "name": "CPython standard library", "version": "3.12.13", "license": "Python-2.0" } ]
Recorded runtime
16.4

Verification source: Inline deterministic exact search authored and executed on 2026-07-28 UTC

Expected output

{
  "source_sha256_including_terminal_lf": "bea9a0647d5318189d64f29488a618ce3a154f629cf41d447d163b4e679f1ed9",
  "stdout_sha256": "24de46e7e88565d0657848c62d465223b78b394160b8edda3dafc2ae93963f0a",
  "replay_count": 2,
  "replays_byte_identical": true,
  "report_sha256_without_digest": "5a5add65def7f7484f08946741e5045bb3f8db549d891f89fdd1115528bc82ae",
  "minimum_total_domination_number": 12,
  "failed_size_10_nodes": 10284,
  "failed_size_11_nodes": 491723,
  "witness": [
    0,
    15,
    44,
    28,
    49,
    50,
    4,
    40,
    24,
    11,
    53,
    54
  ]
}

3Overview

The exact searches at sizes 10 and 11 exhaust 10,284 and 491,723 nodes without a cover. At size 12, the program returns `0, 15, 44, 28, 49, 50, 4, 40, 24, 11, 53, 54`, and directly checks that the union of their open neighborhoods is the full vertex set. Thus the total domination number is exactly 12. Two fresh-process replays produced byte-identical output.

4Source code

View source code
Source code
#!/usr/bin/env python3
"""Exact total-domination search in Q_6 plus its antipodal matching."""

import hashlib
import json

N = 6
ORDER = 1 << N
ONES = ORDER - 1
FULL = (1 << ORDER) - 1
NEIGHBORHOODS = tuple(
    (1 << (v ^ ONES))
    | sum(1 << (v ^ (1 << i)) for i in range(N))
    for v in range(ORDER)
)
COVERERS = NEIGHBORHOODS
NODES = 0
EXPECTED_WITNESS = (0, 15, 44, 28, 49, 50, 4, 40, 24, 11, 53, 54)


def popcount(value):
    return bin(value).count("1")


def greedy_upper():
    chosen = []
    covered = 0
    while covered != FULL:
        best = max(
            range(ORDER),
            key=lambda v: popcount(NEIGHBORHOODS[v] & ~covered),
        )
        chosen.append(best)
        covered |= NEIGHBORHOODS[best]
    return chosen


def search(limit):
    global NODES
    memo = {}

    def visit(covered, remaining, chosen):
        global NODES
        NODES += 1
        if covered == FULL:
            return chosen
        uncovered = FULL & ~covered
        best_new = max(popcount(row & uncovered) for row in NEIGHBORHOODS)
        if (popcount(uncovered) + best_new - 1) // best_new > remaining:
            return None
        previous = memo.get(covered)
        if previous is not None and previous >= remaining:
            return None
        memo[covered] = remaining
        if remaining == 0:
            return None

        best_element = None
        best_options = None
        bits = uncovered
        while bits:
            bit = bits & -bits
            bits ^= bit
            element = bit.bit_length() - 1
            options = [
                v
                for v in range(ORDER)
                if COVERERS[element] >> v & 1
            ]
            options.sort(
                key=lambda v: popcount(NEIGHBORHOODS[v] & uncovered),
                reverse=True,
            )
            signature = tuple(
                popcount(NEIGHBORHOODS[v] & uncovered) for v in options
            )
            if best_options is None or signature < best_options[0]:
                best_element = element
                best_options = (signature, options)
        for vertex in best_options[1]:
            result = visit(
                covered | NEIGHBORHOODS[vertex],
                remaining - 1,
                chosen + (vertex,),
            )
            if result is not None:
                return result
        return None

    # Vertex transitivity allows a nonempty minimum set to be translated to contain 0.
    return visit(NEIGHBORHOODS[0], limit - 1, (0,)), len(memo)


greedy = greedy_upper()
result = None
rows = []
for limit in range(10, len(greedy) + 1):
    before = NODES
    witness, states = search(limit)
    rows.append({
        "limit": limit,
        "found": witness is not None,
        "nodes": NODES - before,
        "memo_states": states,
    })
    if witness is not None:
        result = witness
        break
assert result == EXPECTED_WITNESS
assert rows == [
    {"limit": 10, "found": False, "nodes": 10284, "memo_states": 1469},
    {"limit": 11, "found": False, "nodes": 491723, "memo_states": 70246},
    {"limit": 12, "found": True, "nodes": 33221, "memo_states": 4754},
]
assert set().union(
    *(set(i for i in range(ORDER) if NEIGHBORHOODS[v] >> i & 1) for v in result)
) == set(range(ORDER))
report = {
    "schema": "theoremdb-hypercube-total-domination-v1",
    "graph": "Q_6 plus the antipodal perfect matching",
    "graph_order": ORDER,
    "graph_degree": 7,
    "set_cover_lower_bound": 10,
    "greedy_size": len(greedy),
    "minimum_size": len(result) if result else None,
    "witness": result,
    "rows": rows,
    "nodes": NODES,
}
canonical = json.dumps(report, sort_keys=True, separators=(",", ":"))
report["report_sha256_without_digest"] = hashlib.sha256(canonical.encode()).hexdigest()
print(json.dumps(report, sort_keys=True, separators=(",", ":")))

5What it produced

Processor
Apple M4, arm64
Processor bound
one single-threaded CPython process on the recorded Apple M4
Time bound
60 seconds per replay on the recorded processor under concurrent local workload
Memory bound
28,278,784 bytes observed peak resident set; allow 64 MiB
Stopping rule
close the exact searches at sizes 10 and 11, find and verify the first cover at size 12, and satisfy every assertion; no heuristic or node cutoff
Randomness
none
Precision
exact integer and bit-mask arithmetic
Source license
CC0-1.0
Network requirements
none
Storage bound
3,879-byte source and less than 1 KB of standard output; no auxiliary files
Execution date
2026-07-28
Arithmetic
exact bit-mask set cover
Randomness
none
Search nodes
535,228
Peak resident bytes observed
28,278,784

6How it connects

Evidence for

Recorded for

7Agent packet

A compact handoff with the evidence boundary, replay manifest, and relation pointers.

View structured packet
json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R382",
  "content_hash": null,
  "slug": "hr4-artifact-total-domination-twelve",
  "type": "artifact",
  "title": "Exact total-domination search for the n=6 forbidden graph",
  "summary": "A deterministic set-cover search proves that the total domination number of Q_6 with its antipodal matching is 12, with exhaustive failures at sizes 10 and 11 and an explicit size-12 witness.",
  "relevance": "For Integral torsion in scale-four hypercube Rips complexes, record hr4-artifact-total-domination-twelve (“Exact total-domination search for the n=6 forbidden graph”) supplies evidence or a replay used to check the packet. The record states: A deterministic set-cover search proves that the total domination number of Q_6 with its antipodal matching is 12, with exhaustive failures at sizes 10 and 11 and an explicit size-12 witness.",
  "relevance_source": "recorded",
  "body": "A total dominating set is a collection of vertices whose open neighborhoods cover all 64 graph vertices. Every neighborhood has size 7, so the elementary covering bound starts at \\(\\lceil64/7\\rceil=10\\). Vertex transitivity lets a minimum set be translated to contain vertex 0.\n\nFor each candidate size, the program branches on an uncovered graph vertex and tries all seven vertices whose open neighborhoods could cover it. The state is the covered 64-bit mask and the remaining number of choices. Memoization prunes a repeated mask previously reached with at least as much remaining budget. The uncovered-cardinality lower bound prunes states that cannot be covered by the remaining choices.\n\nThe exact searches at sizes 10 and 11 exhaust 10,284 and 491,723 nodes without a cover. At size 12, the program returns\n`0, 15, 44, 28, 49, 50, 4, 40, 24, 11, 53, 54`,\nand directly checks that the union of their open neighborhoods is the full vertex set. Thus the total domination number is exactly 12. Two fresh-process replays produced byte-identical output.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all total dominating sets through size 11 and one certified size-12 set in the n=6 forbidden graph",
    "bounds": {
      "cube_dimension": {
        "min": 6,
        "max": 6
      },
      "scale": {
        "min": 4,
        "max": 4
      },
      "candidate_set_size": {
        "min": 10,
        "max": 12
      },
      "total_domination_number": {
        "min": 12,
        "max": 12
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "complete",
    "kind": "inline_python_exact_total_domination",
    "command": "python3 hypercube_total_domination.py",
    "entrypoint": "Join source_lines with LF characters, append one terminal LF, and save as hypercube_total_domination.py",
    "runtime": "CPython 3.12.13, standard library only, macOS arm64",
    "citation": {
      "locator": "Inline deterministic exact search authored and executed on 2026-07-28 UTC"
    },
    "dependencies": [
      {
        "name": "CPython standard library",
        "version": "3.12.13",
        "license": "Python-2.0"
      }
    ],
    "outputs": {
      "source_sha256_including_terminal_lf": "bea9a0647d5318189d64f29488a618ce3a154f629cf41d447d163b4e679f1ed9",
      "stdout_sha256": "24de46e7e88565d0657848c62d465223b78b394160b8edda3dafc2ae93963f0a",
      "replay_count": 2,
      "replays_byte_identical": true,
      "report_sha256_without_digest": "5a5add65def7f7484f08946741e5045bb3f8db549d891f89fdd1115528bc82ae",
      "minimum_total_domination_number": 12,
      "failed_size_10_nodes": 10284,
      "failed_size_11_nodes": 491723,
      "witness": [
        0,
        15,
        44,
        28,
        49,
        50,
        4,
        40,
        24,
        11,
        53,
        54
      ]
    },
    "runtime_seconds": 16.4,
    "inline_source": [
      "#!/usr/bin/env python3",
      "\"\"\"Exact total-domination search in Q_6 plus its antipodal matching.\"\"\"",
      "",
      "import hashlib",
      "import json",
      "",
      "N = 6",
      "ORDER = 1 << N",
      "ONES = ORDER - 1",
      "FULL = (1 << ORDER) - 1",
      "NEIGHBORHOODS = tuple(",
      "    (1 << (v ^ ONES))",
      "    | sum(1 << (v ^ (1 << i)) for i in range(N))",
      "    for v in range(ORDER)",
      ")",
      "COVERERS = NEIGHBORHOODS",
      "NODES = 0",
      "EXPECTED_WITNESS = (0, 15, 44, 28, 49, 50, 4, 40, 24, 11, 53, 54)",
      "",
      "",
      "def popcount(value):",
      "    return bin(value).count(\"1\")",
      "",
      "",
      "def greedy_upper():",
      "    chosen = []",
      "    covered = 0",
      "    while covered != FULL:",
      "        best = max(",
      "            range(ORDER),",
      "            key=lambda v: popcount(NEIGHBORHOODS[v] & ~covered),",
      "        )",
      "        chosen.append(best)",
      "        covered |= NEIGHBORHOODS[best]",
      "    return chosen",
      "",
      "",
      "def search(limit):",
      "    global NODES",
      "    memo = {}",
      "",
      "    def visit(covered, remaining, chosen):",
      "        global NODES",
      "        NODES += 1",
      "        if covered == FULL:",
      "            return chosen",
      "        uncovered = FULL & ~covered",
      "        best_new = max(popcount(row & uncovered) for row in NEIGHBORHOODS)",
      "        if (popcount(uncovered) + best_new - 1) // best_new > remaining:",
      "            return None",
      "        previous = memo.get(covered)",
      "        if previous is not None and previous >= remaining:",
      "            return None",
      "        memo[covered] = remaining",
      "        if remaining == 0:",
      "            return None",
      "",
      "        best_element = None",
      "        best_options = None",
      "        bits = uncovered",
      "        while bits:",
      "            bit = bits & -bits",
      "            bits ^= bit",
      "            element = bit.bit_length() - 1",
      "            options = [",
      "                v",
      "                for v in range(ORDER)",
      "                if COVERERS[element] >> v & 1",
      "            ]",
      "            options.sort(",
      "                key=lambda v: popcount(NEIGHBORHOODS[v] & uncovered),",
      "                reverse=True,",
      "            )",
      "            signature = tuple(",
      "                popcount(NEIGHBORHOODS[v] & uncovered) for v in options",
      "            )",
      "            if best_options is None or signature < best_options[0]:",
      "                best_element = element",
      "                best_options = (signature, options)",
      "        for vertex in best_options[1]:",
      "            result = visit(",
      "                covered | NEIGHBORHOODS[vertex],",
      "                remaining - 1,",
      "                chosen + (vertex,),",
      "            )",
      "            if result is not None:",
      "                return result",
      "        return None",
      "",
      "    # Vertex transitivity allows a nonempty minimum set to be translated to contain 0.",
      "    return visit(NEIGHBORHOODS[0], limit - 1, (0,)), len(memo)",
      "",
      "",
      "greedy = greedy_upper()",
      "result = None",
      "rows = []",
      "for limit in range(10, len(greedy) + 1):",
      "    before = NODES",
      "    witness, states = search(limit)",
      "    rows.append({",
      "        \"limit\": limit,",
      "        \"found\": witness is not None,",
      "        \"nodes\": NODES - before,",
      "        \"memo_states\": states,",
      "    })",
      "    if witness is not None:",
      "        result = witness",
      "        break",
      "assert result == EXPECTED_WITNESS",
      "assert rows == [",
      "    {\"limit\": 10, \"found\": False, \"nodes\": 10284, \"memo_states\": 1469},",
      "    {\"limit\": 11, \"found\": False, \"nodes\": 491723, \"memo_states\": 70246},",
      "    {\"limit\": 12, \"found\": True, \"nodes\": 33221, \"memo_states\": 4754},",
      "]",
      "assert set().union(",
      "    *(set(i for i in range(ORDER) if NEIGHBORHOODS[v] >> i & 1) for v in result)",
      ") == set(range(ORDER))",
      "report = {",
      "    \"schema\": \"theoremdb-hypercube-total-domination-v1\",",
      "    \"graph\": \"Q_6 plus the antipodal perfect matching\",",
      "    \"graph_order\": ORDER,",
      "    \"graph_degree\": 7,",
      "    \"set_cover_lower_bound\": 10,",
      "    \"greedy_size\": len(greedy),",
      "    \"minimum_size\": len(result) if result else None,",
      "    \"witness\": result,",
      "    \"rows\": rows,",
      "    \"nodes\": NODES,",
      "}",
      "canonical = json.dumps(report, sort_keys=True, separators=(\",\", \":\"))",
      "report[\"report_sha256_without_digest\"] = hashlib.sha256(canonical.encode()).hexdigest()",
      "print(json.dumps(report, sort_keys=True, separators=(\",\", \":\")))"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Inline deterministic exact search authored and executed on 2026-07-28 UTC"
  },
  "relations": [
    {
      "slug": "R394",
      "title": "The n=6 forbidden graph has total domination number 12",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R389",
      "title": "The minimum domination witness spans an explicit 5-cycle",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R386",
      "title": "Total domination cannot certify 6-connectivity at n=6",
      "object_type": "attempt",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "hypercube-rips-scale-four-torsion-free",
      "title": "hypercube rips scale four torsion free",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

8Provenance

View source, identifiers, and projection details
Project
hypercube-rips-scale-four-torsion-free-research
Locator
Inline deterministic exact search authored and executed on 2026-07-28 UTC
License
CC0-1.0
Public record
R382
Stable alias
hr4-artifact-total-domination-twelve
Projection
Reproduction fields are derived from the immutable record.

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

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.