activity
20242026
collaborators

6 papers

cs.CC2026

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…

math.LO2026

From Gödel incompleteness to the consistency of circuit lower bounds

Albert Atserias, Moritz Müller

We prove that the bounded arithmetic theory is consistent with EXP P/poly. More generally, we show that certain separations of from a theory imp…

cs.CC2026

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…

cs.DB2025

Gamma Acyclicity, Annotated Relations, and Consistency Witness Functions

Albert Atserias, Phokion G. Kolaitis

During the early days of relational database theory it was realized that "acyclic" database schemas possess a number of desirable semantic properties. In fact, three different noti…

cs.CC2025

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…

cs.CC2024

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…