A smaller way to represent Boolean rules—without losing a unique form

How can a computer store a complicated collection of yes-or-no rules so that questions about those rules become easier to answer? One approach is knowledge compilation: invest effort in converting the rules into a representation that supports efficient queries afterward.

In a November 2026 arXiv preprint, Alexis de Colnet and Stefan Szeider introduce algebraic tree decision diagrams, or ATDDs. Their main contribution is theoretical: a representation that can be exponentially more compact than tree decision diagrams while retaining a unique form for a fixed tree of variables. The supplied record does not establish peer-reviewed publication.

Counting cases versus finding independent patterns

A Boolean function takes a collection of binary inputs and returns either zero or one. A decision diagram represents that function without necessarily listing every possible input combination.

Tree decision diagrams organize variables using a rooted binary tree called a vtree. Its leaves are the variables. At each node, the tree separates one group of variables from the rest. Assigning values to the first group leaves a smaller function of the remaining variables—a subfunction.

A conventional tree decision diagram distinguishes the different nonzero subfunctions across that split. ATDDs instead ask how many are linearly independent: how many basic patterns are needed to reconstruct all the others by addition and multiplication by rational numbers.

The paper illustrates the distinction with a four-variable function. At one split, there are four distinct nonzero subfunctions, but the fourth equals the first minus the second plus the third. Counting requires four cases; linear algebra needs only three independent patterns.

More generally, the authors arrange function values into a cut matrix, with assignments on one side indexing rows and assignments on the other indexing columns. Its rank measures the number of independent patterns. The largest cut rank across the vtree is the function’s factor rank for that tree.

Compression with a unique answer

ATDDs store these relationships as a tree tensor network: connected arrays of coefficients that combine information from child nodes. The calculation remains exact, using rational arithmetic rather than approximate numerical compression.

But compactness alone does not guarantee uniqueness. Different choices of independent patterns can produce different networks representing exactly the same function.

The authors remove that freedom using reduced row echelon form, the unique matrix form produced by Gauss–Jordan elimination, together with a fixed ordering of assignments derived from the vtree. They prove that every Boolean function has exactly one ATDD for a given vtree.

Consequently, two ATDDs using the same vtree represent the same function precisely when their stored structures and numbers match. The paper also provides local matrix conditions for checking canonical form and a polynomial-time test of whether a rational tree tensor network returns only Boolean values.

The theoretical compression can be substantial. For the hidden weighted bit function, which selects an input bit according to how many inputs are one, the authors bound factor rank by the number of variables plus two on every vtree. Earlier results require exponentially large tree decision diagrams for an infinite family of these instances.

What becomes efficient—and what does not

Once an ATDD is available, the proposed algorithms support polynomial-time model counting: counting input assignments that make the function true. Weighted counting also works when assignment weights are products of individual variable-value weights, a setting relevant to probabilistic inference.

The representation supports Boolean operations and conditioning. A local vtree rotation changes only two tensors. Conversion to an arbitrary target vtree takes time polynomial in both input and output size; this does not promise a small output.

Nor does efficient querying make compilation universally easy. Some functions still require large representations, and choosing a low-rank vtree remains difficult.

Preliminary tests show gains and costs

The authors implemented paired Rust compilers using identical vtrees and exact arithmetic. In a multiplexer example with 16 data variables and four selector variables, TDD width reached 65,535, compared with ATDD width 16. This comparison depends on the tree: the paper notes that multiplexers have small TDDs on suitable alternative vtrees.

The advantage was not general. On tested pigeonhole and random constraint instances, widths usually coincided, leaving ATDDs with additional overhead. An integer-arithmetic kernel substantially reduced counting costs, but ATDD counting remained slower in the reported family-level comparisons.

Core mathematical results were formalized in Lean, and algorithms were checked against brute-force references and an independent Python implementation. Runtime and bit-size bounds were not machine-checked. The evidence therefore combines mathematical proofs, partial formal verification and preliminary computational benchmarks—not a demonstration of universal practical superiority.