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. 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 2~(n(1-1/O(s~2))) time satisfiability algorithm by Santhanam [32]. 2. 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 [32] has running time 2~(n(1-1/O(f(s)·log n))). 3. 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.
展开▼
