{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R536",
  "content_hash": null,
  "slug": "mpb6-artifact-subset-dp-and-obdd",
  "type": "artifact",
  "title": "Exact 4096-state optimal-order certificate",
  "summary": "Standard-library Python applies the Friedman-Supowit recurrence to all variable subsets and verifies an optimal diagram by direct reduction.",
  "relevance": "For Smallest variable-order OBDD for the middle bit of six-bit multiplication, record mpb6-artifact-subset-dp-and-obdd (“Exact 4096-state optimal-order certificate”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python applies the Friedman-Supowit recurrence to all variable subsets and verifies an optimal diagram by direct reduction.",
  "relevance_source": "recorded",
  "body": "For a set \\(S\\) of variables already tested, let \\(R_S\\) be the set of distinct residual Boolean functions obtained by assigning every variable in \\(S\\). For \\(v\\notin S\\), define\n\\[\nc(S,v)=\\#\\{g\\in R_S:g|_{v=0}\\ne g|_{v=1}\\}.\n\\]\nWhen an order has prefix set \\(S\\) and tests \\(v\\) next, its reduced OBDD has exactly \\(c(S,v)\\) nodes labeled \\(v\\). Equal residual functions merge, and a residual independent of \\(v\\) suppresses that test. This count depends on the set \\(S\\) and the next variable \\(v\\).\n\nThe dynamic program is\n\\[\nD(\\varnothing)=0,\\qquad\nD(T)=\\min_{v\\in T}\\bigl(D(T\\setminus\\{v\\})+c(T\\setminus\\{v\\},v)\\bigr).\n\\]\nChoosing the final variable in each prefix proves by induction that \\(D(T)\\) is the least node count contributed by the variables in \\(T\\). Thus \\(D(V)\\) minimizes over every complete order. The replay gets \\(D(V)=134\\), with 96 minimizing orders.\n\nThe program stores each residual truth table as an exact Python integer. Across all 4,096 subsets it encounters 221,737 distinct residual instances. It also constructs a canonical reduced diagram for one optimal order by merging equal child pairs and suppressing equal children. The direct build has 134 nonterminal nodes. Hashes cover the truth table, the complete cost array, the dynamic-programming array, all 96 optimal orders, and the rebuilt diagram. The canonical report has SHA-256 digest `dfb779421d8f11b9661b6c040165246c83c49a286b9ccc0908fec204cf5636a1`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all 4096 subsets of the 12 input variables and the induced coverage of all 12-factorial variable orders for the stated six-bit middle-product function",
    "bounds": {
      "operand_width": {
        "min": 6,
        "max": 6
      },
      "output_bit_index": {
        "min": 5,
        "max": 5
      },
      "subset_states": {
        "min": 4096,
        "max": 4096
      },
      "variable_orders_covered": {
        "min": 479001600,
        "max": 479001600
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_computation",
    "entrypoint": "join source_lines with newline and run with python3",
    "runtime": "CPython 3, standard library only",
    "citation": {
      "url": "https://www.cs.york.ac.uk/rts/docs/DAC-1964-2006/PAPERS/1987/DAC87_348.PDF",
      "locator": "Steven J. Friedman and Kenneth J. Supowit, Finding the Optimal Variable Ordering for Binary Decision Diagrams, 24th ACM/IEEE Design Automation Conference (1987), Section 2 lemma and Section 3 algorithm; journal version, IEEE Transactions on Computers 39(5), 710-713 (1990), DOI 10.1109/12.53586"
    },
    "inline_source": [
      "from collections import Counter",
      "from hashlib import sha256",
      "from json import dumps",
      "from struct import pack",
      "N=12",
      "ALL=(1<<N)-1",
      "names=[f'x{i}' for i in range(6)]+[f'y{i}' for i in range(6)]",
      "def popcount(x):",
      "    return bin(x).count('1')",
      "def cofactors(bits,width,pos):",
      "    block=1<<pos",
      "    mask=(1<<block)-1",
      "    low=high=out=0",
      "    for base in range(0,width,2*block):",
      "        low|=((bits>>base)&mask)<<out",
      "        high|=((bits>>(base+block))&mask)<<out",
      "        out+=block",
      "    return low,high",
      "truth=sum(((((a&63)*((a>>6)&63))>>5)&1)<<a for a in range(1<<N))",
      "truth_sha=sha256(truth.to_bytes(1<<(N-3),'little')).hexdigest()",
      "assert truth_sha=='9b6a7a15d2450265125ff2d0882f989c169ad27b5f22ac15faf1a9845b9d4be9'",
      "residuals=[None]*(1<<N)",
      "residuals[0]={truth}",
      "cost=[[0]*N for _ in residuals]",
      "for assigned in range(1<<N):",
      "    if assigned:",
      "        bit=assigned&-assigned",
      "        variable=bit.bit_length()-1",
      "        parent=assigned^bit",
      "        width=1<<(N-popcount(parent))",
      "        pos=variable-popcount(parent&((1<<variable)-1))",
      "        values=set()",
      "        for function in residuals[parent]:",
      "            values.update(cofactors(function,width,pos))",
      "        residuals[assigned]=values",
      "    width=1<<(N-popcount(assigned))",
      "    for variable in range(N):",
      "        if not (assigned>>variable)&1:",
      "            pos=variable-popcount(assigned&((1<<variable)-1))",
      "            cost[assigned][variable]=sum(low!=high for low,high in (cofactors(function,width,pos) for function in residuals[assigned]))",
      "residual_level_totals=[sum(len(residuals[s]) for s in range(1<<N) if popcount(s)==k) for k in range(N+1)]",
      "residual_level_maxima=[max(len(residuals[s]) for s in range(1<<N) if popcount(s)==k) for k in range(N+1)]",
      "assert residual_level_totals==[1,24,262,1718,7515,22962,49262,70280,54413,14386,864,48,2]",
      "assert residual_level_maxima==[1,2,4,8,16,32,64,128,232,172,16,4,2]",
      "cost_sha=sha256(b''.join(pack('<H',value) for row in cost for value in row)).hexdigest()",
      "assert cost_sha=='72c67d76d3ba423ec4f22f25ab9cab1de7a8dec2b2715c9a8facaa518e1ecd00'",
      "infinity=10**9",
      "best=[infinity]*(1<<N)",
      "ways=[0]*(1<<N)",
      "best[0]=0",
      "ways[0]=1",
      "for assigned in range(1,1<<N):",
      "    for variable in range(N):",
      "        if (assigned>>variable)&1:",
      "            parent=assigned^(1<<variable)",
      "            candidate=best[parent]+cost[parent][variable]",
      "            if candidate<best[assigned]:",
      "                best[assigned]=candidate",
      "                ways[assigned]=ways[parent]",
      "            elif candidate==best[assigned]:",
      "                ways[assigned]+=ways[parent]",
      "def optimal_orders(assigned):",
      "    if assigned==0:",
      "        yield ()",
      "        return",
      "    for variable in range(N):",
      "        if (assigned>>variable)&1:",
      "            parent=assigned^(1<<variable)",
      "            if best[assigned]==best[parent]+cost[parent][variable]:",
      "                for prefix in optimal_orders(parent):",
      "                    yield prefix+(variable,)",
      "orders=sorted(optimal_orders(ALL))",
      "order_text='\\n'.join(','.join(names[v] for v in order) for order in orders)+'\\n'",
      "chosen_names=('y3','y2','y1','y0','x3','x2','x4','x5','x1','y4','y5','x0')",
      "chosen=tuple(names.index(name) for name in chosen_names)",
      "assert best[ALL]==134 and ways[ALL]==len(orders)==96 and chosen in orders",
      "best_sha=sha256(b''.join(pack('<H',value) for value in best)).hexdigest()",
      "orders_sha=sha256(order_text.encode()).hexdigest()",
      "assert best_sha=='4c03c576d049c5b97b9ee7be99c8006ab0a6839406d4dc89f58bcb39e6fdce38'",
      "assert orders_sha=='fd6f7bc48ca7bba13618840e11d2ab63d6a4767a9e40c2a1acb028e426977845'",
      "permuted=0",
      "for packed_assignment in range(1<<N):",
      "    original_assignment=sum(((packed_assignment>>i)&1)<<v for i,v in enumerate(chosen))",
      "    permuted|=((truth>>original_assignment)&1)<<packed_assignment",
      "def split_first(bits,width):",
      "    low=high=0",
      "    for i in range(width//2):",
      "        low|=((bits>>(2*i))&1)<<i",
      "        high|=((bits>>(2*i+1))&1)<<i",
      "    return low,high",
      "unique={}",
      "nodes=[]",
      "by_level=Counter()",
      "calls=0",
      "def build(bits,depth):",
      "    global calls",
      "    calls+=1",
      "    width=1<<(N-depth)",
      "    if bits==0:",
      "        return 0",
      "    if bits==(1<<width)-1:",
      "        return 1",
      "    low_bits,high_bits=split_first(bits,width)",
      "    low=build(low_bits,depth+1)",
      "    high=build(high_bits,depth+1)",
      "    if low==high:",
      "        return low",
      "    key=(depth,low,high)",
      "    if key not in unique:",
      "        node_id=len(nodes)+2",
      "        unique[key]=node_id",
      "        nodes.append(key)",
      "        by_level[depth]+=1",
      "    return unique[key]",
      "root=build(permuted,0)",
      "level_nodes=[by_level[i] for i in range(N)]",
      "prefix=0",
      "level_cost=[]",
      "for variable in chosen:",
      "    level_cost.append(cost[prefix][variable])",
      "    prefix|=1<<variable",
      "assert root==135 and len(nodes)==sum(level_nodes)==sum(level_cost)==134",
      "assert level_nodes==level_cost==[1,2,4,8,13,23,31,18,20,8,4,2]",
      "obdd_sha=sha256(b''.join(pack('<BHH',*node) for node in nodes)).hexdigest()",
      "assert obdd_sha=='3e411adf0378b5db69206ed60fbf757ad202b824ed4450fd33cac311fb3c4e63'",
      "report={'variables':N,'raw_orders':479001600,'subset_states':1<<N,'truth_table_sha256':truth_sha,'residual_function_instances':sum(map(len,residuals)),'residual_level_totals':residual_level_totals,'residual_level_maxima':residual_level_maxima,'cost_table_sha256':cost_sha,'dp_table_sha256':best_sha,'minimum_nonterminal_nodes':best[ALL],'optimal_order_count':len(orders),'optimal_orders_sha256':orders_sha,'chosen_order':chosen_names,'chosen_level_nodes':level_nodes,'direct_obdd_nodes':len(nodes),'direct_obdd_root_id':root,'direct_obdd_build_calls':calls,'direct_obdd_sha256':obdd_sha}",
      "payload=dumps(report,sort_keys=True,separators=(',',':'))",
      "assert sha256(payload.encode()).hexdigest()=='dfb779421d8f11b9661b6c040165246c83c49a286b9ccc0908fec204cf5636a1'",
      "print(payload)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://www.cs.york.ac.uk/rts/docs/DAC-1964-2006/PAPERS/1987/DAC87_348.PDF",
    "locator": "Steven J. Friedman and Kenneth J. Supowit, Finding the Optimal Variable Ordering for Binary Decision Diagrams, 24th ACM/IEEE Design Automation Conference (1987), Section 2 lemma and Section 3 algorithm; journal version, IEEE Transactions on Computers 39(5), 710-713 (1990), DOI 10.1109/12.53586"
  },
  "models": [],
  "relations": [
    {
      "slug": "R537",
      "title": "The exact minimum is 134 nonterminal nodes",
      "object_type": "claim",
      "relation": "reproduces",
      "direction": "outgoing"
    },
    {
      "slug": "middle-product-bit-obdd-six",
      "title": "middle product bit obdd six",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}