排序方式: 共有12条查询结果,搜索用时 31 毫秒
1.
In this paper we prove an exponential lower bound on the size of bounded-depth Frege proofs for the pigeonhole principle (PHP). We also obtain an (loglogn)-depth lower bound for any polynomial-sized Frege proof of the pigeonhole principle. Our theorem nearly completes the search for the exact complexity of the PHP, as S. Buss has constructed polynomial-size, logn-depth Frege proofs for the PHP. The main lemma in our proof can be viewed as a general Håstad-style Switching Lemma for restrictions that are partial matchings. Our lower bounds for the pigeonhole principle improve on previous superpolynomial lower bounds. 相似文献
2.
3.
Michael Alekhnovich Allan Borodin Joshua Buresh-Oppenheim Russell Impagliazzo Avner Magen Toniann Pitassi 《Computational Complexity》2011,20(4):679-740
We propose a model called priority branching trees (pBT) for backtracking and dynamic programming algorithms. Our model generalizes both the priority model of Borodin, Nielson and
Rackoff, as well as a simple dynamic programming model due to Woeginger, and hence spans a wide spectrum of algorithms. After
witnessing the strength of the model, we then show its limitations by providing lower bounds for algorithms in this model
for several classical problems such as Interval Scheduling, Knapsack and Satisfiability. 相似文献
4.
5.
Maria Luisa Bonet Carlos Domingo Ricard Gavaldà Alexis Maciel Toniann Pitassi 《Computational Complexity》2004,13(1-2):47-68
In this paper, we show how to extend the argument due to Bonet, Pitassi and Raz to show that bounded-depth Frege proofs do not have feasible interpolation, assuming that factoring of Blum integers or computing the Diffie–Hellman function is sufficiently hard. It follows as a corollary that bounded-depth Frege is not automatizable; in other words, there is no deterministic polynomial-time algorithm that will output a short proof if one exists. A notable feature of our argument is its simplicity. 相似文献
6.
7.
8.
Joshua Buresh-Oppenheim Matthew Clegg Russell Impagliazzo Toniann Pitassi 《Computational Complexity》2002,11(3-4):91-108
In standard implementations of the Gröbner basis algorithm,
the original polynomials are homogenized so that each term in a given
polynomial has the same degree. In this paper, we study the effect of
homogenization on the proof complexity of refutations of polynomials
derived from Boolean formulas in both the Polynomial Calculus (PC)
and Nullstellensatz systems. We show that the PC refutations of homogenized
formulas give crucial information about the complexity of the
original formulas. The minimum PC refutation degree of homogenized
formulas is equal to the Nullstellensatz refutation degree of the original
formulas, whereas the size of the homogenized PC refutation is equal
to the size of the PC refutation for the originals. Using this relationship,
we prove nearly linear ((n/log n) vs. O(1)) separations between
Nullstellensatz and PC degree, for a family of explicitly constructed contradictory
3CNF formulas. Previously, an (n
1/2) separation had been
proved for equations that did not correspond to any CNF formulas, and
a log n separation for equations derived from kCNF formulas. 相似文献
9.
It is known that constant-depth Frege proofs of some tautologies require exponential size. No such lower bound result is known for more general proof systems. We consider tree-like sequent calculus proofs in which formulas can contain modular connectives and only the cut formulas are restricted to be of constant depth. Under a plausible hardness assumption concerning small-depth Boolean circuits, we prove exponential lower bounds for such proofs. We prove these lower bounds directly from the computational hardness assumption. We start with a lower bound for cut-free proofs and “lift” it so it applies to proofs with constant-depth cuts. By using the same approach, we obtain the following additional results. We provide a much simpler proof of a known unconditional lower bound in the case where modular connectives are not used. We establish a conditional exponential separation between the power of constant-depth proofs that use different modular connectives. We show that these tree-like proofs with constant-depth cuts cannot polynomially simulate similar dag-like proofs, even when the dag-like proofs are cut-free. We present a new proof of the non-finite axiomatizability of the theory of bounded arithmetic I Δ0(R). Finally, under a plausible hardness assumption concerning the polynomial-time hierarchy, we show that the hierarchy \({G_i^*}\) of quantified propositional proof systems does not collapse. 相似文献
10.
We consider the problem of determining, given a graph G with specified nodes s and t, whether or not there is a path of at most k edges in G from s to t. We show that solving this problem on polynomialsize unbounded fan-in circuits requires depth , improving on a depth lower bound of when given by Ajtai (1989), Bellantoni et al. (1992). More generally, we obtain an improved size-depth tradeoff lower bound for the problem for all .?The key to our technique is a new form of “switching lemma” which combines some of the features of iteratively shortening
terms due to Furst et al. (1984) and Ajtai (1983) with the features of switching lemma arguments introduced by Yao (1985), H?stad (1987), and Cai
(1986) that have been the methods of choice for subsequent results.
Received: July 2, 1996. 相似文献