Computational and Proof Complexity Bounds

本研究解决了各种计算环境下的问题，在每种情况下，研究的一个重要目标是获得问题复杂性的新下界。我们感兴趣的主要计算设置是，命题重言式证明的复杂性是基本的，因为它相当于NP与co-NP问题。分析特定证明方法的复杂性对其本身以及自动定理证明的实际问题都很重要，并且可能产生对NP与co-NP问题的见解。在这一领域的研究是关于扩展复杂性界已知的证明系统的范围，特别强调随机选择的k-CNF公式的研究。根据以往的经验，研究电路复杂性的方法有望在这一分析中发挥作用。第二个感兴趣的设置是能够以单位成本对字级数量进行操作的随机存取机器的计算复杂性。对于许多问题，例如排序，在这个模型中已经显示出惊人的高效算法。该领域研究的目标是了解该模型中可能的算法改进的局限性。最后的设置是表示布尔函数的复杂性，以便于它们易于操作和比较，这是符号模型检查算法的重要属性。在这一领域要研究的主要问题是易于操作和比较的表示是否可以有效地表示非线性和线性函数。

This research addresses problems in a variety of computational settings, In each case, a significant goal of the research is to obtain new lower bounds on the problems' complexity. The prime computational setting of interest is that of the complexity of proofs in propositional tautologies is fundmental in that it is equivalent to the NP versus co-NP question. Analysis of the complexity of specific methods of proof is important in its own right as well as for practical questions of automated theorem- proving and may yield insight into the NP versus co-NP question. The research in this area is concerned with extending the range of proof systems in which complexity bounds are currently known, with particular emphasis on the study of randomly chosen k-CNF formulas. Based on past experience, methods from the study of circuit complexity are expected to be useful in this analysis. The second setting of interest is the complexity of computations on random access machines able to operate on word-level quantities at unit cost. Surprisingly efficient algorithms for a number of problems, such as sorting, have been shown in this model. The goal of the research in this area is to understand the limits of the algorithmic improvements possible in this model. The final setting is that of the complexity of representing Boolean functions so that they are easy to manipulate and compare, important properties for symbolic model checking algorithms. The major question to investigate in this area is whether representations which are easy to manipulate and compare can efficiently represent non-linear as well as linear functions.