Parameterized Proof Complexity

计算复杂性研究有效计算的可能性和局限性。传统上，一个问题被认为是易处理的，如果它允许一个多项式时间算法;所有这些问题的类形成复杂性类P。虽然P vs NP问题是现代计算机科学和数学的核心问题之一（正如克莱数学研究所在2000年提出的七个千年奖问题之一所证明的那样），但我们似乎离解决方案还很远。然而，在优化、人工智能、计算生物学和许多其他领域中，成千上万个具有重大实际意义的问题都是NP完全的。参数化的复杂性是现代主要的方法之一，它有助于理解易处理性和难处理性之间的精确边界。当P vs NP将计算问题的世界渲染成黑色和白色时，参数化复杂性利用了问题的额外结构，并揭示了一个更详细的画面。它的结果在许多NP难问题的算法解决方案，使用固定参数易处理性（FPT）的新概念。这种方法已经彻底改变了我们处理棘手问题的方式;许多经典的困难问题变得可解的大类相关instance.While参数化的复杂性已经深入研究在过去的二十年中，参数化的概念已经转移到证明复杂性由Dantchev，Martin，和Szeider（FOCS 2007）。证明复杂性研究定理证明的复杂性：在给定的证明系统中构造一个形式陈述的证明有多难？最短证明的长度是多少？这些问题与计算复杂性和逻辑学中的中心问题有着紧密的联系。事实上，证明的复杂性提供了一个主要的方法对P与NP问题通过库克的programme.This项目将是一个重大的贡献，对参数化证明的复杂性领域的发展。虽然最近的研究结果已经证明了这种方法的有效性，但还有许多基础性工作要做。类似地，参数化复杂性提供了运行时间的精细分类，参数化证明复杂性提供了对证明长度的更细粒度的分析。特别是，这导致许多公式的FPT大小证明，这些公式在经典设置中需要指数大小证明。与此同时，证明规模的下界也变得更加困难：首先是因为硬度的候选公式较少;其次是因为许多经典技术被证明是无效的。本项目将开发新技术，并重新评估现有的证明复杂性和计算复杂性技术在参数化证明复杂性中的适用性。这些技术进步将用于显示参数化证明系统的强下界，目前没有非平凡的下界是已知的。一个特殊的系统是参数化的解决方案与参数化公理的有效编码。除了它的复杂性和逻辑的联系，证明复杂性是主要的理论工具来分析现代SAT求解器的性能。这些算法具有非常精细的实现，成功地解决了大部分工业实例的布尔可满足性（SAT）的NP完全问题，这些实例来自软件验证或模型检查。该项目将开发新的算法方法来解决SAT问题，其灵感来自参数化证明复杂性的见解。一个特别的目标是改进基于DPLL的求解器的参数化算法。

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.