Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

All reports by Author Albert Atserias:

TR14-118 | 9th September 2014
Albert Atserias, Massimo Lauria, Jakob Nordström

Narrow Proofs May Be Maximally Long

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 counting argument that any formula refutable in width w must have a proof in size n^O(w) is essentially tight. ... more >>>

TR13-149 | 28th October 2013
Albert Atserias, Neil Thapen

The Ordering Principle in a Fragment of Approximate Counting

The ordering principle states that every finite linear order has a least element. We show that, in the relativized setting, the surjective weak pigeonhole principle for polynomial time functions does not prove a Herbrandized version of the ordering principle over $\mathrm{T}^1_2$. This answers an open question raised in [Buss, Ko{\l}odziejczyk ... more >>>

TR13-116 | 29th August 2013
Albert Atserias, Moritz Müller, Sergi Oliva

Lower Bounds for DNF-Refutations of a Relativized Weak Pigeonhole Principle

The 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 DNF-refutation of the CNF encoding of this principle requires size $2^{(\log n)^{3/2-\epsilon}}$ for every $\epsilon > 0$ and every sufficiently ... more >>>

TR12-096 | 17th July 2012
Albert Atserias, Sergi Oliva

Bounded-width QBF is PSPACE-complete

Revisions: 3

Tree-width is a well-studied parameter of structures that measures their similarity to a tree. Many important NP-complete problems, such as Boolean satisfiability (SAT), are tractable on bounded tree-width instances. In this paper we focus on the canonical PSPACE-complete problem QBF, the fully-quantified version of SAT. It was shown by Pan ... more >>>

TR12-015 | 22nd February 2012
Albert Atserias, Anuj Dawar

Degree Lower Bounds of Tower-Type for Approximating Formulas with Parity Quantifiers

Revisions: 2

Kolaitis and Kopparty have shown that for any first-order formula with
parity quantifiers over the language of graphs there is a family of
multi-variate polynomials of constant-degree that agree with the
formula on all but a $2^{-\Omega(n)}$-fraction of the graphs with $n$
vertices. The proof yields a bound on the ... more >>>

TR11-077 | 8th May 2011
Albert Atserias, Elitza Maneva

Graph Isomorphism, Sherali-Adams Relaxations and Expressibility in Counting Logics

Two graphs with adjacency matrices $\mathbf{A}$ and $\mathbf{B}$ are isomorphic if there exists a permutation matrix $\mathbf{P}$ for which the identity $\mathbf{P}^{\mathrm{T}} \mathbf{A} \mathbf{P} = \mathbf{B}$ holds. Multiplying through by $\mathbf{P}$ and relaxing the permutation matrix to a doubly stochastic matrix leads to the notion of fractional isomorphism. We show ... more >>>

TR10-197 | 14th December 2010
Albert Atserias, Elitza Maneva

Mean-payoff games and propositional proofs

We associate a CNF-formula to every instance of the mean-payoff game problem in such a way that if the value of the game is non-negative the formula is satisfiable, and if the value of the game is negative the formula has a polynomial-size refutation in $\Sigma_2$-Frege (i.e.~DNF-resolution). This reduces mean-payoff ... more >>>

TR05-154 | 11th December 2005
Albert Atserias

Non-Uniform Hardness for NP via Black-Box Adversaries

We may believe SAT does not have small Boolean circuits.
But is it possible that some language with small circuits
looks indistiguishable from SAT to every polynomial-time
bounded adversary? We rule out this possibility. More
precisely, assuming SAT does not have small circuits, we
show that ... more >>>

TR03-041 | 29th May 2003
Albert Atserias, Maria Luisa Bonet, Jordi Levy

On Chvatal Rank and Cutting Planes Proofs

We study the Chv\'atal rank of polytopes as a complexity measure of
unsatisfiable sets of clauses. Our first result establishes a
connection between the Chv\'atal rank and the minimum refutation
length in the cutting planes proof system. The result implies that
length lower bounds for cutting planes, or even for ... more >>>

TR02-035 | 27th May 2002
Albert Atserias, Víctor Dalmau

A Combinatorial Characterization of Resolution Width

We provide a characterization of the resolution
width introduced in the context of Propositional Proof Complexity
in terms of the existential pebble game introduced
in the context of Finite Model Theory. The characterization
is tight and purely combinatorial. Our
first application of this result is a surprising
proof that the ... more >>>

TR02-010 | 21st January 2002
Albert Atserias, Maria Luisa Bonet

On the Automatizability of Resolution and Related Propositional Proof Systems

Having good algorithms to verify tautologies as efficiently as possible
is of prime interest in different fields of computer science.
In this paper we present an algorithm for finding Resolution refutations
based on finding tree-like Res(k) refutations. The algorithm is based on
the one of Beame and Pitassi \cite{BP96} ... more >>>

TR00-087 | 14th November 2000
Albert Atserias, Nicola Galesi, Pavel Pudlak

Monotone simulations of nonmonotone propositional proofs

We show that an LK proof of size $m$ of a monotone sequent (a sequent

that contains only formulas in the basis $\wedge,\vee$) can be turned

into a proof containing only monotone formulas of size $m^{O(\log m)}$

and with the number of proof lines polynomial in $m$. Also we show

... more >>>

TR00-008 | 20th January 2000
Albert Atserias, Nicola Galesi, Ricard Gavaldà

Monotone Proofs of the Pigeon Hole Principle

We 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 quasipolynomial-size proofs
in this system. This result is a consequence of ... more >>>

ISSN 1433-8092 | Imprint