Small fragments need a controlled joint interface

Our broader goal is to understand when future computational behavior admits representations maintained by finite rules with bounded local access and allocation. The composition question here is whether two independently small-width constraint fragments can be combined cheaply. Individual width is insufficient. A bounded joint frontier, together with a paid alignment procedure, gives a useful sufficient condition.

This is a worked specialization of classical decision-diagram and constraint-elimination ideas, with explicit resource accounting. It is not a new general lower bound or a characterization of FPRD.

1. Exact fragment and query contract

Each fragment is a complete leveled ordered binary decision diagram (OBDD) over the same named Boolean boundary $X$, with $|X|=b$. A diagram has one transition layer for every variable, in a permutation of $X$. Each layer maps its incoming state and the variable’s bit to an outgoing state. There is a specified initial state and a specified accepting subset at the final layer. Width bounds $w_1,w_2\ge1$ include rejecting states. Padding unreachable states is harmless. Skipped levels are not implicit in this model.

The independently prepared fragments have orders $\pi,\rho$. The required output is one Boolean: does some boundary assignment satisfy both diagrams? No canonical composite diagram, witnesses, or arbitrary subsequent query interface is required. Algorithms below are deterministic and exact.

For fixed widths, explicit binary names and node identifiers give combined input size $N=\Theta(b\log(b+2))$ for nonempty diagrams. No exponential truth table or auxiliary Boolean variables is hidden. Native transition streams take $O(b)$ fixed-width records after variable alignment; the named input retains its bit cost. For variable widths, padded transition tables use $O(b(w_1+w_2))$ state-transition entries, with logarithmic state/name encodings in $N$.

2. A classical obstruction already occurs at width three

Claim. Conjunction satisfiability of two such width-at-most-three diagrams with independent orders is NP-complete.

Proof. Given a 3CNF, replace every literal occurrence by a fresh boundary variable. Let $b$ be the number of occurrences. The first diagram groups these variables by original variable and checks that each group has a common value. Two live states remember zero or one; a third is a permanent rejection state. At a group boundary, a successful check resets the live state. A singleton group simply passes.

The second diagram groups occurrence variables by clause. Two live states remember whether a true signed literal has appeared in the current clause. At its end, reject if none has appeared; otherwise reset. Its third state is permanent rejection. Propagate rejection through every later level, so both diagrams are complete and leveled. Each has $O(b)$ nodes. Their conjunction has a satisfying assignment exactly when the original formula does: equality recovers one value per original variable, while the second diagram checks the clauses. Guessing the $b$ bits and running both diagrams establishes membership in NP. The construction has $N=\Theta(b\log(b+2))$ encoded bits. $\square$

Different-order OBDD consistency is classical: Darwiche and Marquis (2002), Appendix A, printed p.253 and pp.259–260 cite Meinel and Theobald’s Lemma 8.14. We inspected that compilation paper, not the original book proof. Ordyniak, Paesani, Rychlicki and Szeider (2024), §6.3, pp.26–28 explicitly describe the occurrence-copy/equality construction. Their Theorem 41 concerns explanation problems and its formal reduction uses a width-four ensemble; the width-three statement above is proved directly, not attributed verbatim to that theorem. We claim no novelty for this specialization.

This obstructs uniformly polynomial independent preparation followed by uniformly polynomial composition and answer, unless P=NP. It is not an unconditional superpolynomial time bound, and says nothing of that form after unrestricted preprocessing. The cost includes deferred answer work. Polynomial preparation can store polynomially many records; arbitrarily large precomputed storage is outside this conditional implication.

3. Identical orders are sufficient, but unnecessary

With a common order, the unreduced product tracks a pair of states. Reachability through its $b$ layers takes $O(bw_1w_2)$ table operations. No canonical reduction is needed.

A more informative construction handles different orders. Write the second diagram’s intermediate states as $q_0,\ldots,q_b$, with transition $j$ reading $\rho_j$ and linking $q_{j-1}$ to $q_j$. Sweep variables in the first diagram’s order. After $i$ steps put

$$P_i=\{\pi_1,\ldots,\pi_i\},\qquad F_i=\{j:1\le j<b,\;[\rho_j\in P_i]\ne[\rho_{j+1}\in P_i]\},$$

$$h_i=|F_i|,\qquad h=\max_{0\le i\le b}h_i.$$

Thus $F_i$ names second-diagram state connections between a processed and an unprocessed transition. It counts unresolved state connections, not all previously read input bits.

Frontier claim. Given the orders and an aligned transition schedule, compatibility can be decided using tables with at most $w_1w_2^{h_i}$ entries at layer $i$. A conservative bound is

$$O\!\left(b(h+1)w_1w_2^{h+1}\right)$$

word/table operations, with $O(w_1w_2^h)$ Boolean table entries, in addition to the input and schedule. Tuple descriptions use up to $h$ state coordinates. These are algorithmic array bounds, not uniform constant-cost local operations when the parameters grow.

Invariant and proof. Let $T_i(a,\mathbf q)$ mean there exists an assignment to $P_i$ reaching first-diagram state $a$ and satisfying every processed second-diagram transition, with the indicated values at the state connections $F_i$. All internal states lying wholly inside processed segments have been existentially eliminated. Connections incident only to unprocessed transitions impose no constraints yet.

