Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Circus of Circuits: Connections Between Decision Diagrams, Circuits, and Automata

Antoine Amarilli, Marcelo Arenas, YooJung Choi, Mikaël Monet, Guy Van den Broeck, Benjie Wang

TL;DR

This work surveys and unifies representations of Boolean functions across binary decision diagrams and Boolean circuits, highlighting how structure, determinism, and sharing influence tractability in knowledge compilation. It introduces provenance-based correspondences between automata (on words and trees) and both BDDS and structured circuits, enabling linear-time translations that preserve key properties (e.g., free/ordered, unambiguous/deterministic, complete/smooth). The paper provides formal definitions, translation procedures, and complexity bounds that connect automata-theoretic notions to circuit/BDD classes, facilitating cross-domain insights and potential transfer of tractable techniques. Together, these results lay a Rosetta-stone framework to reason about representations, operations, and provenance across BDDS, circuits, and automata, with implications for query evaluation, probabilistic databases, and SAT/knowledge compilation tasks.

Abstract

This document is an introduction to two related formalisms to define Boolean functions: binary decision diagrams, and Boolean circuits. It presents these formalisms and several of their variants studied in the setting of knowledge compilation. Last, it explains how these formalisms can be connected to the notions of automata over words and trees.

A Circus of Circuits: Connections Between Decision Diagrams, Circuits, and Automata

TL;DR

This work surveys and unifies representations of Boolean functions across binary decision diagrams and Boolean circuits, highlighting how structure, determinism, and sharing influence tractability in knowledge compilation. It introduces provenance-based correspondences between automata (on words and trees) and both BDDS and structured circuits, enabling linear-time translations that preserve key properties (e.g., free/ordered, unambiguous/deterministic, complete/smooth). The paper provides formal definitions, translation procedures, and complexity bounds that connect automata-theoretic notions to circuit/BDD classes, facilitating cross-domain insights and potential transfer of tractable techniques. Together, these results lay a Rosetta-stone framework to reason about representations, operations, and provenance across BDDS, circuits, and automata, with implications for query evaluation, probabilistic databases, and SAT/knowledge compilation tasks.

Abstract

This document is an introduction to two related formalisms to define Boolean functions: binary decision diagrams, and Boolean circuits. It presents these formalisms and several of their variants studied in the setting of knowledge compilation. Last, it explains how these formalisms can be connected to the notions of automata over words and trees.
Paper Structure (18 sections, 3 theorems, 6 figures, 2 tables)

This paper contains 18 sections, 3 theorems, 6 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Binary Decision Diagrams
  4. Basic classes
  5. Binary decision diagrams with or-nodes
  6. Completion and zero-suppressed semantics
  7. Decision trees
  8. Boolean Circuits
  9. Definitions
  10. Sentential decision diagrams
  11. Formulas
  12. Smoothness
  13. From Binary Decision Diagrams to Boolean Circuits
  14. Automata
  15. Automata on words
  16. ...and 3 more sections

Key Result

proposition 1

Given a nBDD$\mathcal{D}$, we can convert it in linear time to a Boolean circuit $C$ that describes the same Boolean function. The translation preserves the following:

Figures (6)

  • Figure 1: An nBDD over the set of variables $\bm{X}\xspace = \{X,Y,Z,W\}$.
  • Figure 2: Two deterministic binary decision diagrams over the set of variables $\bm{X}\xspace = \{X,Y,Z,W\}$.
  • Figure 3: Transformation of a BDD with or-nodes into an nBDD.
  • Figure 4: A deterministic and decomposable Boolean circuit as a classifier and its vtree.
  • Figure 5: An example of a sentential decision diagram (SDD) and its vtree.
  • ...and 1 more figures

Theorems & Definitions (8)

  • proposition 1
  • proof
  • definition 1
  • proposition 2
  • proposition 3
  • proof : Proof of Proposition \ref{['prp:wordprov']}
  • definition 2
  • proof : Proof of Proposition \ref{['prp:treeprov']}