We investigate the algorithmic properties of circuits of bounded treewidth. Here the treewidth of a circuit C is defined as the treewidth of the underlying undirected graph of C,
after the vertices corresponding to input gates have been removed. Thus, boolean formulae correspond to circuits of treewidth 1.
- Our first main result is an algorithm for counting the number of satisfying assignments of circuits with n input gates, treewidth ω, and at most s · n gates. The running time
of our algorithm is 2^[n(1−1/O(s·ω·4ω))], which for formulae instantiates to 2^[n(1−1/O(s))]. This is the first algorithm to achieve exponential speed-up over brute force for the
satisfiability of linear size circuits with treewidth bounded by a constant greater than 1. For treewidth 1, i.e., boolean formulae, our algorithm significantly outperforms the
previously fastest 2n(1−1/O(s2))time satisfiability algorithm by Santhanam [FOCS 2010].
- Our second main result is an algorithm for True Quantified Boolean Circuit Satisfiability for circuits of treewidth ω, in which every input gate has fan-out at most s. The
running time of our algorithm is 2^[n(1−1/O(s·ω·4ω))]. Our algorithm is the first to achieve exponential speed-up over brute force for such circuits. Indeed, even for quantified
boolean formulae where every variable appears at most s times, the previously best known algorithm by Santhanam [30] has running time 2^[n(1−1/O(f(s)·log n))].
- Utilizing the structural properties of low treewidth circuits which helped us obtain improved exponential-time algorithms for satisfiability, we also show that the number of wires of any constant treewidth circuit that computes the majority function must be super-linear.