Beating Brute Force for (Quantified) Satisfiability of Circuits of Bounded Treewidth

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.