Parameterized Proof Complexity

点击翻译按钮获取中文摘要

Computational complexity studies the possibilities and limitations of efficient computation. Traditionally, a problem has been perceived as tractable if it admits a polynomial-time algorithm; and the class of all such problems forms the complexity class P. Conversely, a problem is hard if it is associated with a complexity class believed to be beyond the realm of tractability like NP. While the P vs NP question is one of the central questions of modern computer science and mathematics (as witnessed by its inclusion as one of the seven Millennium Prize Problems posed by the Clay Mathematics Institute in 2000), we seem to be far from a solution. However, literally thousands of problems of great practical significance from optimisation, artificial intelligence, computational biology, and many further fields are known to be NP-complete. And they desperately need to be solved for practical instances.Parameterized complexity is one of the main modern approaches that help to understand the precise border between tractability and intractability. While P vs NP colours the world of computational problems into black and white, parameterized complexity exploits additional structure of the problems and reveals a much more detailed picture. It results in algorithmic solutions for many NP-hard problems using the new concept of fixed parameter tractability (FPT). This approach has revolutionised the way we approach intractable problems today; and many classically hard problems become solvable for large classes of relevant instances.While parameterized complexity has been intensively studied during the last two decades, the concept of parameterization has been only recently transferred to proof complexity by Dantchev, Martin, and Szeider (FOCS 2007). Proof complexity studies the complexity of theorem proving: how difficult is it to construct a proof of a formal statement in a given proof system? What is the length of the shortest proof? These questions have tight relations to central problems in computational complexity and logic. Indeed, proof complexity offers one of the main approaches towards the P vs NP question via Cook's programme.This project will be a substantial contribution towards the development of the field of parameterized proof complexity. While recent findings have already proved the effectiveness of the approach, much foundational work lies ahead. Similarly as parameterized complexity provides a fine classification of running times, parameterized proof complexity offers a more fine-grained analysis of lengths of proofs. In particular, this results in FPT-size proofs for many formulas that require exponential-size proofs in the classical setting. At the same time, showing lower bounds to the size of proofs becomes much harder: firstly, because there are less candidate formulas for hardness; and secondly, because many classical techniques turn out to be ineffective.This project will develop new techniques and reassess current techniques in proof complexity and computational complexity for their applicability in parameterized proof complexity. These technical advances will be used to show strong lower bounds for parameterized proof systems where currently no non-trivial lower bounds are known. A particular system of interest is parameterized resolution with an efficient encoding of parameterized axioms.In addition to its links to complexity and logic, proof complexity is the main theoretical tool to analyse the performance of modern SAT solvers. These are algorithms with very fine-tuned implementations that successfully solve the NP-complete problem of boolean satisfiability (SAT) for large fractions of industrial instances stemming from applications as software verification or model checking. This project will develop new algorithmic approaches to SAT solving inspired by insights from parameterized proof complexity. One particular goal are parameterized algorithms that refine DPLL-based solvers.