All reports by Author Jakob Nordström:

__
TR20-064
| 2nd May 2020
__

Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere, Dmitry Sokolov, Susanna de Rezende#### Automating Algebraic Proof Systems is NP-Hard

Revisions: 1

__
TR20-001
| 31st December 2019
__

Or Meir, Jakob Nordström, Robert Robere, Susanna de Rezende#### Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling

Revisions: 2

__
TR19-186
| 31st December 2019
__

Or Meir, Jakob Nordström, Toniann Pitassi, Robert Robere, Susanna de Rezende#### Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity

Revisions: 4

__
TR19-174
| 2nd December 2019
__

Susanna de Rezende, Jakob Nordström, Kilian Risse, Dmitry Sokolov#### Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs

__
TR16-203
| 21st December 2016
__

Christoph Berkholz, Jakob Nordström#### Supercritical Space-Width Trade-offs for Resolution

__
TR16-135
| 31st August 2016
__

Christoph Berkholz, Jakob Nordström#### Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps

__
TR15-078
| 4th May 2015
__

Mladen Mikša, Jakob Nordström#### A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds

__
TR15-053
| 7th April 2015
__

Massimo Lauria, Jakob Nordström#### Tight Size-Degree Bounds for Sums-of-Squares Proofs

__
TR14-118
| 9th September 2014
__

Albert Atserias, Massimo Lauria, Jakob Nordström#### Narrow Proofs May Be Maximally Long

__
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

__
TR12-132
| 21st October 2012
__

Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga Ron-Zewi, Neil Thapen#### Space Complexity in Polynomial Calculus

__
TR10-136
| 26th August 2010
__

Arnab Bhattacharyya, Elena Grigorescu, Jakob Nordström, Ning Xie#### Separations of Matroid Freeness Properties

Revisions: 1

__
TR10-125
| 11th August 2010
__

Eli Ben-Sasson, Jakob Nordström#### Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions

__
TR10-045
| 15th March 2010
__

Jakob Nordström#### On the Relative Strength of Pebbling and Resolution

Revisions: 1

__
TR09-100
| 16th October 2009
__

Jakob Nordström, Alexander Razborov#### On Minimal Unsatisfiability and Time-Space Trade-offs for $k$-DNF Resolution

__
TR09-047
| 20th April 2009
__

Eli Ben-Sasson, Jakob Nordström#### A Space Hierarchy for k-DNF Resolution

Comments: 1

__
TR09-034
| 25th March 2009
__

Eli Ben-Sasson, Jakob Nordström#### Understanding Space in Resolution: Optimal Lower Bounds and Exponential Trade-offs

Comments: 1

__
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

__
TR08-026
| 28th February 2008
__

Jakob Nordström, Johan Håstad#### Towards an Optimal Separation of Space and Length in Resolution

__
TR07-114
| 28th September 2007
__

Jakob Nordström#### A Simplified Way of Proving Trade-off Results for Resolution

__
TR05-066
| 4th June 2005
__

Jakob Nordström#### Narrow Proofs May Be Spacious: Separating Space and Width in Resolution

Revisions: 2
,
Comments: 1

Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere, Dmitry Sokolov, Susanna de Rezende

We show that algebraic proofs are hard to find: Given an unsatisfiable CNF formula $F$, it is NP-hard to find a refutation of $F$ in the Nullstellensatz, Polynomial Calculus, or Sherali--Adams proof systems in time polynomial in the size of the shortest such refutation. Our work extends, and gives a ... more >>>

Or Meir, Jakob Nordström, Robert Robere, Susanna de Rezende

We establish an exactly tight relation between reversible pebblings of graphs and Nullstellensatz refutations of pebbling formulas, showing that a graph $G$ can be reversibly pebbled in time $t$ and space $s$ if and only if there is a Nullstellensatz refutation of the pebbling formula over $G$ in size $t+1$ ... more >>>

Or Meir, Jakob Nordström, Toniann Pitassi, Robert Robere, Susanna de Rezende

We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve two open ... more >>>

Susanna de Rezende, Jakob Nordström, Kilian Risse, Dmitry Sokolov

We show exponential lower bounds on resolution proof length for pigeonhole principle (PHP) formulas and perfect matching formulas over highly unbalanced, sparse expander graphs, thus answering the challenge to establish strong lower bounds in the regime between balanced constant-degree expanders as in [Ben-Sasson and Wigderson '01] and highly unbalanced, dense ... 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 >>>

Christoph Berkholz, Jakob Nordström

We prove near-optimal trade-offs for quantifier depth versus number of variables in first-order logic by exhibiting pairs of n-element structures that can be distinguished by a k-variable first-order sentence but where every such sentence requires quantifier depth at least n^?(k/log k). Our trade-offs also apply to first-order counting logic, and ... more >>>

Mladen Mikša, Jakob Nordström

We study the problem of obtaining lower bounds for polynomial calculus (PC) and polynomial calculus resolution (PCR) on proof degree, and hence by [Impagliazzo et al. '99] also on proof size. [Alekhnovich and Razborov '03] established that if the clause-variable incidence graph of a CNF formula F is a good ... more >>>

Massimo Lauria, Jakob Nordström

We exhibit families of 4-CNF formulas over n variables that have sums-of-squares (SOS) proofs of unsatisfiability of degree (a.k.a. rank) d but require SOS proofs of size n^{Omega(d)} for values of d = d(n) from constant all the way up to n^{delta} for some universal constant delta. This shows that ... 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 >>>

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

Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga Ron-Zewi, Neil Thapen

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

Arnab Bhattacharyya, Elena Grigorescu, Jakob Nordström, Ning Xie

Properties of Boolean functions on the hypercube that are invariant

with respect to linear transformations of the domain are among some of

the most well-studied properties in the context of property testing.

In this paper, we study a particular natural class of linear-invariant

properties, called matroid freeness properties. These properties ...
more >>>

Eli Ben-Sasson, Jakob Nordström

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

Jakob Nordström

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

Jakob Nordström, Alexander Razborov

In the context of proving lower bounds on proof space in $k$-DNF

resolution, [Ben-Sasson and Nordström 2009] introduced the concept of

minimally unsatisfiable sets of $k$-DNF formulas and proved that a

minimally unsatisfiable $k$-DNF set with $m$ formulas can have at most

$O((mk)^{k+1})$ variables. They also gave an example of ...
more >>>

Eli Ben-Sasson, Jakob Nordström

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

Eli Ben-Sasson, Jakob Nordström

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

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

Jakob Nordström, Johan Håstad

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

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

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