All reports by Author Susanna de Rezende:

__
TR21-033
| 7th March 2021
__

Susanna de Rezende#### Automating Tree-Like Resolution in Time $n^{o(\log n)}$ Is ETH-Hard

__
TR21-006
| 18th January 2021
__

Susanna de Rezende, Jakob Nordström, Marc Vinyals#### How Limited Interaction Hinders Real Communication (and What It Means for Proof and Circuit Complexity)

__
TR20-099
| 6th July 2020
__

Susanna de Rezende, Or Meir, Jakob Nordström, Toniann Pitassi, Robert Robere#### KRW Composition Theorems via Lifting

Revisions: 1

__
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: 2

__
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

Susanna de Rezende

We show that tree-like resolution is not automatable in time $n^{o(\log n)}$ unless ETH is false. This implies that, under ETH, the algorithm given by Beame and Pitassi (FOCS 1996) that automates tree-like resolution in time $n^{O(\log n)}$ is optimal. We also provide a simpler proof of the result of ... more >>>

Susanna de Rezende, Jakob Nordström, Marc Vinyals

We obtain the first true size-space trade-offs for the cutting planes proof system, where the upper bounds hold for size and total space for derivations with constant-size coefficients, and the lower bounds apply to length and formula space (i.e., number of inequalities in memory) even for derivations with exponentially large ... more >>>

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

One of the major open problems in complexity theory is proving super-logarithmic lower bounds on the depth of circuits (i.e., $\mathbf{P}\not\subseteq\mathbf{NC}^1$). Karchmer, Raz, and Wigderson (Computational Complexity 5(3/4), 1995) suggested to approach this problem by proving that depth complexity behaves “as expected” with respect to the composition of functions $f ... more >>>

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