9 found
  1.  3
    An Exponential Separation Between the Parity Principle and the Pigeonhole Principle.Paul Beame & Toniann Pitassi - 1996 - Annals of Pure and Applied Logic 80 (3):195-228.
    The combinatorial parity principle states that there is no perfect matching on an odd number of vertices. This principle generalizes the pigeonhole principle, which states that for a fixed bipartition of the vertices, there is no perfect matching between them. Therefore, it follows from recent lower bounds for the pigeonhole principle that the parity principle requires exponential-size bounded-depth Frege proofs. Ajtai previously showed that the parity principle does not have polynomial-size bounded-depth Frege proofs even with the pigeonhole principle as an (...)
    Direct download (5 more)  
    Export citation  
    Bookmark   6 citations  
  2. Minimum Propositional Proof Length is NP-Hard to Linearly Approximate.Michael Alekhnovich, Sam Buss, Shlomo Moran & Toniann Pitassi - 2001 - Journal of Symbolic Logic 66 (1):171-191.
    We prove that the problem of determining the minimum propositional proof length is NP- hard to approximate within a factor of 2 log 1 - o(1) n . These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution, Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by (...)
    Direct download (8 more)  
    Export citation  
    Bookmark   2 citations  
  3.  35
    Lower Bounds for Cutting Planes Proofs with Small Coefficients.Maria Bonet, Toniann Pitassi & Ran Raz - 1997 - Journal of Symbolic Logic 62 (3):708-728.
    We consider small-weight Cutting Planes (CP * ) proofs; that is, Cutting Planes (CP) proofs with coefficients up to $\operatorname{Poly}(n)$ . We use the well known lower bounds for monotone complexity to prove an exponential lower bound for the length of CP * proofs, for a family of tautologies based on the clique function. Because Resolution is a special case of small-weight CP, our method also gives a new and simpler exponential lower bound for Resolution. We also prove the following (...)
    Direct download (9 more)  
    Export citation  
    Bookmark   3 citations  
  4.  51
    The Complexity of Analytic Tableaux.Noriko H. Arai, Toniann Pitassi & Alasdair Urquhart - 2006 - Journal of Symbolic Logic 71 (3):777 - 790.
    The method of analytic tableaux is employed in many introductory texts and has also been used quite extensively as a basis for automated theorem proving. In this paper, we discuss the complexity of the system as a method for refuting contradictory sets of clauses, and resolve several open questions. We discuss the three forms of analytic tableaux: clausal tableaux, generalized clausal tableaux, and binary tableaux. We resolve the relative complexity of these three forms of tableaux proofs and also resolve the (...)
    Direct download (5 more)  
    Export citation  
    Bookmark   1 citation  
  5.  14
    University of Azores, Ponta Delgada, Azores, Portugal June 30–July 4, 2010.Eric Allender, José L. Balcázar, Shafi Goldwasser, Denis Hirschfeldt, Sara Negri, Toniann Pitassi & Ronald de Wolf - 2011 - Bulletin of Symbolic Logic 17 (3).
    Direct download  
    Export citation  
  6. An Exponential Separation Between the Matching Principles and the Pigeonhole Principle, Forthcoming.Paul Beame & Toniann Pitassi - forthcoming - Annals of Pure and Applied Logic.
  7.  21
    Madison, WI, USA March 31–April 3, 2012.Alan Dow, Isaac Goldbring, Warren Goldfarb, Joseph Miller, Toniann Pitassi, Antonio Montalbán, Grigor Sargsyan, Sergei Starchenko & Moshe Vardi - 2013 - Bulletin of Symbolic Logic 19 (2).
  8.  42
    The Complexity of Resolution Refinements.Joshua Buresh-Oppenheim & Toniann Pitassi - 2007 - Journal of Symbolic Logic 72 (4):1336 - 1352.
    Resolution is the most widely studied approach to propositional theorem proving. In developing efficient resolution-based algorithms, dozens of variants and refinements of resolution have been studied from both the empirical and analytic sides. The most prominent of these refinements are: DP (ordered). DLL (tree), semantic, negative, linear and regular resolution. In this paper, we characterize and study these six refinements of resolution. We give a nearly complete characterization of the relative complexities of all six refinements. While many of the important (...)
    Direct download (4 more)  
    Export citation  
  9.  9
    University of California, San Diego, March 20–23, 1999.Julia F. Knight, Steffen Lempp, Toniann Pitassi, Hans Schoutens, Simon Thomas, Victor Vianu & Jindrich Zapletal - 1999 - Bulletin of Symbolic Logic 5 (3).