Name
Title | ||
|---|---|---|
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 [Equation], which for formulae instantiates to 2n(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 [32].
• 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 [Equation]. 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(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.
|
Year | DOI | Venue |
|---|---|---|
2018 | 10.5555/3174304.3175284 | SODA '18: Symposium on Discrete Algorithms
New Orleans
Louisiana
January, 2018 |
Field | DocType | ISBN |
Generating function,Discrete mathematics,Combinatorics,Boolean circuit,Exponential function,Vertex (geometry),Computer science,Satisfiability,Treewidth,Majority function,Bounded function | Conference | 978-1-61197-503-1 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Daniel Lokshtanov | 1 | 1438 | 110.05 |
| Ivan Mikhailin | 2 | 0 | 0.34 |
| Ramamohan Paturi | 3 | 1260 | 92.20 |
| Pavel Pudlák | 4 | 0 | 0.34 |