When a small diagram fails, the future queries may still be manageable

Our broader goal is to understand representations of future behavior maintained by finite rules with bounded local access and allocation. The composition question here is whether two individually simple fragments can retain a small joint decision diagram by choosing a better variable order. An explicit grid example says no. A different representation nevertheless supports persistent changes to partial assignments efficiently.

The point is the distinction between the behavior we must maintain and a particular format used to encode it. This is a classical-method comparison with a direct proof and resource accounting, not a new general lower bound.

The two fragments

Let $m\ge2$, put $b=m^2$, and name the Boolean variables by the vertices of an $m\times m$ grid, using row-major names $v(r,c)=rm+c$ for $0\le r,c<m$. Let

$$H_m=\bigwedge_{\text{horizontal }uv}(x_u\lor x_v),\qquad V_m=\bigwedge_{\text{vertical }uv}(x_u\lor x_v),\qquad F_m=H_m\land V_m.$$

There are $2m(m-1)$ clauses and $4m(m-1)$ literal occurrences altogether, with no auxiliary variables. Explicit binary variable names give $N=\Theta(b\log(b+2))$ bits. Each operand has a complete leveled width-three OBDD with $O(b)$ nodes: scan rows for $H_m$ and columns for $V_m$, remembering whether the previous value was zero, whether it was one, or whether an edge has already been violated. Reset the remembered value between paths and propagate rejection permanently. Initialization treats the missing predecessor as one.

A complete OBDD reads every boundary variable once in a fixed order, with a deterministic transition at each layer. Width counts all states at a layer, including rejection. The output requirement considered first is an explicit OBDD for all future complete-assignment membership queries, with any chosen order. This is stronger than asking whether the conjunction is satisfiable: the latter is always true here.

Reordering cannot keep the composite small

Claim. Every complete OBDD for $F_m$, in every variable order and without requiring a canonical form, has width at least $2^{m/120}$.

Here is the direct grid argument. At the balanced cut in any variable order, let $A$ be the first $\lfloor b/2\rfloor$ vertices. Both sides have at least $b/3$ vertices. If at least $m/3$ rows are mixed, each contributes a crossing horizontal edge. Otherwise there must be a row wholly in $A$ and a row wholly outside it: without either kind, its side could occupy fewer than $b/3$ vertices. Each column between those two rows then contributes a crossing vertical edge. Thus at least $m/3$ edges cross the cut.

The grid has maximum degree four. Greedily choose a crossing edge and discard crossing edges incident to the closed neighborhoods of its endpoints. At most $2\cdot4\cdot5=40$ edges are discarded per choice. We obtain an induced crossing matching $a_iz_i$, $1\le i\le k$, with $a_i\in A$, $z_i\notin A$, and $k\ge m/120$.

Assign an arbitrary subset of the $a_i$ zero, and every other prefix vertex one. These $2^k$ prefixes induce distinct remaining Boolean functions: two different subsets are distinguished by setting the corresponding $z_i$ zero and all other suffix vertices one. The induced-matching condition excludes any other edge between selected endpoints. Therefore the prefixes must reach distinct states, proving the claim.

The residual-function method is classical. Bova and Slivovsky, On Compiling Structured CNFs to OBDDs, §4.1, Definition 16 and Theorem 17, give the related subfunction-width argument; their §4.2 uses expanders for a stronger bounded-degree family. We use the explicit grid because it splits into exactly two path fragments. No novelty or attribution of this exact grid formulation to their theorem is claimed.

This closes a specific maintenance proposal: individually bounded-width fragments do not ensure a bounded-width composite, even after arbitrary reordering. It is not merely a difficulty finding a good order. In terms of input bits the lower bound is $2^{\Omega(\sqrt{N/\log N})}$, since $N=\Theta(b\log(b+2))$.

Use an explicit-node encoding with at least one graph record per OBDD state. If an implementation must construct that diagram, all old available records number $S$, and each local step allocates at most $a$ records, then

$$S+aT\ge 2^{m/120}.$$

This counts composition and deferred output construction together. Polynomial $S$ gives a superpolynomial post-preparation consequence for this output format. Unrestricted preparation could prebuild the diagram; that case is excluded from the implication. The state lower bound also applies to a fixed-order one-pass evaluator with no query-dependent storage beyond its counted state. It does not apply to arbitrary persistent memory or to every query algorithm.

A maintained representation for meaningful future queries

Now specify the behavior directly. After joining the fresh fragments, keep a partial assignment $\alpha:X\to\{0,1,*\}$. Support:

• Set: from a supplied old version handle, change one named variable to zero, one, or unassigned, returning a new version while retaining the old one.
• Extend: return whether that version’s partial assignment extends to a model of $F_m$.

The elementary invariant is

$$\operatorname{Extend}(\alpha) \iff \text{no grid edge has both endpoints assigned zero}.$$

Necessity follows from an edge clause. For sufficiency, set every unassigned variable to one. This query includes complete-assignment membership, but also answers genuinely partial queries after arbitrary branching update histories.

Independently prepared storage and initial join

