{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R136",
  "content_hash": null,
  "slug": "cdt6-artifact-isomorphism-dp-certificate",
  "type": "artifact",
  "title": "Isomorphism-reduced optimal-policy and lower-bound certificate",
  "summary": "Standard C++ evaluates the exact recurrence, checks all stored lower bounds, and replays the optimal policy.",
  "relevance": "For Leaf complexity of six-vertex graph connectivity, record cdt6-artifact-isomorphism-dp-certificate (“Isomorphism-reduced optimal-policy and lower-bound certificate”) supplies evidence or a replay used to check the packet. The record states: Standard C++ evaluates the exact recurrence, checks all stored lower bounds, and replays the optimal policy.",
  "relevance_source": "recorded",
  "body": "Edges use the order `01,02,03,04,05,12,13,14,15,23,24,25,34,35,45`. A canonical state key is `present_mask | (absent_mask << 15)`, minimized over all 720 vertex permutations. Each certificate row is\n```\ncanonical_key,value,choice\n```\nwhere `choice` is an edge index in the canonical labeling and `-1` marks a terminal state.\n\nThe default run solves the recurrence and then verifies the certificate locally. At a nonterminal record, every unknown edge must have a certified child sum at least as large as the record's value. The stored choice must attain equality. A branch-and-bound shortcut may omit a present-edge child only when the already certified absent-edge child reaches the record value by itself, since the omitted child contributes at least one leaf. Terminal records are checked directly by connectivity of the present graph or disconnection of the maximal possible graph.\n\nThe program then follows the stored choices to replay an upper-bound policy with 1,693 leaves. Passing `--dump-certificate` emits all 23,352 sorted rows. That stream has SHA-256 digest `1229da5ce8044b6f3a7a1062182b46c433540fc82e452015c25d6bc24b0ffcdf`. This table is a matching lower certificate and a reconstructible optimal policy.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all partial assignments of the 15 edges on six labeled vertices that are needed by the exact recurrence certificate",
    "bounds": {
      "vertices": {
        "min": 6,
        "max": 6
      },
      "possible_edges": {
        "min": 15,
        "max": 15
      },
      "canonical_certificate_states": {
        "min": 23352,
        "max": 23352
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_cpp_computation",
    "entrypoint": "join source_lines with newline, save as check.cpp, compile with c++ -O3 -std=c++17 check.cpp -o check, run ./check, and run ./check --dump-certificate | shasum -a 256",
    "runtime": "C++17 standard library",
    "citation": {
      "url": "https://doi.org/10.1145/3564246.3585199",
      "locator": "C++17 source below, compiled and executed 2026-07-24"
    },
    "outputs": "L6=1693\ncanonical_states=23352 internal=14433 terminal=8919\npolicy_leaves=1693 root_query=01\nsolver_calls=146434 branches=82096 prunes=17759\ncertificate_fnv1a64=2fe1c127a59f5a08\n",
    "inline_source": [
      "#include <algorithm>",
      "#include <array>",
      "#include <cassert>",
      "#include <cstdint>",
      "#include <cstdio>",
      "#include <string>",
      "#include <unordered_map>",
      "#include <utility>",
      "#include <vector>",
      "using namespace std;",
      "constexpr int N=6, M=15, SPACE=1<<M, ALL=SPACE-1;",
      "int edge_u[M], edge_v[M], edge_index[N][N];",
      "array<uint8_t,SPACE> is_connected;",
      "vector<array<int,N>> permutations;",
      "vector<uint16_t> permuted_mask;",
      "struct Node { uint16_t value; int8_t choice; };",
      "unordered_map<uint32_t,Node> certificate;",
      "uint64_t calls=0, branches=0, prunes=0;",
      "",
      "bool connected(uint16_t mask) {",
      "    int parent[N];",
      "    for (int i=0;i<N;i++) parent[i]=i;",
      "    auto root = [&](int x) {",
      "        while (parent[x]!=x) { parent[x]=parent[parent[x]]; x=parent[x]; }",
      "        return x;",
      "    };",
      "    for (int e=0;e<M;e++) if ((mask>>e)&1) {",
      "        int a=root(edge_u[e]), b=root(edge_v[e]);",
      "        if (a!=b) parent[a]=b;",
      "    }",
      "    int r=root(0);",
      "    for (int i=1;i<N;i++) if (root(i)!=r) return false;",
      "    return true;",
      "}",
      "",
      "uint32_t canonical_key(uint16_t present,uint16_t absent) {",
      "    uint32_t best=UINT32_MAX;",
      "    for (size_t pi=0;pi<permutations.size();pi++) {",
      "        size_t offset=pi*SPACE;",
      "        uint32_t key=uint32_t(permuted_mask[offset+present]) |",
      "                     (uint32_t(permuted_mask[offset+absent])<<M);",
      "        if (key<best) best=key;",
      "    }",
      "    return best;",
      "}",
      "",
      "uint16_t solve(uint16_t present,uint16_t absent) {",
      "    calls++;",
      "    uint32_t key=canonical_key(present,absent);",
      "    auto found=certificate.find(key);",
      "    if (found!=certificate.end()) return found->second.value;",
      "    present=key&ALL; absent=key>>M;",
      "    if (is_connected[present] || !is_connected[ALL^absent]) {",
      "        certificate.emplace(key,Node{1,-1});",
      "        return 1;",
      "    }",
      "    uint16_t unknown=ALL^(present|absent), best=UINT16_MAX;",
      "    int best_edge=-1;",
      "    while (unknown) {",
      "        int e=__builtin_ctz(unknown);",
      "        unknown&=unknown-1;",
      "        branches++;",
      "        uint16_t zero=solve(present,absent|(1<<e));",
      "        if (zero>=best) { prunes++; continue; }",
      "        uint16_t one=solve(present|(1<<e),absent);",
      "        uint16_t sum=zero+one;",
      "        if (sum<best) { best=sum; best_edge=e; }",
      "    }",
      "    assert(best_edge>=0);",
      "    certificate.emplace(key,Node{best,(int8_t)best_edge});",
      "    return best;",
      "}",
      "",
      "const Node& get_node(uint16_t present,uint16_t absent) {",
      "    auto found=certificate.find(canonical_key(present,absent));",
      "    assert(found!=certificate.end());",
      "    return found->second;",
      "}",
      "",
      "uint16_t replay_policy(uint16_t present,uint16_t absent) {",
      "    uint32_t key=canonical_key(present,absent);",
      "    const Node &node=certificate.at(key);",
      "    present=key&ALL; absent=key>>M;",
      "    if (node.choice<0) return 1;",
      "    int e=node.choice;",
      "    return replay_policy(present,absent|(1<<e))+",
      "           replay_policy(present|(1<<e),absent);",
      "}",
      "",
      "void build_tables() {",
      "    int e=0;",
      "    for (int u=0;u<N;u++) for (int v=u+1;v<N;v++) {",
      "        edge_u[e]=u; edge_v[e]=v; edge_index[u][v]=edge_index[v][u]=e++;",
      "    }",
      "    array<int,N> p={0,1,2,3,4,5};",
      "    do { permutations.push_back(p); } while (next_permutation(p.begin(),p.end()));",
      "    permuted_mask.resize(permutations.size()*SPACE);",
      "    for (size_t pi=0;pi<permutations.size();pi++) {",
      "        size_t offset=pi*SPACE;",
      "        for (int mask=1;mask<SPACE;mask++) {",
      "            int e0=__builtin_ctz(mask), rest=mask&(mask-1);",
      "            int u=permutations[pi][edge_u[e0]];",
      "            int v=permutations[pi][edge_v[e0]];",
      "            permuted_mask[offset+mask]=permuted_mask[offset+rest] | (1<<edge_index[u][v]);",
      "        }",
      "    }",
      "    for (int mask=0;mask<SPACE;mask++) is_connected[mask]=connected(mask);",
      "}",
      "",
      "int main(int argc,char **argv) {",
      "    build_tables();",
      "    certificate.reserve(30000);",
      "    uint16_t answer=solve(0,0);",
      "    assert(answer==1693);",
      "    vector<pair<uint32_t,Node>> rows(certificate.begin(),certificate.end());",
      "    sort(rows.begin(),rows.end(),[](const auto& x,const auto& y){return x.first<y.first;});",
      "    size_t terminal_count=0, internal_count=0;",
      "    for (const auto &record:rows) {",
      "        uint32_t key=record.first;",
      "        const Node &node=record.second;",
      "        uint16_t present=key&ALL, absent=key>>M;",
      "        bool terminal=is_connected[present] || !is_connected[ALL^absent];",
      "        if (terminal) {",
      "            assert(node.value==1 && node.choice==-1);",
      "            terminal_count++;",
      "            continue;",
      "        }",
      "        internal_count++;",
      "        assert(node.choice>=0 && ((present|absent)&(1<<node.choice))==0);",
      "        bool choice_attains=false;",
      "        uint16_t unknown=ALL^(present|absent);",
      "        while (unknown) {",
      "            int e=__builtin_ctz(unknown);",
      "            unknown&=unknown-1;",
      "            uint16_t zero=get_node(present,absent|(1<<e)).value;",
      "            if (zero>=node.value) { assert(e!=node.choice); continue; }",
      "            uint16_t one=get_node(present|(1<<e),absent).value;",
      "            assert(zero+one>=node.value);",
      "            if (e==node.choice) {",
      "                assert(zero+one==node.value);",
      "                choice_attains=true;",
      "            }",
      "        }",
      "        assert(choice_attains);",
      "    }",
      "    uint16_t replayed=replay_policy(0,0);",
      "    assert(replayed==answer && certificate.at(0).choice==0);",
      "    uint64_t fnv=14695981039346656037ULL;",
      "    for (const auto &record:rows) {",
      "        char line[64];",
      "        int length=snprintf(line,sizeof(line),\"%u,%u,%d\\n\",record.first,record.second.value,int(record.second.choice));",
      "        for (int i=0;i<length;i++) { fnv^=uint8_t(line[i]); fnv*=1099511628211ULL; }",
      "    }",
      "    if (argc==2 && string(argv[1])==\"--dump-certificate\") {",
      "        for (const auto &record:rows)",
      "            printf(\"%u,%u,%d\\n\",record.first,record.second.value,int(record.second.choice));",
      "        return 0;",
      "    }",
      "    assert(argc==1);",
      "    printf(\"L6=%u\\n\",answer);",
      "    printf(\"canonical_states=%zu internal=%zu terminal=%zu\\n\",rows.size(),internal_count,terminal_count);",
      "    printf(\"policy_leaves=%u root_query=01\\n\",replayed);",
      "    printf(\"solver_calls=%llu branches=%llu prunes=%llu\\n\",(unsigned long long)calls,(unsigned long long)branches,(unsigned long long)prunes);",
      "    printf(\"certificate_fnv1a64=%016llx\\n\",(unsigned long long)fnv);",
      "}"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1145/3564246.3585199",
    "locator": "C++17 source below, compiled and executed 2026-07-24"
  },
  "models": [],
  "relations": [
    {
      "slug": "R138",
      "title": "The minimum decision-tree leaf count is 1,693",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "connectivity-decision-tree-six-leaves",
      "title": "connectivity decision tree six leaves",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}