Decision diagrams stop counting subfunctions: ATDDs use cut-matrix rank to give one canonical form on any vtree

A new representation of Boolean functions replaces width as the number of distinct subfunctions with the dimension of the space those subfunctions span, so the same function can be written smaller on the same vtree. Tree decision diagrams (TDDs) count the distinct nonzero subfunctions across each vtree cut; that count is the factor width and equals the width of the minimal TDD at that cut. In a four-variable example, the middle output bit of the sum of two 2-bit numbers has four distinct rows at one cut of the balanced vtree, so a minimal TDD has four nodes there; the last row is the first minus the second plus the third, the row space has dimension three, and the corresponding ATDD has three vectors at that cut.

An ATDD is a tree tensor network over the vtree, storing a list of vectors at each node and using a coefficient tensor at each internal node to combine the children's vectors into the parent's. At each node the vectors are a basis of the cut matrix's column space, fixed in reduced row echelon form, which is unique and therefore pins down the whole network from the function and the vtree. With echelon bases, the canonical tests at a node are products of the children's canonical tests, so checking that each tensor satisfies an echelon condition and a rank condition decides in polynomial time whether a network is the ATDD of its function, without reference to the function.

The gain in succinctness does not cost canonicity: for a fixed vtree each Boolean function has exactly one ATDD, and equivalence checking reduces to syntactic equality. Earlier rank-based representations such as weighted tree automata and tensor trains were unique only up to a change of basis or required genericity assumptions such as distinct singular values, and none was canonical over arbitrary vtrees. Over the rationals and with no genericity assumption, two ATDDs respecting the same vtree and computing nonzero Boolean functions compute the same function if and only if they are syntactically identical; model counting, weighted model counting and the Boolean-promise test all run in time polynomial in the ATDD size.

Vtree change can be local: after one rotation at a node, the new ATDD differs from the old one in two tensors only, computed from the two old ones. The complexity of changing the vtree of a TDD was an open question, and prior work only suggested adapting local vtree changes from SDD compilers. A rotation costs a number of multiplications plus one reduced row echelon computation; vtree change runs in output-polynomial time for both TDDs and ATDDs, answering the earlier complexity question.

The demonstrated scope is Boolean-function representation under a fixed vtree: width equals the factor rank, the operation set includes polynomial-time model counting, weighted model counting, conditioning, forgetting, conjunction, disjunction, negation and equivalence checking, and vtree change runs in time polynomial in input and output. The empirical part is preliminary timing from two Rust prototype compilers over six function families, plus model counts on eight native CNFs that agree with the independent exact counter sharpSAT-TD.

The authors list two open problems: whether the quasi-polynomial separation from structured deterministic DNNFs can be sharpened to an exponential one, and whether any two low-rank vtrees are joined by a rotation path without high-rank intermediates. Timings are preliminary; on the pigeonhole and random 3-CNF instances tested, TDD and ATDD widths coincide at almost every node, so ATDDs have no advantage and incur larger overhead, and on the larger pigeonhole instances the ATDD compiler exceeded a time cap the TDD met.