{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R537",
  "content_hash": null,
  "slug": "mpb6-claim-exact-minimum-134",
  "type": "claim",
  "title": "The exact minimum is 134 nonterminal nodes",
  "summary": "A published table gives 136 nodes including the two sinks, and an exact subset dynamic program independently gives 134 internal nodes.",
  "relevance": "For Smallest variable-order OBDD for the middle bit of six-bit multiplication, record mpb6-claim-exact-minimum-134 (“The exact minimum is 134 nonterminal nodes”) records a bound, answer, status fact, or structural consequence. The record states: A published table gives 136 nodes including the two sinks, and an exact subset dynamic program independently gives 134 internal nodes.",
  "relevance_source": "recorded",
  "body": "The minimum is\n\\[\n\\boxed{134}\n\\]\nnonterminal nodes. One optimal variable order is\n\\[\ny_3,y_2,y_1,y_0,x_3,x_2,x_4,x_5,x_1,y_4,y_5,x_0.\n\\]\nThe numbers of nodes carrying those labels are\n\\[\n1,2,4,8,13,23,31,18,20,8,4,2,\n\\]\nwhose sum is 134.\n\nAmano's 2010 survey already records the exact small-width table. Its middle bit at operand width 6 is bit 5 under the candidate's zero-based convention. Figure 1 gives 136 as the minimum OBDD size at that width. Definition 1 counts every graph node, including the 0-sink and 1-sink. The middle-product function assumes both values, so both sinks occur. The convention in this candidate excludes them, giving \\(136-2=134\\). The same figure lists 156 total nodes for the quasi-reduced model, which keeps tests whose two children agree.\n\nThe executable certificate regenerates the truth table, evaluates every subset state in the Friedman-Supowit dynamic program, and obtains 134 across all \\(12!=479{,}001{,}600\\) orders. It finds 96 optimal orders. A separate bottom-up reduction builds the diagram for the displayed order and recounts its 134 nonterminal nodes.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "bounded",
    "statement": "the reduced ordered binary decision diagram for bit 5 of the product of two unsigned six-bit integers, minimized over all orders of its 12 input variables and counting nonterminal nodes only",
    "bounds": {
      "operand_width": {
        "min": 6,
        "max": 6
      },
      "output_bit_index": {
        "min": 5,
        "max": 5
      },
      "input_variables": {
        "min": 12,
        "max": 12
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://bulletin.eatcs.org/index.php/beatcs/article/download/181/176",
      "locator": "Kazuyuki Amano, Researching the Complexity of Boolean Functions with Computers, Bulletin of the EATCS 101 (June 2010), 64-91: Definition 1 on page 66 counts all nodes; Figure 1 and the exact dynamic-programming discussion on page 67 give minimum OBDD size 136 at operand width 6"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://bulletin.eatcs.org/index.php/beatcs/article/download/181/176",
    "locator": "Kazuyuki Amano, Researching the Complexity of Boolean Functions with Computers, Bulletin of the EATCS 101 (June 2010), 64-91: Definition 1 on page 66 counts all nodes; Figure 1 and the exact dynamic-programming discussion on page 67 give minimum OBDD size 136 at operand width 6"
  },
  "relations": [
    {
      "slug": "R536",
      "title": "Exact 4096-state optimal-order certificate",
      "object_type": "artifact",
      "relation": "reproduces",
      "direction": "incoming"
    },
    {
      "slug": "middle-product-bit-obdd-six",
      "title": "middle product bit obdd six",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}