All reports by Author Albert Atserias:

__
TR14-118
| 9th September 2014
__

Albert Atserias, Massimo Lauria, Jakob Nordström#### Narrow Proofs May Be Maximally Long

__
TR13-149
| 28th October 2013
__

Albert Atserias, Neil Thapen#### The Ordering Principle in a Fragment of Approximate Counting

__
TR13-116
| 29th August 2013
__

Albert Atserias, Moritz Müller, Sergi Oliva#### Lower Bounds for DNF-Refutations of a Relativized Weak Pigeonhole Principle

__
TR12-096
| 17th July 2012
__

Albert Atserias, Sergi Oliva#### Bounded-width QBF is PSPACE-complete

Revisions: 3

__
TR12-015
| 22nd February 2012
__

Albert Atserias, Anuj Dawar#### Degree Lower Bounds of Tower-Type for Approximating Formulas with Parity Quantifiers

Revisions: 2

__
TR11-077
| 8th May 2011
__

Albert Atserias, Elitza Maneva#### Graph Isomorphism, Sherali-Adams Relaxations and Expressibility in Counting Logics

__
TR10-197
| 14th December 2010
__

Albert Atserias, Elitza Maneva#### Mean-payoff games and propositional proofs

__
TR05-154
| 11th December 2005
__

Albert Atserias#### Non-Uniform Hardness for NP via Black-Box Adversaries

__
TR03-041
| 29th May 2003
__

Albert Atserias, Maria Luisa Bonet, Jordi Levy#### On Chvatal Rank and Cutting Planes Proofs

__
TR02-035
| 27th May 2002
__

Albert Atserias, Víctor Dalmau#### A Combinatorial Characterization of Resolution Width

__
TR02-010
| 21st January 2002
__

Albert Atserias, Maria Luisa Bonet#### On the Automatizability of Resolution and Related Propositional Proof Systems

__
TR00-087
| 14th November 2000
__

Albert Atserias, Nicola Galesi, Pavel Pudlak#### Monotone simulations of nonmonotone propositional proofs

__
TR00-008
| 20th January 2000
__

Albert Atserias, Nicola Galesi, Ricard Gavaldà#### Monotone Proofs of the Pigeon Hole Principle

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

Albert Atserias, Neil Thapen

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 >>>

Albert Atserias, Moritz Müller, Sergi Oliva

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 >>>

Albert Atserias, Sergi Oliva

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 >>>

Albert Atserias, Anuj Dawar

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 >>>

Albert Atserias, Elitza Maneva

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 >>>

Albert Atserias, Elitza Maneva

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 >>>

Albert Atserias

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 >>>

Albert Atserias, Maria Luisa Bonet, Jordi Levy

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 >>>

Albert Atserias, Víctor Dalmau

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 >>>

Albert Atserias, Maria Luisa Bonet

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 >>>

Albert Atserias, Nicola Galesi, Pavel Pudlak

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 >>>Albert Atserias, Nicola Galesi, Ricard Gavaldà

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 >>>