6 papers
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…
A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds
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…
Tight Size-Degree Bounds for Sums-of-Squares Proofs
Massimo Lauria, Jakob Nordström
We exhibit families of -CNF formulas over variables that have sums-of-squares (SOS) proofs of unsatisfiability of degree (a.k.a. rank) but require SOS proofs of size $n^…
Towards an Optimal Separation of Space and Length in Resolution
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 obv…