79 citations · 93 across the 20 of their papers we have counts for
12 papers · 1 filter
Hard Clique Formulas for Resolution
Albert Atserias
We show how to convert any unsatisfiable 3-CNF formula which is sparse and exponentially hard to refute in Resolution into a negative instance of the -clique problem whose corre…
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…
Simple general magnification of circuit lower bounds
Albert Atserias, Moritz Müller
We introduce a technically and conceptually simple approach to magnification of circuit and formula lower bounds. Central to the method are so-called distinguishers, sparse matrice…
Feasibly Constructive Proof of Schwartz-Zippel Lemma and the Complexity of Finding Hitting Sets
Albert Atserias, Iddo Tzameret
The Schwartz-Zippel Lemma states that if a low-degree multivariate polynomial with coefficients in a field is not zero everywhere in the field, then it has few roots on every finit…
On the Consistency of Circuit Lower Bounds for Non-Deterministic Time
Albert Atserias, Sam Buss, Moritz Müller
We prove the first unconditional consistency result for superpolynomial circuit lower bounds with a relatively strong theory of bounded arithmetic. Namely, we show that the theory…
Promise Constraint Satisfaction and Width
Albert Atserias, Víctor Dalmau
We study the power of the bounded-width consistency algorithm in the context of the fixed-template Promise Constraint Satisfaction Problem (PCSP). Our main technical finding is tha…
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…
Automating Resolution is NP-Hard
Albert Atserias, Moritz Müller
We show that the problem of finding a Resolution refutation that is at most polynomially longer than a shortest one is NP-hard. In the parlance of proof complexity, Resolution is n…
Size-Degree Trade-Offs for Sums-of-Squares and Positivstellensatz Proofs
Albert Atserias, Tuomas Hakoniemi
We show that if a system of degree- polynomial constraints on~ Boolean variables has a Sums-of-Squares (SOS) proof of unsatisfiability with at most~ many monomials, then i…
Proof Complexity Meets Algebra
Albert Atserias, Joanna Ochremiak
We analyse how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional, algebraic, and semi…
A Note on Semi-Algebraic Proofs and Gaussian Elimination over Prime Fields
Albert Atserias
In this note we show that unsatisfiable systems of linear equations with a constant number of variables per equation over prime finite fields have polynomial-size constant-degree s…
Narrow Proofs May Be Maximally Long
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 co…