Studies in Proof Complexity and Circuit Complexity

证明复杂性和电路复杂性研究

• 批准号: 9820831
• 负责人: Toniann Pitassi
• 金额: $ 7.12万
• 依托单位: University of Arizona
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1999
• 资助国家: 美国
• 起止时间: 1999-09-01 至 2003-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9820831&HistoricalAwards=false
• 关键词: Studies; Proof; Complexity; Circuit

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.

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