Albert Atserias

Noel Arteche, Albert Atserias, Susanna F. de Rezende et al.

Atserias and Müller (JACM, 2020) proved that for every unsatisfiable CNF formula $φ$, the formula $\operatorname{Ref}(φ)$, stating "$φ$ has small Resolution refutations", does not have subexponential-size Resolution refutations. Conversely, when $φ$ is satisfiable, Pudlák (TCS, 2003) showed how to construct a polynomial-size Resolution refutation of $\operatorname{Ref}(φ)$ given a satisfying assignment of $φ$. A question that remained open is: do all short Resolution refutations of $\operatorname{Ref}(φ)$ explicitly leak a satisfying assignment of $φ$? We answer this question affirmatively by giving a polynomial-time algorithm that extracts a satisfying assignment for $φ$ given any short Resolution refutation of $\operatorname{Ref}(φ)$. The algorithm follows from a new feasibly constructive proof of the Atserias-Müller lower bound, formalizable in Cook's theory $\mathsf{PV_1}$ of bounded arithmetic. Motivated by this, we introduce a computational problem concerning Resolution lower bounds: the Proof Analysis Problem (PAP). For a proof system $Q$, the Proof Analysis Problem for $Q$ asks, given a CNF formula $φ$ and a $Q$-proof of a Resolution lower bound for $φ$, encoded as $\neg \operatorname{Ref}(φ)$, whether $φ$ is satisfiable. In contrast to PAP for Resolution, we prove that PAP for Extended Frege (EF) is NP-complete. Our results yield new insights into proof complexity: (i) every proof system simulating EF is (weakly) automatable if and only if it is (weakly) automatable on formulas stating Resolution lower bounds; (ii) we provide Ref formulas exponentially hard for bounded-depth Frege systems; and (iii) for every strong enough theory of arithmetic $T$ we construct unsatisfiable CNF formulas exponentially hard for Resolution but for which $T$ cannot prove even a quadratic lower bound.

Albert Atserias, Moritz Müller

We prove that the bounded arithmetic theory $S^1_2$ is consistent with EXP $\not\subseteq$ P/poly. More generally, we show that certain separations of $V^1_2$ from a theory $T$ imply the consistency of $T$ with EXP $\not\subseteq$ P/poly. For $T=S^1_2$, Takeuti (1988) established such a separation using a variant of Gödel's consistency statement. Analogous results hold for PSPACE $\not\subseteq$ P/poly but the required separations of theories are yet unknown. Finally, we give magnification results for the hardness of proving almost-everywhere versions of these lower bounds.

Albert Atserias, José L. Balcázar, Marie Ely Piceno

We study a natural variant of the implicational fragment of propositional logic. Its formulas are pairs of conjunctions of positive literals, related together by an implicational-like connective; the semantics of this sort of implication is defined in terms of a threshold on a conditional probability of the consequent, given the antecedent: we are dealing with what the data analysis community calls confidence of partial implications or association rules. Existing studies of redundancy among these partial implications have characterized so far only entailment from one premise and entailment from two premises, both in the stand-alone case and in the case of presence of additional classical implications (this is what we call "relative entailment"). By exploiting a previously noted alternative view of the entailment in terms of linear programming duality, we characterize exactly the cases of entailment from arbitrary numbers of premises, again both in the stand-alone case and in the case of presence of additional classical implications. As a result, we obtain decision algorithms of better complexity; additionally, for each potential case of entailment, we identify a critical confidence threshold and show that it is, actually, intrinsic to each set of premises and antecedent of the conclusion.

Albert Atserias, Johannes Klaus Fichte, Marc Thurley

We offer a new understanding of some aspects of practical SAT-solvers that are based on DPLL with unit-clause propagation, clause-learning, and restarts. We do so by analyzing a concrete algorithm which we claim is faithful to what practical solvers do. In particular, before making any new decision or restart, the solver repeatedly applies the unit-resolution rule until saturation, and leaves no component to the mercy of non-determinism except for some internal randomness. We prove the perhaps surprising fact that, although the solver is not explicitly designed for it, with high probability it ends up behaving as width-k resolution after no more than O(n^2k+2) conflicts and restarts, where n is the number of variables. In other words, width-k resolution can be thought of as O(n^2k+2) restarts of the unit-resolution rule with learning.