Studies in Proof Complexity and Circuit Complexity

复杂性理论的中心问题是理解哪些问题可以有效地解决。命题证明复杂性的核心问题是理解在标准证明系统中哪些重言式具有有效的证明。这两个研究领域之间有许多相互联系，在过去的十年里，通过结合和混合这两个领域的想法，取得了令人振奋的新结果。这个研究项目的总体目标是在这两个领域(电路复杂性和证明复杂性)取得进展，重点是证明命题证明系统的下界。一个焦点是代数证明系统的复杂性：这些系统是从Grobner基算法派生出来的自然证明系统。为了说明它们的基本性质，已经有了一些代数下界的应用，包括NP搜索问题的下界，有界深度Frege证明的下界，以及可满足性测试的新算法。研究的相关问题包括：随机公式的复杂性，解决P=？NP问题所需的证明论强度，以及与代数电路下界的联系。上述理论工作的一个补充方面是建立良好的可满足性测试算法。有一种越来越多的趋势来解决许多问题，特别是在人工智能领域，使用启发式算法来实现可满足性。这些算法通常是标准证明搜索方法的变体(即，分辨率的随机版本)，并且在经验上表现得相当好。然而，对于启发式方法如何、为什么以及在哪些条件下工作得很好，几乎没有分析结果。这项研究的一个目标是提供有意义的分析结果，并为SAT和SSAT(随机SAT)开发新的算法，以改进现有的最先进算法。

CCR-9820831PitassiThe central problem in complexity theory is to understand which problems can be solved efficiently. The central problem in propositional proof complexity is to understand which tautologies have efficient proofs in standard proof systems. There are many interconnections between these two lines of research, and in the last decade exciting new results have been obtained by combining and mixing ideas from both fields. The overall aim of this research project is to make progress in both of these areas (circuit complexity and proof complexity) with emphasis on proving lower bounds for propositional proof systems. A focus is the complexity of algebraic proof systems: these are natural proof systems derived from the Grobner basis algorithm. To illustrate their fundamental nature, there have already been several applications of algebraic lower bounds, including lower bounds for NP-search problems, lower bounds for bounded depth Frege proofs, and new algorithms for satisfiability testing. Related problems investigated include: the complexity of random formulas, the proof-theoretic strength required to resolve the P=?NP question, and connections to algebraic circuit lower bounds.A complementary facet of the theoretical work described above is to build good algorithms for satisfiability testing. There has been an increasing trend to solve many problems, particular in AI domains, with heuristics for satisfiability. These algorithms are typically variations of standard proof search methods (i.e., randomized versions of resolution) and perform quite well empirically. However, almost no analytical results are known as to how, why and under which conditions the heuristics work well. A goal of this research is to provide analytical results that are meaningful, and to develop new algorithms for SAT and SSAT (stochastic SAT) that improve upon existing state-of-the-art algorithms.