All reports by Author Maria Luisa Bonet:

__
TR24-045
| 6th March 2024
__

Ilario Bonacina, Maria Luisa Bonet, Sam Buss, Massimo Lauria#### Redundancy for MaxSAT

__
TR21-182
| 30th December 2021
__

Ilario Bonacina, Maria Luisa Bonet#### On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems

__
TR15-163
| 11th October 2015
__

James Aisenberg, Maria Luisa Bonet, Sam Buss#### 2-D Tucker is PPA complete

__
TR03-041
| 29th May 2003
__

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

__
TR02-010
| 21st January 2002
__

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

__
TR98-035
| 8th May 1998
__

Maria Luisa Bonet, Juan Luis Esteban, Jan Johannsen#### Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems

Ilario Bonacina, Maria Luisa Bonet, Sam Buss, Massimo Lauria

The concept of redundancy in SAT lead to more expressive and powerful proof search techniques, e.g. able to express various inprocessing techniques, and to interesting hierarchies of proof systems [Heule et.alâ€™20, Buss-Thapenâ€™19].

We propose a general way to integrate redundancy rules in MaxSAT, that is we define MaxSAT variants of ...
more >>>

Ilario Bonacina, Maria Luisa Bonet

The propositional proof system Sherali-Adams (SA) has polynomial-size proofs of the pigeonhole principle (PHP). Similarly, the Nullstellensatz (NS) proof system has polynomial size proofs of the bijective (i.e. both functional and onto) pigeonhole principle (ofPHP). We characterize the strength of these algebraic proof systems in terms of Boolean proof systems ... more >>>

James Aisenberg, Maria Luisa Bonet, Sam Buss

The 2-D Tucker search problem is shown to be PPA-hard under many-one reductions; therefore it is complete for PPA. The same holds for $k$-D Tucker for all $k\ge 2$. This corrects a claim in the literature that the Tucker search problem is in PPAD.

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

Maria Luisa Bonet, Juan Luis Esteban, Jan Johannsen

We prove an exponential lower bound for tree-like Cutting Planes

refutations of a set of clauses which has polynomial size resolution

refutations. This implies an exponential separation between tree-like

and dag-like proofs for both Cutting Planes and resolution; in both

cases only superpolynomial separations were known before.

In order to ...
more >>>