Beating brute force for (quantified) satisfiability of circuits of bounded treewidth

Abstract

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 2n(1 1 O(s4) ), which for formulae instantiates to 2n(11=O(s)). This is the first algorithm to achieve exponential speedup 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(11=O(s2)) time satisfiability algorithm by Santhanam [32]. Our second main result is an algorithm for True Quantified Boolean Circuit Satisfiability for circuits of treewidth !, in which every input gate has fanout at most s. The running time of our algorithm is 2n(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 2n(11=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.