Michael Alekhnovich, Eli Ben-Sasson, Alexander Razborov, Avi Wigderson

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

Michael Alekhnovich, Eli Ben-Sasson, Alexander Razborov, Avi Wigderson

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

Alexander Razborov

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

Michael Alekhnovich, Jan Johannsen, Alasdair Urquhart

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.

Alexander Razborov

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.

Albert Atserias, Maria Luisa Bonet

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

Albert Atserias, Maria Luisa Bonet, Jordi Levy

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

Arist Kojevnikov

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.

Nathan Segerlind

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

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

Eli Ben-Sasson, Jakob Nordström

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

Soren Riis

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

Albert Atserias, Elitza Maneva

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

Luke Friedman, Yixin Xu

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

Luke Friedman

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

Michal Garlik

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

Nashlen Govindasamy, Tuomas Hakoniemi, Iddo Tzameret

We prove super-polynomial lower bounds on the size of propositional proof systems operating with constant-depth algebraic circuits over fields of zero characteristic. Specifically, we show that the subset-sum variant $\sum_{i,j,k,l\in[n]} z_{ijkl}x_ix_jx_kx_l-\beta = 0$, for Boolean variables, does not have polynomial-size IPS refutations where the refutations are multilinear and written as ... more >>>