Parameterized Proof Complexity

计算复杂性研究高效计算的可能性和局限性。传统上，如果一个问题允许一个多项式时间算法，它就被认为是可处理的；所有这类问题的类别构成了复杂性类P。相反，如果一个问题与一个被认为超出了可处理范围的复杂性类(如NP)相关联，那么它就是困难的。虽然P与NP问题是现代计算机科学和数学的核心问题之一(2000年克莱数学研究所提出的七个千年奖问题之一就证明了这一点)，但我们似乎远未找到解决方案。然而，从字面上讲，从优化、人工智能、计算生物学以及许多更深的领域中，数以千计具有重大实际意义的问题都是NP-完全的。它们迫切需要为实际情况解决。参数化复杂性是帮助理解易处理和难处理之间的精确边界的主要现代方法之一。虽然P与NP将计算问题的世界描绘成黑白的，但参数化的复杂性利用了问题的额外结构，并揭示了更详细的图景。它使用固定参数可处理性(FPT)的新概念，为许多NP-Hard问题提供了算法解。这种方法彻底改变了我们今天处理棘手问题的方式；许多经典的困难问题变得可以在大类相关实例中求解。虽然参数化复杂性在过去20年中得到了深入的研究，但参数化的概念直到最近才被Dantchev，Martin和Szeider转移到证明复杂性(FOCS 2007)。证明复杂性研究定理证明的复杂性：在给定的证明系统中构造形式陈述的证明有多难？最短的校样有多长？这些问题与计算复杂性和逻辑方面的核心问题密切相关。事实上，证明复杂性是通过Cook的程序解决P与NP问题的主要方法之一。该项目将对参数证明复杂性领域的发展做出重大贡献。虽然最近的研究结果已经证明了这种方法的有效性，但还有很多基础性的工作要做。类似地，由于参数化复杂性提供了运行时间的精细分类，所以参数化证明复杂性提供了对证明长度的更细粒度的分析。特别是，这导致了在经典设置中需要指数大小的证明的许多公式的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.