Graph decompositions have proven to be a powerful tool, both for proving theoretical properties of graphs, as well as in applications of graph theory in theoretical computer science. The proposed project looks at basic questions on graph decompositions and develops applications of graph decomposition techniques in theoretical computer science and complexity theory.
The specific research topics to be tackled lay in two primary directions. First, we consider the development of an approximate structural characterization of excluded vertex minors, a model of graph containment generalizing recent work on excluded matroid minors of Geelen, Gerards, and Whittle as well as the classic work of Robertson and Seymour on excluded graph minors. Second, we look at new approaches to proving rigorous lower bounds on proof complexity for difficult NP problems such as SAT and k-clique. The two research topics will proceed in parallel with techniques from one being applied in the other, and vice versa.
Success on each target will constitute a significant advance on the current state of the art; furthermore, progress on the proposed targets should lead to new algorithmic techniques to tackle computationally difficult problems in theoretical computer science.
When discussing each target, we looked at the potential to advance the state of the art on the specific topics studied. In this section, we look the broader impacts of the proposed research in theoretical computer science as well as describing the more innovative aspects of the project.
Applications in theoretical computer science:
Under standard complexity theoretic assumptions, NP-complete problems do not admit an efficient polynomial time algorithm. However, such problems arise a number of real-world applications, motivating alternate approaches to computing NP-hard problems.
Fixed parameter complexity seeks to isolate what parameters of the problem give rise to the hardness, yielding efficient algorithms when one parameter of the problem is fixed. Problems admitting such an algorithm are called Fixed Parameter Tractable, and the resulting algorithm is known as an FPT algorithm. See [DF1999] for an overview on the field. The approach was pioneered by the proof of Robertson and Seymour [RS1995] that the k-disjoint paths problem, which is NP-complete in general as shown by Karp, can be solved in time O(|V(G)|3) for fixed values of k. Graph decompositions play a fundamental role in the Robertson Seymour result, and further developments in the field have continued to rely on such techniques. For example, while it is NP-complete to test whether a given graph G contains a smaller graph H as a topological minor, when H is a fixed graph is fixed parameter tractable as shown by Wollan in 2011 [GKMW2011], resolving an open question of Downey from 1995.
The graph structure of boolean formulas has been studied in connection with the performance of SAT solvers. There are FPT algorithms that solve formulas with graph structure of bounded treewidth [GSS2002]. The proposed work on SAT solvers will extend these approaches by using stronger structural properties. New graph decompositions may lead to FPT algorithms for a wider class of SAT instances.
The efficiency of a SAT solver technique can be measured in terms of the size of logical proofs that this technique produces (automatizability [BPR2000]). In particular the graph structure of the minimal proof and the running time of the SAT solver are tightly related. In the project we explore how graph decompositions of proofs (rather than formulas) can answer such questions in an innovative way.
[DF1999] R. Downey and M. Fellows, ¿Parameterized Complexity¿, Monographs in Computer Science (1999).
[RS1995] N. Robertson and P. Seymour, Graph Minors XIII: the disjoint paths problem, J. Comb. Theory Ser. B. (1995) 63:65 ¿ 110.
[GKMW2011] Grohe, Kawarabayashi, Marx, Wollan, Finding Topological Subgraphs is Fixed Parameter Tractable. Proc. STOC (2011), 479 ¿ 484.
[GSS2002] Gottlob, Scarcello, and Sideri. Fixed-Parameter Complexity in AI and Nonmonotonic Reasoning. Art. Int. (2002) 138:55¿86.
[BPR2000] Bonet, Pitassi, and Raz. On Interpolation and Automatization for Frege Systems. SIAM J. Comput. (2000) 29 (6):1939¿67.