Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > KEYWORD > PIGEONHOLE PRINCIPLE:
Reports tagged with Pigeonhole Principle:
TR97-007 | 21st February 1997
Stasys Jukna

#### Exponential Lower Bounds for Semantic Resolution

In a semantic resolution proof we operate with clauses only
but allow {\em arbitrary} rules of inference:

C_1 C_2 ... C_m
__________________
C

Consistency is the only requirement. We prove a very simple
exponential lower bound for the size ... more >>>

TR02-010 | 21st January 2002
Albert Atserias, Maria Luisa Bonet

#### On the Automatizability of Resolution and Related Propositional Proof Systems

Having good algorithms to verify tautologies as efficiently as possible
is of prime interest in different fields of computer science.
In this paper we present an algorithm for finding Resolution refutations
based on finding tree-like Res(k) refutations. The algorithm is based on
the one of Beame and Pitassi \cite{BP96} ... more >>>

TR02-023 | 16th April 2002
Josh Buresh-Oppenheim, Paul Beame, Ran Raz, Ashish Sabharwal

#### Bounded-depth Frege lower bounds for weaker pigeonhole principles

Revisions: 1

We prove a quasi-polynomial lower bound on the size of bounded-depth
Frege proofs of the pigeonhole principle $PHP^{m}_n$ 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 ... more >>>

TR20-012 | 14th February 2020
Dmitry Sokolov

#### (Semi)Algebraic Proofs over $\{\pm 1\}$ Variables

One of the major open problems in proof complexity is to prove lower bounds on $AC_0[p]$-Frege proof
systems. As a step toward this goal Impagliazzo, Mouli and Pitassi in a recent paper suggested to prove
lower bounds on the size for Polynomial Calculus over the $\{\pm 1\}$ basis. In this ... more >>>

ISSN 1433-8092 | Imprint