Browsing by Author "Atserias, Albert"

A Note on polynomialsize monotone proofs of the pigeon hole principle
Atserias, Albert (200009)
External research report
Open AccessWe see that the version of the pigeonhole principle in which every hole is forced to receive a pigeon (called onto) and the version in which every pigeon is mapped into exactly one hole (called functional) have ... 
Automating Resolution is NPhard
Atserias, Albert; Muller, Moritz Martin (Institute of Electrical and Electronics Engineers (IEEE), 2019)
Conference report
Open AccessWe show that the problem of finding a Resolution refutation that is at most polynomially longer than a shortest one is NPhard. In the parlance of proof complexity, Resolution is not automatizable unless P = NP. Indeed, ... 
Boundedwidth QBF is PSPACEcomplete
Atserias, Albert; Oliva Valls, Sergi (Schloss Dagstuhl  LeibnizZentrum für Informatik, 2013)
Conference report
Open AccessTreewidth is a wellstudied parameter of structures that measures their similarity to a tree. Many important NPcomplete problems, such as Boolean satisﬁability (SAT), are tractable on bounded treewidth instances. In ... 
Boundedwidth QBF is PSPACEcomplete
Atserias, Albert; Oliva Valls, Sergi (20141101)
Article
Open AccessTreewidth and pathwidth are two wellstudied parameters of structures that measure their similarity to a tree and a path, respectively. We show that QBF on instances with constant pathwidth, and hence constant treewidth, ... 
CALCULABILITAT (Examen 2n quadrim)
Atserias, Albert (Universitat Politècnica de Catalunya, 20100531)
Exam
Restricted access to the UPC academic community 
Circular (yet sound) proofs
Atserias, Albert; Lauria, Massimo (Springer, 2019)
Conference report
Open AccessWe introduce a new way of composing proofs in rulebased proof systems that generalizes treelike and daglike proofs. In the new definition, proofs are directed graphs of derived formulas, in which cycles are allowed as ... 
Clique is hard on average for regular resolution
Atserias, Albert; Bonacina, Ilario; Rezende, Susanna F. de; Lauria, Massimo; Nordström, Jakob; Razborov, Alexander (Association for Computing Machinery (ACM), 2018)
Conference report
Open AccessWe prove that for k ≪4√n regular resolution requires length nΩ(k) to establish that an Erdős–Rényi graph with appropriately chosen edge density does not contain a kclique. This lower bound is optimal up to the multiplicative ... 
Definable ellipsoid method, sumsofsquares proofs, and the isomorphism problem
Atserias, Albert; Ochremiak, Joanna (Association for Computing Machinery (ACM), 2018)
Conference report
Open AccessThe ellipsoid method is an algorithm that solves the (weak) feasibility and linear optimization problems for convex sets by making oracle calls to their (weak) separation problem. We observe that the previously known method ... 
Definable inapproximability: new challenges for duplicator
Atserias, Albert; Dawar, Anuj (2019)
Article
Open AccessWe consider the hardness of approximation of optimization problems from the point of view of definability. For many NPhard optimization problems it is known that, unless P=NP, no polynomialtime algorithm can give an ... 
Definable inapproximability: New challenges for duplicator
Atserias, Albert; Dawar, Anuj (Schloss Dagstuhl  LeibnizZentrum für Informatik, 2018)
Conference report
Open AccessWe consider the hardness of approximation of optimization problems from the point of view of definability. For many NPhard optimization problems it is known that, unless P = NP, no polynomialtime algorithm can give an ... 
Degree lower bounds of towertype for approximating formulas with parity quantifiers
Atserias, Albert; Dawar, Anuj (20140201)
Article
Open AccessKolaitis and Kopparty have shown that for any firstorder formula with parity quantifiers over the language of graphs, there is a family of multivariate polynomials of constantdegree that agree with the formula on all but ... 
Entailment among probabilistic implications
Atserias, Albert; Balcázar Navarro, José Luis (Institute of Electrical and Electronics Engineers (IEEE), 2015)
Conference report
Open AccessWe study a natural variant of the implicational fragment of propositional logic. Its formulas are pairs of conjunctions of positive literals, related together by an implicationallike connective, the semantics of this sort ... 
From unplugged to physically realizable machines, and back
Atserias, Albert (20160330)
Audiovisual
Restricted access  author's decisionAround 1936, Alan Turing conceived his model of an automated computer. This was long before the transistor was even discovered. Thus, one would think that Turing's original model could nowadays be considered a piece of ... 
Generalized satisfiability problems via operator assignments
Atserias, Albert; Kolaitis, Phokion; Severini, Simone (201909)
Article
Open AccessSchaefer introduced a framework for generalized satisfiability problems on the Boolean domain and characterized the computational complexity of such problems. We investigate an algebraization of Schaefer's framework in ... 
Lower bounds for DNFrefutations of a relativized weak pigeonhole principle
Atserias, Albert; Müller, Moritz; Oliva Valls, Sergi (Institute of Electrical and Electronics Engineers (IEEE), 2013)
Conference report
Open AccessThe relativized weak pigeonhole principle states that if at least 2n out of n2 pigeons fly into n holes, then some hole must be doubly occupied. We prove that every DNFrefutation of the CNF encoding of this principle ... 
Lower bounds for DNFrefutations of a relativized weak pigeonhole principle
Atserias, Albert; Müller, Moritz; Oliva Valls, Sergi (20150601)
Article
Open AccessThe relativized weak pigeonhole principle states that if at least 2n out of n(2) pigeons fly into n holes, then some hole must be doubly occupied. We prove that every DNFrefutation of the CNF encoding of this principle ... 
Monotone proofs of the pigeon hole principle
Atserias, Albert; Galesi, Nicola; Gavaldà Mestre, Ricard (200004)
External research report
Open AccessWe study the complexity of proving the Pigeon Hole Principle (PHP) in a monotone variant of the Gentzen Calculus, also known as Geometric Logic. We show that the standard encoding of the PHP as a monotone sequent admits ... 
Narrow proofs may be maximally long
Atserias, Albert; Lauria, Massimo; Nordström, Jakob (20160703)
Article
Open AccessWe prove that there are 3CNF 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 counting argument that any formula refutable ... 
Narrow proofs may be maximally long
Atserias, Albert; Lauria, Massimo; Nordström, Jakob (Institute of Electrical and Electronics Engineers (IEEE), 2014)
Conference report
Open AccessWe prove that there are 3CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n¿(w). This shows that the simple counting argument that any formula refutable in ... 
Nonhomogenizable classes of finite structures
Atserias, Albert; Torunczyk, Szymon Abram (Schloss Dagstuhl  LeibnizZentrum für Informatik, 2016)
Conference report
Open AccessHomogenization is a powerful way of taming a class of finite structures with several interesting applications in different areas, from Ramsey theory in combinatorics to constraint satisfaction problems (CSPs) in computer ...