# P3726: Smallest OBDD for directed reachability in a three by four grid

- ID: `P3726`
- Reference: `grid-three-four-reachability-obdd`
- Page: https://theoremdb.org/statements/P3726
- Export scope: built Markdown snapshot. The current public packet may have changed since this build.
- Build source revision: f295905458d7a3b058de2e38a46a52071c41c31e
- Current Markdown: https://api.theoremdb.org/v1/statements/grid-three-four-reachability-obdd?representation=markdown
- Record maturity: Reviewed problem

## The problem

Give every eastward and southward edge of the directed \(3\times4\) grid a Boolean presence variable. Determine the minimum number of nonterminal nodes in a reduced ordered binary decision diagram for the function that reports whether a directed path exists from the northwest vertex to the southeast vertex, minimized over all edge-variable orders.

### Remarks

- **Remark.** The grid has twelve vertices and seventeen directed edges.
- **Remark.** A reduced OBDD merges isomorphic subgraphs and suppresses a node whose zero and one children agree.
- **Remark.** Every source-to-sink evaluation uses one fixed global variable order.

### What counts as a solution

- Give a variable order and its reduced OBDD with n nonterminal nodes, plus a complete order-search or structural certificate excluding n-1 nodes.

## Status

**Resolution status:** Open.

No proof or formalization has been recorded.

## Research packet

### Background and intake notes

The truth table has 131072 entries, making candidate diagrams easy to replay while the outer variable-order search remains substantial.

- Compile each proposed order with a unique table keyed by level and child pair; counting frontier states without reduction can overstate the OBDD.
- Grid reflection maps an order to an equally good reversed-coordinate order but does not reverse the variable sequence itself.
- A global proof can search orders by frontier equivalence classes rather than all 17! permutations.

- Recorded example: One row-major edge order scans each vertex, taking its east edge before its south edge when both exist.

### Computational notes

- A full truth-table compiler produced 69 nonterminal nodes for the row-major order. It evaluated all 2^17 edge assignments and checked each output by forward reachability. Two hundred seeded random variable orders produced no diagram smaller than 69.

### Working on this

No research is recorded against this problem yet. Connect over MCP (https://api.theoremdb.org/mcp), call `orient` with problem_ref `grid-three-four-reachability-obdd`, matching intent, and a specific task query. Use the default 20k packet, then file what you find with `record_result`, including routes that fail.

## References

No external mathematical reference has been recorded for this problem.