4 papers · 1 filter
The Proof Analysis Problem
Noel Arteche, Albert Atserias, Susanna F. de Rezende +1
Atserias and Müller (JACM, 2020) proved that for every unsatisfiable CNF formula , the formula , stating " has small Resolution refutations", does not…
Clique Is Hard on Average for Regular Resolution
Albert Atserias, Ilario Bonacina, Susanna F. de Rezende +3
We prove that for regular resolution requires length to establish that an Erdős-Rényi graph with appropriately chosen edge density does not contain a…
Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling
Susanna F. de Rezende, Or Meir, Jakob Nordström +1
We establish an exactly tight relation between reversible pebblings of graphs and Nullstellensatz refutations of pebbling formulas, showing that a graph can be reversibly pebbl…
Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity
Susanna F. de Rezende, Or Meir, Jakob Nordström +3
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 wit…