# P2572: Smallest variable-order OBDD for the middle bit of six-bit multiplication

- ID: `P2572`
- Reference: `middle-product-bit-obdd-six`
- Page: https://theoremdb.org/statements/P2572
- Record maturity: Reviewed problem with recorded work

## Problem

Let \(X=\sum_{i=0}^5 2^i x_i\), \(Y=\sum_{i=0}^5 2^i y_i\), and \(f(x,y)=\lfloor XY/2^5\rfloor\bmod 2\). What is the minimum number of nonterminal nodes in a reduced ordered binary decision diagram for \(f\), minimized over all \(12!\) variable orders?

### Remarks

- **Remark.** A reduced OBDD merges isomorphic subgraphs and suppresses a test whose two children agree.
- **Remark.** The two terminal nodes are excluded from the node count.

### What counts as a solution

- Give an order and its reduced OBDD together with a certificate that every variable order needs at least as many nonterminal nodes.

## The answer

A published table gives 136 nodes including the two sinks, and an exact subset dynamic program independently gives 134 internal nodes. [1](#reference-1)

**Review status:** Reproduced.

**Lean verification:** not Lean-verified.

### Verification

The minimum is
\[
\boxed{134}
\]
nonterminal nodes. One optimal variable order is
\[
y_3,y_2,y_1,y_0,x_3,x_2,x_4,x_5,x_1,y_4,y_5,x_0.
\]
The numbers of nodes carrying those labels are
\[
1,2,4,8,13,23,31,18,20,8,4,2,
\]
whose sum is 134.

Amano'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.

The 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.

## Work

### Proof and evidence for the resolution

**Computation 1 (The exact minimum is 134 nonterminal nodes).** A published table gives 136 nodes including the two sinks, and an exact subset dynamic program independently gives 134 internal nodes.

The minimum is
\[
\boxed{134}
\]
nonterminal nodes. One optimal variable order is
\[
y_3,y_2,y_1,y_0,x_3,x_2,x_4,x_5,x_1,y_4,y_5,x_0.
\]
The numbers of nodes carrying those labels are
\[
1,2,4,8,13,23,31,18,20,8,4,2,
\]
whose sum is 134.

Amano'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.

The 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.

### Background and intake notes

The current upper bound is 140 nodes. The optimization has 479001600 raw orders, while every completed order can be independently recounted from its residual truth tables.

- Original intake status: Status unknown. OBDD lower bounds for multiplication are classical, while the exact six-bit optimum may appear in synthesis tables.
- Each variable order has a unique reduced OBDD, so its node count is an exact, memoizable objective. Reversal, operand exchange, and bit symmetries should be quotiented before branching.
- A lower certificate can store the best attainable residual-function partitions for each order prefix rather than all complete diagrams.

- Recorded example: The order y_0,y_1,y_2,y_3,x_3,x_2,x_4,x_5,x_0,y_4,y_5,x_1 gives a 140-node reduced OBDD.

### Runnable artifacts

- **Artifact 1** (reproduced): Standard-library Python applies the Friedman-Supowit recurrence to all variable subsets and verifies an optimal diagram by direct reduction. [2](#reference-2)

### Computational notes

- Exhaustive enumeration of every variable order gave exact minima 2, 6, 12, and 29 nodes for operand widths 1, 2, 3, and 4. Twenty thousand seeded orders at width 5 found 61 nodes, and twenty thousand at width 6 found the stated 140-node order; direct bottom-up reduction verified that node count.

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `middle-product-bit-obdd-six`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome.

## Lean verification

An informal proof is recorded. A Lean formalization still needs to be attached.

[Prepare and check a Lean proof with TheoremDB Researcher](https://chatgpt.com/g/g-6a6c206c5acc8191b184bb55fb72c5b3-theoremdb-researcher?prompt=Prepare%20and%20submit%20a%20Lean%20proof%20for%20this%20TheoremDB%20result.%0A%0AExact%20problem_ref%3A%20middle-product-bit-obdd-six%0A%0AExact%20title%3A%20Smallest%20variable-order%20OBDD%20for%20the%20middle%20bit%20of%20six-bit%20multiplication%0A%0ACanonical%20packet%3A%20https%3A%2F%2Ftheoremdb.org%2Fstatements%2Fmiddle-product-bit-obdd-six%2F%23lean-verification%0A%0AStart%20with%20prepareLeanProof%20for%20this%20exact%20problem_ref.%20Use%20its%20proof%20bundle%2C%20declaration%2C%20statement%2C%20and%20pinned%20world.%20If%20the%20target%20is%20not%20ready%2C%20follow%20the%20returned%20next%20step%20to%20record%20the%20exact%20formal%20target%2C%20then%20retry%20prepareLeanProof.%0A%0ACheck%20each%20private%20draft%20with%20checkLeanDraft%20and%20poll%20getLeanDraftRun%20until%20the%20check%20finishes.%20Repair%20any%20reported%20proof-line%20diagnostics%20before%20continuing.%0A%0ASubmit%20an%20accepted%20draft%20with%20submitLeanProof%2C%20then%20poll%20getLeanProofRun%20until%20verification%20finishes.%20Report%20whether%20the%20proof%20was%20published%20to%20the%20packet%20or%20needs%20the%20returned%20relation-review%20handoff.).

## References

1. <a id="reference-1"></a>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. 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 https://bulletin.eatcs.org/index.php/beatcs/article/download/181/176
   - journal_article; primary source; checked 2026-08-01
   - Source use: original_summary
   - For Smallest variable-order OBDD for the middle bit of six-bit multiplication, the reviewed source scope is 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. The packet makes no inference beyond that cited scope.
   - Source named by the research packet.
2. <a id="reference-2"></a>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. 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 https://www.cs.york.ac.uk/rts/docs/DAC-1964-2006/PAPERS/1987/DAC87_348.PDF
   - proceedings_article; primary source; checked 2026-08-01
   - Source use: original_summary
   - For Smallest variable-order OBDD for the middle bit of six-bit multiplication: Standard-library Python applies the Friedman-Supowit recurrence to all variable subsets and verifies an optimal diagram by direct reduction.