Use the public universe of fixed-length binary names $0,\ldots,b-1$, with length $\ell=\lceil\log_2 b\rceil$. Each fragment independently prepares a binary lookup trie mapping a vertex to its at-most-two incident fragment edges. An entry includes neighbor names and the name of the edge’s owner, chosen as the smaller endpoint. In the grid, every vertex owns at most one horizontal and one vertical edge. Comparisons and name copying are charged bit operations.

Each side also prepares a Boolean flag trie indexed by owner names, initially all false, and an all-unassigned value trie. A flag says that the corresponding edge is violated; unused owner positions remain false. Internal flag nodes store the OR of their children. Trie depth is $\ell$, padded unused keys have neutral values, and all records have bounded degree and finite tags. A straightforward persistent insertion construction costs $O(b\log(b+2))$ local steps and records, including construction history. Thus the chosen representation has $S=O(N)$ prepared records, not $O(N)$ serialized pointer bits.

The fresh join takes the two graph-index roots, two flag roots, and one already prepared all-unassigned value root and places them in a constant-size version record. It takes $O(1)$ local steps and allocations under the stated common-universe contract. It neither compares pointer identities nor discovers a common namespace. Namespace validation or conversion, if required, is additional charged work. This initial monotone conjunction is trivially satisfiable; the useful guarantee concerns its subsequent future-query behavior.

This join is not a merge of independently changed partial assignments. Such merges, or adding new constraints to an already edited version, are outside this constant-time join contract.

Persistent update and query

To set $x_v$:

1. Follow the bits of $v$ through the assignment trie and copy its root-to-leaf path with the new trit.
2. Read the at-most-four incident edges from the two independently prepared graph indexes. Look up their endpoints in the new assignment trie.
3. Recompute those edge flags. Copy the affected paths in the two flag tries, recomputing each OR tag from its children.
4. Return a fresh version record holding the new roots and the unchanged graph indexes.

All other flags remain valid because their endpoints did not change. Path copying preserves every old root and its entire interpretation; later updates may branch from any supplied old root. The OR tags then make Extend a constant number of root observations.

Reading a name costs $O(\ell)$ bit operations. Every lookup or path copy uses $O(\ell)$ local steps. There are only constantly many affected edges. Traversal stacks can themselves be immutable bounded-arity records, with every allocation charged. Construct replacement nodes bottom-up so each new record points to older records. No random access by numerical address, physical pointer equality, unbounded alphabet, unit-cost name comparison, or free initialization is used. Consequently,

$$T_{\rm Set}=O(\log(b+2)),\quad A_{\rm Set}=O(\log(b+2)),\quad T_{\rm Extend}=O(1).$$

After $U$ updates, all retained storage, including preparation and temporary traversal history, is

$$M=O\bigl(N+U\log(b+2)\bigr)\text{ records}.$$

An explicit binary serialization of their pointers uses $O(M\log(M+2))$ bits. Selecting a version by an integer index is not free: the bound starts with a supplied version handle. For $Q$ queries, full work is $O(N+U\log(b+2)+Q)$ plus any namespace conversion. Each logical update takes logarithmic work; bounded work per machine step does not make the whole update constant-time.

Path copying is classical. Driscoll, Sarnak, Sleator and Tarjan, Making Data Structures Persistent (1989), printed p.116, end of §4, discuss copying access paths and credit prior implementations. We use that simple method and the proof above, not their stronger space-saving transformations. No novelty is claimed for the persistent construction.

What this changes in the research direction

The two outcomes concern the same constraint relation. Every single-order diagram needs many states, while an indexed persistent representation supports useful future updates and queries compactly. This strengthens the earlier fixed-canonical-output diagnostic: changing the order or dropping canonicity cannot repair the diagram, and the positive comparison supports repeated partial-assignment changes rather than only a one-shot complete-assignment scan.

It would therefore be a mistake to make preservation of small diagram width the general goal. It is one sufficient format for some operations, not a necessary condition for maintaining future behavior. Conversely, this example does not solve arbitrary constraint joins, unbounded confluent merges, or constant-time logical updates. The grid construction changes the evaluator’s access pattern and pays for it explicitly.

The next assessment should focus on a maintained operation and query contract, rather than improving this exponent. Relevant dynamic-decomposition literature already distinguishes maintaining summaries on a supplied structure from rebuilding that structure. For example, Korhonen et al., Dynamic treewidth (2023), Theorem 1.1 and §2.1, treat edge updates with amortized bounds and a width bound or a too-large marker. Those guarantees do not directly give worst-case bounded-local persistent joins. Their hypotheses and access model must be checked before using them as a route toward the broader goal.

Verification status

Written proofs and independent review support the claims; there is no formal verification. The standalone finite checker checks every balanced vertex cut for the $2\times2$ and $3\times3$ grids against exact residual truth tables. It also checks 750 branching persistent updates on three small grids, rechecking every retained version against the edge semantics and counting copied tree nodes. Results all pass. The Python checker uses ordinary host-language operations and is a semantic/allocation regression, not a verification of the local-machine running-time bound.