Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

Reports tagged with Space:
TR01-031 | 5th April 2001
Eli Ben-Sasson, Nicola Galesi

Space Complexity of Random Formulae in Resolution

We study the space complexity of refuting unsatisfiable random $k$-CNFs in
the Resolution proof system. We prove that for any large enough $\Delta$,
with high probability a random $k$-CNF over $n$ variables and $\Delta n$
clauses requires resolution clause space of
$\Omega(n \cdot \Delta^{-\frac{1+\epsilon}{k-2-\epsilon}})$,
for any $0<\epsilon<1/2$. For constant $\Delta$, ... more >>>

TR01-079 | 6th September 2001
Michele Zito

An Upper Bound on the Space Complexity of Random Formulae in Resolution

We prove that, with high probability, the space complexity of refuting
a random unsatisfiable boolean formula in $k$-CNF on $n$
variables and $m = \Delta n$ clauses is
$O(n \cdot \Delta^{-\frac{1}{k-2}})$.

more >>>

TR03-044 | 12th May 2003
Juan Luis Esteban, Jacobo Toran

A Combinatorial Characterization of Treelike Resolution Space

We show that the Player-Adversary game from a paper
by Pudlak and Impagliazzo played over
CNF propositional formulas gives
an exact characterization of the space needed
in treelike resolution refutations. This
characterization is purely combinatorial
and independent of the notion of resolution.
We use this characterization to give ... more >>>

TR05-066 | 4th June 2005
Jakob Nordström

Narrow Proofs May Be Spacious: Separating Space and Width in Resolution

Revisions: 2 , Comments: 1

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

TR06-103 | 5th July 2006
Oded Lachish, Ilan Newman, Asaf Shapira

Space Complexity vs. Query Complexity

Combinatorial property testing deals with the following relaxation
of decision problems: Given a fixed property and an input $x$, one
wants to decide whether $x$ satisfies the property or is ``far''
from satisfying it. The main focus of property testing is in
identifying large families of properties that can be ... more >>>

TR07-046 | 23rd April 2007
Philipp Hertel

An Exponential Time/Space Speedup For Resolution

Comments: 1

Satisfiability algorithms have become one of the most practical and successful approaches for solving a variety of real-world problems, including hardware verification, experimental design, planning and diagnosis problems. The main reason for the success is due to highly optimized algorithms for SAT based on resolution. The most successful of these ... more >>>

TR07-114 | 28th September 2007
Jakob Nordström

A Simplified Way of Proving Trade-off Results for Resolution

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

TR08-026 | 28th February 2008
Jakob Nordström, Johan Hastad

Towards an Optimal Separation of Space and Length in Resolution

Most state-of-the-art satisfiability algorithms today are variants of
the DPLL procedure augmented with clause learning. The main bottleneck
for such algorithms, other than the obvious one of time, is the amount
of memory used. In the field of proof complexity, the resources of
time and memory correspond to the length ... more >>>

TR09-034 | 25th March 2009
Eli Ben-Sasson, Jakob Nordström

Understanding Space in Resolution: Optimal Lower Bounds and Exponential Trade-offs

Comments: 1

For current state-of-the-art satisfiability algorithms based on the
DPLL procedure and clause learning, the two main bottlenecks are the
amounts of time and memory used. Understanding time and memory
consumption, and how they are related to one another, is therefore a
question of considerable practical importance. In the field of ... more >>>

TR09-047 | 20th April 2009
Eli Ben-Sasson, Jakob Nordström

A Space Hierarchy for k-DNF Resolution

Comments: 1

The k-DNF resolution proof systems are a family of systems indexed by
the integer k, where the kth member is restricted to operating with
formulas in disjunctive normal form with all terms of bounded arity k
(k-DNF formulas). This family was introduced in [Krajicek 2001] as an
extension of the ... more >>>

TR10-045 | 15th March 2010
Jakob Nordström

On the Relative Strength of Pebbling and Resolution

Revisions: 1

The last decade has seen a revival of interest in pebble games in the
context of proof complexity. Pebbling has proven to be a useful tool
for studying resolution-based proof systems when comparing the
strength of different subsystems, showing bounds on proof space, and
establishing size-space trade-offs. The typical approach ... more >>>

TR10-125 | 11th August 2010
Eli Ben-Sasson, Jakob Nordström

Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions

For current state-of-the-art satisfiability algorithms based on the DPLL procedure and clause learning, the two main bottlenecks are the amounts of time and memory used. In the field of proof complexity, these resources correspond to the length and space of resolution proofs for formulas in conjunctive normal form (CNF). There ... more >>>

TR12-132 | 21st October 2012
Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga Ron-Zewi, Neil Thapen

Space Complexity in Polynomial Calculus

During the last decade, an active line of research in proof complexity has been to study space complexity and time-space trade-offs for proofs. Besides being a natural complexity measure of intrinsic interest, space is also an important issue in SAT solving, and so research has mostly focused on weak systems ... more >>>

TR14-081 | 13th June 2014
Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, Marc Vinyals

From Small Space to Small Width in Resolution

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

TR14-138 | 29th October 2014
Nicola Galesi, Pavel Pudlak, Neil Thapen

The space complexity of cutting planes refutations

We study the space complexity of the cutting planes proof system, in which the lines in a proof are integral linear inequalities. We measure the space used by a refutation as the number of inequalities that need to be kept on a blackboard while verifying it. We show that any ... more >>>

TR15-005 | 5th January 2015
Chin Ho Lee, Emanuele Viola

Some limitations of the sum of small-bias distributions

Revisions: 1

We exhibit $\epsilon$-biased distributions $D$
on $n$ bits and functions $f\colon \{0,1\}^n
\to \{0,1\}$ such that the xor of two independent
copies ($D+D$) does not fool $f$, for any of the
following choices:

1. $\epsilon = 2^{-\Omega(n)}$ and $f$ is in P/poly;

2. $\epsilon = 2^{-\Omega(n/\log n)}$ and $f$ is ... more >>>

TR16-203 | 21st December 2016
Christoph Berkholz, Jakob Nordström

Supercritical Space-Width Trade-offs for Resolution

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

TR19-052 | 9th April 2019
Nicola Galesi, Leszek Kolodziejczyk, Neil Thapen

Polynomial calculus space and resolution width

We show that if a $k$-CNF requires width $w$ to refute in resolution, then it requires space $\sqrt w$ to refute in polynomial calculus, where the space of a polynomial calculus refutation is the number of monomials that must be kept in memory when working through the proof. This is ... more >>>

ISSN 1433-8092 | Imprint