Initially the table contains just the first diagram’s initial state. Process $x=\pi_{i+1}$, whose position in $\rho$ is $j$. For each true old entry and each bit $t$, update the first state using $t$. Enforce the second transition $q_j=\delta_j(q_{j-1},t)$ with the same bit. An incident state already on the old frontier must match its stored value. Otherwise, if its value is needed, enumerate the incoming state; determinism fixes the outgoing state. Introduce new frontier coordinates and project away coordinates no longer in $F_{i+1}$. Take the Boolean union of all consistent extensions.

The start condition on $q_0$ is enforced when transition 1 is processed, and the final acceptance condition on $q_b$ when transition $b$ is processed, wherever those occur in the sweep. Endpoints are never free frontier coordinates. For $b=1$, both conditions apply in the same update. For $b=0$, check the two initial states’ acceptance directly.

Every full satisfying assignment supplies a consistent extension at each update. Conversely, every surviving table entry has a witnessing processed assignment by induction; forgotten states interact with the remainder only through the retained frontier. At the end the frontier is empty, all second transitions and endpoint constraints have been checked, and acceptance of the remaining first state decides the query. This proves correctness. Each old tuple has two bit choices and at most $w_2$ incoming-state choices, and tuple manipulation takes $O(h+1)$ table operations, yielding the stated conservative bound. $\square$

This is an explicit instance of the classical join-and-project elimination principle. Dechter (1999), §2.1, Figure 3 and Theorems 1–2, printed pp.44–47, describes preserving the effect of eliminated variables as a relation on the remaining interface. Our particular frontier and transition bound are established above; we do not equate this $h$ with minimum treewidth or import a decomposition algorithm for free.

Reverse-order test. If $\rho$ is the reverse of $\pi$, each proper processed prefix in $\pi$ is a suffix in $\rho$. Hence $h=1$. Compatibility remains linear in $b$ for fixed widths. An evaluator that buffers every bit until the second diagram can read forward may accumulate a linear backlog, but that backlog is not inherent: the frontier table propagates a relation on one state instead.

Large $h$ does not itself prove hardness. For example, width-one diagrams accepting every assignment are easy for every order pair. The parameter bounds this construction, not every possible representation or algorithm.

4. What bounded local execution actually requires

Fix $w_1,w_2,h$ as constants independently of $b$. Supply two transition streams aligned in $\pi$ order and a valid schedule specifying frontier-slot introduction, removal, and permutation, including endpoint markers. These instructions and transition maps have a finite alphabet. The Boolean table has a fixed finite number of entries and can be part of finite control. A deterministic controller consumes one record from each stream and the schedule per stage; it uses bounded local access and bounded allocation at each step. Total core work and conservative fresh-history allocation are both $O(b)$. The operands remain immutable. Initialization uses a fixed table, and the outcome alphabet is Boolean; no numerical address, pointer identity, hidden metadata, or random source is required.

Alignment is charged. A valid schedule is a promise of this core theorem, not a free service for arbitrary input. If the order pair is public before coefficient preparation, a coefficient-independent layout may be built first, charging its construction, after which each side independently installs its own transition maps. If independently chosen named orders arrive only at composition, the composer must match names, reorder maps, and construct or verify that schedule. Let $L$ and $A_L$ be the actual local work and fresh allocations for this stage. The promised fixed-parameter bound is

$$T_{\rm compose}+T_{\rm deferred\ answer}=L+O(b),\qquad A_{\rm join}=A_L+O(b).$$

Repeated scans and explicit string comparisons give a polynomial layout procedure on finite named inputs; no linear bound for that stage is asserted. An unverified schedule may not be trusted when deciding the original named-input problem.

With fixed parameters, aligned streams and a schedule occupy $O(b)$ active records. Let $S$ include all independently prepared storage, layouts already built, and retained history. If preparation incurred $P_1,P_2$ local steps and $A_1,A_2$ allocations, the full accounting is $P_1+P_2+L+O(b)$ work and $A_1+A_2+A_L+O(b)$ new records, in addition to any declared initial storage. For a total of $M$ bounded-arity historical records, explicit binary pointers may require $O(M\log(M+2))$ bits. No reclamation of history is presumed.

This is a supplied-layout, two-fragment decision procedure. It does not give constant-time composition, bounded per-arrival preparation, or closure under an arbitrary sequence of joins. Product widths can grow under repeated composition. No unrestricted SAT algorithm, Turing-machine lower bound, scaffold-recognition theorem, or PEG consequence follows.

5. Verification and the consequential next question

The proof is written and independently reviewed, not formally verified. The standalone checker compares the frontier procedure against exhaustive assignments on 874 seeded diagram pairs, covering every second order through six variables, and checks 154 small occurrence-copy reductions. Results include empty inputs, endpoints, rejection and reversed orders. These finite checks expose implementation errors; they do not prove the quantified claims. The checker recomputes layouts by scans and is an answer-correctness regression, not an implementation or empirical verification of the linear prepared-schedule cost bound.

The structural lesson is that individually small summaries need not have a small joint interface, while exact order agreement is stronger than necessary. The useful remaining question is whether the layout and interface promise can itself be maintained through independently prepared or repeated joins at the required local cost. A proposed continuation must specify that operation contract and charge layout construction and growing widths. The classical frontier algorithm alone does not settle it. The next assessment should examine those maintenance requirements, rather than sharpening this bound or treating a supplied schedule as a complete solution to the broader goal.