We continue a study initiated by Krajicek of a Resolution-like proof system working with clauses of linear inequalities, R(CP). For all proof systems of this kind Krajicek proved in [1] an exponential lower bound of t...
详细信息
ISBN:
(纸本)9783540727873
We continue a study initiated by Krajicek of a Resolution-like proof system working with clauses of linear inequalities, R(CP). For all proof systems of this kind Krajicek proved in [1] an exponential lower bound of the form: exp(n(Omega(1)))/M-O(W log2n), where M is the maximal absolute value of coefficients in a given proof and W is the maximal clause width. In this paper we improve this lower bound. For tree-like R(CP)-like proof systems we remove a dependence on the maximal absolute value of coefficients M, hence, we give the answer to an open question from [2]. proof follows from an upper bound on the real communication complexity of a polyhedra.
We present a reduction from the Pigeon-Hole Principle to the classical Sperner Lemma. The reduction is used 1. to show that the Sperner Lemma does not have a short constant-depth Frege proof, and 2. to prove lower bou...
详细信息
ISBN:
(纸本)3540354662
We present a reduction from the Pigeon-Hole Principle to the classical Sperner Lemma. The reduction is used 1. to show that the Sperner Lemma does not have a short constant-depth Frege proof, and 2. to prove lower bounds on the Query complexity of the Sperner Lemma in the Black-Box model of Computation.
We show that constant-depth Frege systems with counting axioms modulo m polynomially simulate Nullstellensatz refutations modulo m. Central to this is a new definition of reducibility from propositional formulas to sy...
详细信息
We show that constant-depth Frege systems with counting axioms modulo m polynomially simulate Nullstellensatz refutations modulo m. Central to this is a new definition of reducibility from propositional formulas to systems of polynomials. Using our definition of reducibility, most previously studied propositional formulas reduce to their polynomial translations. When combined with a previous result of the authors, this establishes the first size separation between Nullstellensatz and polynomial calculus refutations. We also obtain new upper bounds on refutation sizes for certain CNFs in constant-depth Frege with counting axioms systems.
By a well-known result of Cook and Reckhow [S.A. Cook, R.A. Reckhow, The relative efficiency of propositionalproof systems, Journal of Symbolic Logic 44 (1) (1979) 36-50;R.A. Reckhow, On the lengths of proofs in the ...
详细信息
By a well-known result of Cook and Reckhow [S.A. Cook, R.A. Reckhow, The relative efficiency of propositionalproof systems, Journal of Symbolic Logic 44 (1) (1979) 36-50;R.A. Reckhow, On the lengths of proofs in the propositional calculus, Ph.D. Thesis, Department of Computer Science, University of Toronto, 1976], all Frege systems for the classical propositional calculus (CPC) are polynomially equivalent. Mints and Kojevnikov [G. Mints, A. Kojevnikov, Intuitionistic Frege systems are polynomially equivalent, Zapiski Nauchnyh Seminarov POMI 316 (2004) 129-146] have recently shown p-equivalence of Frege systems for the intuitionistic propositional calculus (IPC) in the standard language, building on a description of admissible rules of IPC by Iemhoff [R. Iemhoff, On the admissible rules of intuitionistic propositional logic, Journal of Symbolic Logic 66 (1) (2001) 281-294]. We prove a similar result for an infinite family of normal modal logics, including K4, GL, S4, and S4Grz. (c) 2006 Elsevier B.V. All rights reserved.
We prove that the Cutting Plane proof system based on Gomory-Chvatal cuts polynomially simulates the lift-and-project system with integer coefficients written in unary. The restriction on the coefficients can be omitt...
详细信息
We prove that the Cutting Plane proof system based on Gomory-Chvatal cuts polynomially simulates the lift-and-project system with integer coefficients written in unary. The restriction on the coefficients can be omitted when using Krajicek's cut-free Gentzen-style extension of both systems. We also prove that Tseitin tautologies have short proofs in this extension (of any of these systems and with any coefficients). (c) 2005 Elsevier B.V. All rights reserved.
Res(k) is a propositionalproof system that extends resolution by working with k-DNFs instead of clauses. We show that there exist constants beta, gamma > 0 so that if k is a function from positive integers to posi...
详细信息
Res(k) is a propositionalproof system that extends resolution by working with k-DNFs instead of clauses. We show that there exist constants beta, gamma > 0 so that if k is a function from positive integers to positive integers so that for all n, k(n) less than or equal to beta log n, then for each n, there exists a set of clauses C-n of size n(O(1)) that has Res(k(n) + 1) refutations of size n(O(1)), yet every Res(k(n)) refutation of C-n has size at least 2(ngamma). (C) 2004 Elsevier B.V. All rights reserved.
A propositionalproof system is automatizable if there is an algorithm that, given a tautology, produces a proof in time polynomial in the size of its smallest proof. This notion can be weakened if we allow the algori...
详细信息
A propositionalproof system is automatizable if there is an algorithm that, given a tautology, produces a proof in time polynomial in the size of its smallest proof. This notion can be weakened if we allow the algorithm to produce a proof in a stronger system within the same time bound. This new notion is called weak antomatizability. Among other characterizations, we prove that a system is weakly automatizable exactly when a weak form of the satisfiability problem is solvable in polynomial time. After studying the robustness of the definition, we prove the equivalence between: (i). Resolution is weakly automatizable, (ii) Res(k) is weakly automatizable, and (iii) Res(k) has feasible interpolation, when k > 1. In order to prove this result, we show that Res(2) has polynomial-size proofs of the reflection principle of Resolution, which is a version of consistency. We also show that Res(k), for every k > 1, proves its consistency in polynomial size, while Resolution does not. In fact, we show that Resolution proofs of its own consistency require almost exponential size. This gives a better lower bound for the monotone interpolation of Res(2) and a separation from Resolutionas a byproduct. Our techniques also give us a way to obtain a large class of examples that have small Resolution refutations but require relatively large width. This answers a question of Alekhnovich and Razborov related to whether Resolution is automatizable in quasipolynomial-time. (C) 2003 Elsevier Inc. All rights reserved.
We prove a new switching lemma that works for restrictions that set only a small fraction of the variables and is applicable to formulas in disjunctive normal form (DNFs) with small terms. We use this to prove lower b...
详细信息
We prove a new switching lemma that works for restrictions that set only a small fraction of the variables and is applicable to formulas in disjunctive normal form (DNFs) with small terms. We use this to prove lower bounds for the Res(k) propositionalproof system, an extension of resolution which works with k-DNFs instead of clauses. We also obtain an exponential separation between depth d circuits of bottom fan-in k and depth d circuits of bottom fan-in k+1. Our results for Res(k) are as follows: 1. The 2n to n weak pigeonhole principle requires exponential size to refute in Res(k) for krootlog n/log log n. 2. For each constant k, there exists a constant w>k so that random w-CNFs require exponential size to refute in Res(k). 3. For each constant k, there are sets of clauses which have polynomial size Res(k+1) refutations but which require exponential size Res(k) refutations.
We prove a quasi-polynomial lower bound on the size of bounded-depth Frege proofs of the pigeonhole principle PHPnm where m = (1 + 1/ polylog n)n. This lower bound qualitatively matches the known quasi-polynomial-size...
详细信息
We prove a quasi-polynomial lower bound on the size of bounded-depth Frege proofs of the pigeonhole principle PHPnm where m = (1 + 1/ polylog n)n. This lower bound qualitatively matches the known quasi-polynomial-size bounded-depth Frege proofs for these principles. Our technique, which uses a switching lemma argument like other lower bounds for bounded-depth Frege proofs, is novel in that the tautology to which this switching lemma is applied remains random throughout the argument.
Mutilated chessboard principle CB, says that it is impossible to cover by domino tiles the chessboard 2n x 2n with two diagonally opposite corners removed. We prove Omega((rootn)) lower bound on the size of minimal re...
详细信息
Mutilated chessboard principle CB, says that it is impossible to cover by domino tiles the chessboard 2n x 2n with two diagonally opposite corners removed. We prove Omega((rootn)) lower bound on the size of minimal resolution refutation of CBn. (C) 2003 Elsevier B.V. All rights reserved.
暂无评论