Jakob Nordström

The width of a resolution proof is the maximal number of literals in any clause of the proof. The space of a proof is the maximal number of memory cells used if the proof is only allowed to resolve on clauses kept in memory. Both of these measures have previously ... more >>>

Jakob Nordström

We present a greatly simplified proof of the length-space

trade-off result for resolution in Hertel and Pitassi (2007), and

also prove a couple of other theorems in the same vein. We point

out two important ingredients needed for our proofs to work, and

discuss possible conclusions to be drawn regarding ...
more >>>

Meena Mahajan, B. V. Raghavendra Rao

Functions in arithmetic NC1 are known to have equivalent constant

width polynomial degree circuits, but the converse containment is

unknown. In a partial answer to this question, we show that syntactic

multilinear circuits of constant width and polynomial degree can be

depth-reduced, though the resulting circuits need not be ...
more >>>

Alex Hertel, Alasdair Urquhart

We discovered a serious error in one of our previous submissions to ECCC and wish to make sure that this mistake is publicly known.

The main argument of the report TR06-133 is in error. The paper claims to prove the result of the title by reduction from the (Exists,k)-pebble game, ... more >>>

Eli Ben-Sasson, Jan Johannsen

It has been observed empirically that clause learning does not significantly improve the performance of a SAT solver when restricted

to learning clauses of small width only. This experience is supported by lower bound theorems. It is shown that lower bounds on the runtime of width-restricted clause learning follow from ...
more >>>

Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, Marc Vinyals

In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of CNF formulas is always an upper bound on the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies heavily on tools ... more >>>

Dmitry Itsykson, Mikhail Slabodkin, Dmitry Sokolov

The resolution complexity of the perfect matching principle was studied by Razborov [Raz04], who developed a technique for proving its lower bounds for dense graphs. We construct a constant degree bipartite graph $G_n$ such that the resolution complexity of the perfect matching principle for $G_n$ is $2^{\Omega(n)}$, where $n$ is ... more >>>

Albert Atserias, Massimo Lauria, Jakob Nordström

We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n^Omega(w). This shows that the simple counting argument that any formula refutable in width w must have a proof in size n^O(w) is essentially tight. ... more >>>

Alexander Razborov

In this paper we initiate the study of width in semi-algebraic proof systems

and various cut-based procedures in integer programming. We focus on two

important systems: Gomory-Chv\'atal cutting planes and

Lov\'asz-Schrijver lift-and-project procedures. We develop general methods for

proving width lower bounds and apply them to random $k$-CNFs and several ...
more >>>

Ilario Bonacina

Given an unsatisfiable $k$-CNF formula $\phi$ we consider two complexity measures in Resolution: width and total space. The width is the minimal $W$ such that there exists a Resolution refutation of $\phi$ with clauses of at most $W$ literals. The total space is the minimal size $T$ of a memory ... more >>>

Christoph Berkholz, Jakob Nordström

We show that there are CNF formulas which can be refuted in resolution

in both small space and small width, but for which any small-width

proof must have space exceeding by far the linear worst-case upper

bound. This significantly strengthens the space-width trade-offs in

[Ben-Sasson '09]}, and provides one more ...
more >>>