Welcome to the Tractable Circuit Zoo

Boolean functions are one of the most basic objects in computer science, with countless applications demanding their efficient representation, manipulation, and querying. However, the succinctness of a representation is usually in tension with its tractability for manipulation and querying. The tractable circuit zoo catalogs known representation languages together with their relations in terms of succinctness and tractability. While research in the area spans many decades, lots of progress has been made just recently, and much work remains. We hope the zoo may serve as an open source survey of the area that grows as our understanding does.

Zoo Features

In addition to the manually maintained database of representation languages and their succinctness and tractability relations, the zoo performs automated reasoning using simple inference rules. For example, succinctness is transitive: if A compiles to B and B compiles to C, then A compiles to C. Throughout the zoo, zebra cells—i.e., cells with a striped background—denote results which were derived automatically in this way.

This makes it easy to check consistency of the database, and reduces the number of relations that need to be manually entered. It also makes it fun to consider “possible worlds”. By entering “sandbox mode” the user can enter hypothetical (yet unproven) relations and immediately visualize what other relations follow from their hypotheses. The zoo is open source and will soon have a user interface for contributing directly through the website.

Central Concepts

We give informal descriptions of some central concepts, leaving formal definitions to the literature (see, e.g., [24, 42]).

Representation Language: A representation language is a method of expressing Boolean functions, such as a truth table or a class of Boolean circuits. Slightly more formally, a representation language is a pair $(R,I)$ where $R$ is a set of strings (over some fixed alphabet) and $I$ is an interpretation function that maps each $r\in R$ to the Boolean function that $r$ represents. The size of a representation $r\in R$ is its length (number of symbols) denoted $|r|$.

Succinctness: Let $A$ and $B$ be representation languages. We say $a\in A$ and $b\in B$ are equivalent if they represent the same function. We say $A$ is at least as succinct as $B$, denoted $A\le B$, if for every $b\in B$ there is an equivalent and not too much larger $a\in A$, specifically, $|a|\le |b|^{O(1)}$.

Tractability: We say a query (such as "is $f$ satisfiable?") is tractable for a representation language $A$ if there exists an algorithm which given any $a\in A$ answers the query in polynomial time (in the input length $|a|$). Similarly, a transformation (such as "negate $f$" or "conjoin $f$ and $g$") is tractable for representation language $A$ if there exists an algorithm which given input representation(s) in $A$ computes a correct output representation in $A$ in polynomial time (in the length of the input).

Some Technical Notes

Non-Strings: For representation languages not directly defined as strings, e.g. circuits or decision diagrams, one may freely take a reasonable encoding of the object into a string, and the theory will be unaffected (since it does not distinguish between polynomial changes in size). Equivalently, one may think of a separate size measure defined directly on such objects (e.g, the number of nodes) which is polynomially related to the length of reasonable encodings.

Families of Representation Languages: We’d like to include representation languages like $OBDD_<$, which contains all OBDDs respecting a specific variable order $<$. However, there are infinitely many different $OBDD_<$ languages, one for every choice of $<$. Therefore we include families of representation languages in the zoo. For example, $\{OBDD_<\}_{orders <}$. We extend the definition of succinctness to families as follows. We say family $\mathcal{B}$ is at least as succinct as family $\mathcal{A}$, denoted $\mathcal{B}\le \mathcal{A}$, if for every $A\in \mathcal{A}$ there exists a $B\in \mathcal{B}$ such that $B\le A$. In the special case of singleton families (families containing a single representation language), this recovers the behavior of the usual definition of succinctness. For larger families, it behaves in the intuitive way. For example $OBDD\le \{OBDD_<\}$ but $\{OBDD_<\}\not\le OBDD$, and $\{SDNNF_T\}\le \{OBDD_<\}$ but $\{OBDD_<\}\not\le\{SDNNF_T\}$. Such a definition allows us to consider representation languages and families of representation languages in a common way. To avoid excessive braces throughout the zoo, we just write $OBDD_<$ to mean the family $\{OBDD_<\}$ (and similar for families involving vtrees).

Quasipolynomial Succinctness: Actually, we further distinguish between polynomial and quasipolynomial size since some central languages are known to support quasipolynomial compilations, whereas others have exponential separations. See the succinctness table for notation. Recall that functions with polynomial growth are in $n^{O(1)}$ whereas functions with quasipolynomial growth are in $n^{\log^{O(1)} n}$.