Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > KEYWORD > PROPOSITIONAL PROOF COMPLEXITY:
Reports tagged with propositional proof complexity:
TR99-040 | 20th October 1999
Michael Alekhnovich, Eli Ben-Sasson, Alexander Razborov, Avi Wigderson

#### Space Complexity in Propositional Calculus

We study space complexity in the framework of
propositional proofs. We consider a natural model analogous to
Turing machines with a read-only input tape, and such
popular propositional proof systems as Resolution, Polynomial
Calculus and Frege systems. We propose two different space measures,
corresponding to the maximal number of bits, ... more >>>

TR00-023 | 11th May 2000
Michael Alekhnovich, Eli Ben-Sasson, Alexander Razborov, Avi Wigderson

#### Pseudorandom Generators in Propositional Proof Complexity

We call a pseudorandom generator $G_n:\{0,1\}^n\to \{0,1\}^m$ {\em
hard} for a propositional proof system $P$ if $P$ can not efficiently
prove the (properly encoded) statement $G_n(x_1,\ldots,x_n)\neq b$ for
{\em any} string $b\in\{0,1\}^m$. We consider a variety of
combinatorial'' pseudorandom generators inspired by the
Nisan-Wigderson generator on the one hand, and ... more >>>

TR01-055 | 26th July 2001
Alexander Razborov

#### Improved Resolution Lower Bounds for the Weak Pigeonhole Principle

Recently, Raz established exponential lower bounds on the size
of resolution proofs of the weak pigeonhole principle. We give another
proof of this result which leads to better numerical bounds. Specifically,
we show that every resolution proof of $PHP^m_n$ must have size
$\exp\of{\Omega(n/\log m)^{1/2}}$ which implies an
$\exp\of{\Omega(n^{1/3})}$ bound when ... more >>>

TR01-056 | 6th August 2001
Michael Alekhnovich, Jan Johannsen, Alasdair Urquhart

#### An Exponential Separation between Regular and General Resolution

This paper gives two distinct proofs of an exponential separation
between regular resolution and unrestricted resolution.
The previous best known separation between these systems was
quasi-polynomial.

more >>>

TR01-075 | 2nd November 2001
Alexander Razborov

#### Resolution Lower Bounds for the Weak Functional Pigeonhole Principle

We show that every resolution proof of the {\em functional} version
$FPHP^m_n$ of the pigeonhole principle (in which one pigeon may not split
between several holes) must have size $\exp\of{\Omega\of{\frac n{(\log m)^2}}}$. This implies an $\exp\of{\Omega(n^{1/3})}$ bound when the number
of pigeons $m$ is arbitrary.

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 >>>

TR03-041 | 29th May 2003
Albert Atserias, Maria Luisa Bonet, Jordi Levy

#### On Chvatal Rank and Cutting Planes Proofs

We study the Chv\'atal rank of polytopes as a complexity measure of
unsatisfiable sets of clauses. Our first result establishes a
connection between the Chv\'atal rank and the minimum refutation
length in the cutting planes proof system. The result implies that
length lower bounds for cutting planes, or even for ... more >>>

TR07-010 | 4th January 2007
Arist Kojevnikov

#### Improved Lower Bounds for Resolution over Linear Inequalities

Revisions: 1

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 an exponential lower bound that depends
on the maximal absolute value of coefficients in the given proof and
the maximal clause width.

... more >>>

TR07-107 | 26th October 2007
Nathan Segerlind

#### Exponential lower bounds and integrality gaps for tree-like Lovasz-Schrijver procedures

The matrix cuts of Lov{\'{a}}sz and Schrijver are methods for tightening linear relaxations of zero-one programs by the addition of new linear inequalities. We address the question of how many new inequalities are necessary to approximate certain combinatorial problems with strong guarantees, and to solve certain instances of Boolean satisfiability.

... more >>>

TR07-126 | 5th November 2007
Nathan Segerlind

#### On the relative efficiency of resolution-like proofs and ordered binary decision diagram proofs

We show that tree-like OBDD proofs of unsatisfiability require an exponential increase ($s \mapsto 2^{s^{\Omega(1)}}$) in proof size to simulate unrestricted resolution, and that unrestricted OBDD proofs of unsatisfiability require an almost-exponential increase ($s \mapsto 2^{ 2^{\left( \log s \right)^{\Omega(1)}}}$) in proof size to simulate $\Res{O(\log n)}$. The OBDD proof ... more >>>

TR09-002 | 23rd November 2008
Eli Ben-Sasson, Jakob Nordström

#### Short Proofs May Be Spacious: An Optimal Separation of Space and Length in Resolution

A number of works have looked at the relationship between length and space of resolution proofs. A notorious question has been whether the existence of a short proof implies the existence of a proof that can be verified using limited space.

In this paper we resolve the question by answering ... more >>>

TR09-014 | 7th February 2009
Soren Riis

#### On the asymptotic Nullstellensatz and Polynomial Calculus proof complexity

We show that the asymptotic complexity of uniformly generated (expressible in First-Order (FO) logic) propositional tautologies for the Nullstellensatz proof system (NS) as well as for Polynomial Calculus, (PC) has four distinct types of asymptotic behavior over fields of finite characteristic. More precisely, based on some highly non-trivial work by ... more >>>

TR10-197 | 14th December 2010
Albert Atserias, Elitza Maneva

#### Mean-payoff games and propositional proofs

We associate a CNF-formula to every instance of the mean-payoff game problem in such a way that if the value of the game is non-negative the formula is satisfiable, and if the value of the game is negative the formula has a polynomial-size refutation in $\Sigma_2$-Frege (i.e.~DNF-resolution). This reduces mean-payoff ... more >>>

TR13-018 | 29th January 2013
Luke Friedman, Yixin Xu

#### Exponential Lower Bounds for Refuting Random Formulas Using Ordered Binary Decision Diagrams

A propositional proof system based on ordered binary decision diagrams (OBDDs) was introduced by Atserias et al. Krajicek proved exponential lower bounds for a strong variant of this system using feasible interpolation, and Tveretina et al. proved exponential lower bounds for restricted versions of this system for refuting formulas derived ... more >>>

TR13-027 | 29th January 2013
Luke Friedman

#### A Framework for Proving Proof Complexity Lower Bounds on Random CNFs Using Encoding Techniques

Propositional proof complexity is an area of complexity theory that addresses the question of whether the class NP is closed under complement, and also provides a theoretical framework for studying practical applications such as SAT solving.
Some of the most well-studied contradictions are random $k$-CNF formulas where each clause of ... more >>>

TR20-037 | 18th March 2020
Michal Garlik

#### Failure of Feasible Disjunction Property for $k$-DNF Resolution and NP-hardness of Automating It

We show that for every integer $k \geq 2$, the Res($k$) propositional proof system does not have the weak feasible disjunction property. Next, we generalize a recent result of Atserias and Müller [FOCS, 2019] to Res($k$). We show that if NP is not included in P (resp. QP, SUBEXP) then ... more >>>

ISSN 1433-8092 | Imprint