Alladi Ramakrishnan Hall

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

Daniel Lokshtanov

University of Bergen, Norway

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.