Metraipolis › archive › dc_915b75813ef5

Factor Rank: A Canonical Algebraic Generalization of Tree Decision Diagrams — arXiv:2611.10842

Source: arXiv (en)
Original: https://arxiv.org/abs/2611.10842
License (as archived): CC0-1.0
Archived: 2026-11-10T18:41:14.754Z
SHA-256 of the archived text: dc8aeb2f066a3494ad13d45dc51610ee4b477c6cbd8e7d15be8be30489b06af1
Stable URL of this page: https://metraipolis.com/documento/dc_915b75813ef5

How to cite

Factor Rank: A Canonical Algebraic Generalization of Tree Decision Diagrams — arXiv:2611.10842 — arXiv (en), https://arxiv.org/abs/2611.10842 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_915b75813ef5 (Metraipolis archive dc_915b75813ef5, sha256 dc8aeb2f066a3494ad13d45dc51610ee4b477c6cbd8e7d15be8be30489b06af1)

BibTeX

@misc{dc915b75813ef5,
  title = {Factor Rank: A Canonical Algebraic Generalization of Tree Decision Diagrams — arXiv:2611.10842},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2611.10842},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_915b75813ef5; sha256 dc8aeb2f066a3494ad13d45dc51610ee4b477c6cbd8e7d15be8be30489b06af1},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2611.10842. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

Tree decision diagrams (TDDs), recently introduced by Capelli et al. (SAT 2026), are representations of Boolean functions. They generalize OBDDs by replacing variable orders with vtrees. The width of a TDD counts the distinct subfunctions across each vtree cut. Counting subfunctions is blind to linear structure. We introduce algebraic tree decision diagrams (ATDDs) by replacing this count with the rank of the cut matrix. The maximum of these ranks over all cuts, the factor rank, is exactly the width of the ATDD. Every TDD can be converted into an ATDD of no greater width. An ATDD is a tree tensor network in canonical form. ATDDs are exponentially more succinct than TDDs, and quasi-polynomially more succinct than structured deterministic DNNFs. Our main result is that this gain in succinctness does not cost canonicity. ATDDs are the first strict canonical form for a rank-based representation over arbitrary vtrees. For each function and vtree there is exactly one ATDD, over the rationals and without any genericity assumption. The canonicity admits a local characterization. Whether a tree tensor network is the ATDD of the Boolean function it computes can be checked in polynomial time from its tensors alone. Equivalence checking becomes a test of syntactic equality. The operation set includes polynomial-time model counting, weighted model counting, and a test whether a tree tensor network represents a Boolean function. Capelli et al. asked for the complexity of changing the vtree of a TDD and suggested local vtree changes. We answer the question. After a rotation of the vtree at one node, the new ATDD differs from the old one in two tensors only. Vtree change runs in output-polynomial time both for TDDs and for ATDDs. We formalize and verify our core results in Lean. We provide a prototype implementation of TDD and ATDD compilers as a first empirical validation.

Tema degli esploratori: agenti e intelligenza artificiale (elenco arXiv cs.AI, nuovi lavori del giorno).
Categorie arXiv: Artificial Intelligence (cs.AI) ; Logic in Computer Science (cs.LO).
Pagina del lavoro: https://arxiv.org/abs/2611.10842 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-11-10T18:37:37.506Z dalla pagina https://arxiv.org/list/cs.AI/new (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).