On the Deduction Rule and the Number of Proof Lines - Maria Luisa Bonet; Samuel R. Buss (LICS, 1991)

The Deduction Rule and Linear and Near-Linear Proof Simulations. - Maria Luisa Bonet; Samuel R. Buss (J. Symb. Log., 1993)

Size-Depth Tradeoffs for Boolean Fomulae. - Maria Luisa Bonet; Samuel R. Buss (Inf. Process. Lett., 1994)

The Serial Transitive Closure Problem for Trees. - Maria Luisa Bonet; Samuel R. Buss (SIAM J. Comput., 1995)

Inferring evolutionary trees from polymorphic characters, and an analysis of the Indo-European family of languages. - Maria Luisa Bonet; Cynthia A. Phillips; Tandy J. Warnow; Shibu Yooseph (Mathematical Hierarchies and Biology, 1996)

Linear Lower Bounds and Simulations in Frege Systems with Substitutions. - Maria Luisa Bonet; Nicola Galesi (CSL, 1997)

No Feasible Interpolation for TC0-Frege Proofs. - Maria Luisa Bonet; Toniann Pitassi; Ran Raz (FOCS, 1997)

Lower Bounds for Cutting Planes Proofs with Small Coefficients. - Maria Luisa Bonet; Toniann Pitassi; Ran Raz (J. Symb. Log., 1997)

Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems - Maria Luisa Bonet; Juan Luis Esteban; Nicola Galesi; Jan Johannsen (Electron. Colloquium Comput. Complex., 1998)

Better Methods for Solving Parsimony and Compatibility. - Maria Luisa Bonet; Mike A. Steel; Tandy J. Warnow; Shibu Yooseph (J. Comput. Biol., 1998)

A Study of Proof Search Algorithms for Resolution and Polynomial Calculus. - Maria Luisa Bonet; Nicola Galesi (FOCS, 1999)

Constructing Evolutionary Trees in the Presence of Polymorphic Characters. - Maria Luisa Bonet; Cynthia A. Phillips; Tandy J. Warnow; Shibu Yooseph (SIAM J. Comput., 1999)

On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems. - Maria Luisa Bonet; Juan Luis Esteban; Nicola Galesi; Jan Johannsen (SIAM J. Comput., 2000)

On Interpolation and Automatization for Frege Systems. - Maria Luisa Bonet; Toniann Pitassi; Ran Raz (SIAM J. Comput., 2000)

Lower Bounds for the Weak Pigeonhole Principle Beyond Resolution. - Albert Atserias; Maria Luisa Bonet; Juan Luis Esteban (ICALP, 2001)

Optimality of size-width tradeoffs for resolution. - Maria Luisa Bonet; Nicola Galesi (Comput. Complex., 2001)

On the Automatizability of Resolution and Related Propositional Proof Systems - Albert Atserias; Maria Luisa Bonet (Electron. Colloquium Comput. Complex., 2002)

Lower Bounds for the Weak Pigeonhole Principle and Random Formulas beyond Resolution. - Albert Atserias; Maria Luisa Bonet; Juan Luis Esteban (Inf. Comput., 2002)

Degree complexity for a modified pigeonhole principle. - Maria Luisa Bonet; Nicola Galesi (Arch. Math. Log., 2003)

On Chvatal Rank and Cutting Planes Proofs - Albert Atserias; Maria Luisa Bonet; Jordi Levy (Electron. Colloquium Comput. Complex., 2003)

Non-Automatizability of Bounded-Depth Frege Proofs. - Maria Luisa Bonet; Carlos Domingo; Ricard Gavaldà; Alexis Maciel; Toniann Pitassi (Comput. Complex., 2004)

A Complete Calculus for Max-SAT. - Maria Luisa Bonet; Jordi Levy; Felip Manyà (SAT, 2006)

Approximating Subtree Distances Between Phylogenies. - Maria Luisa Bonet; Katherine St. John; Ruchi Mahindru; Nina Amenta (J. Comput. Biol., 2006)

Inference Rules for High-Order Consistency in Weighted CSP. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy; Felip Manyà (AAAI, 2007)

What Is a Real-World SAT Instance? - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy; Felip Manyà (CCIA, 2007)

The Logic Behind Weighted CSP. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy; Felip Manyà (IJCAI, 2007)

A Complete Resolution Calculus for Signed Max-SAT. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy; Felip Manyà (ISMVL, 2007)

Mapping CSP into Many-Valued SAT. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy; Felip Manyà (SAT, 2007)

Resolution for Max-SAT. - Maria Luisa Bonet; Jordi Levy; Felip Manyà (Artif. Intell., 2007)

Measuring the Hardness of SAT Instances. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy; Felip Manyà (AAAI, 2008)

Random SAT Instances à la Carte. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (CCIA, 2008)

On Solving MaxSAT Through SAT. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (CCIA, 2009)

On the Structure of Industrial SAT Instances. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (CP, 2009)

Towards Industrial-Like Random SAT Instances. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (IJCAI, 2009)

Solving (Weighted) Partial MaxSAT through Satisfiability Testing. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (SAT, 2009)

Efficiently Calculating Evolutionary Tree Measures Using SAT. - Maria Luisa Bonet; Katherine St. John (SAT, 2009)

A New Algorithm for Weighted Partial MaxSAT. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (AAAI, 2010)

On the Complexity of uSPR Distance. - Maria Luisa Bonet; Katherine St. John (IEEE ACM Trans. Comput. Biol. Bioinform., 2010)

Analysis and Generation of Pseudo-Industrial MaxSAT Instances. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy; Chu Min Li 001 (CCIA, 2012)

Improving SAT-Based Weighted MaxSAT Solvers. - Carlos Ansótegui; Maria Luisa Bonet; Joel Gabàs; Jordi Levy (CP, 2012)

An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning. - Maria Luisa Bonet; Samuel R. Buss (SAT, 2012)

The Complexity of Finding Multiple Solutions to Betweenness and Quartet Compatibility. - Maria Luisa Bonet; Simone Linz; Katherine St. John (IEEE ACM Trans. Comput. Biol. Bioinform., 2012)

Improving WPM2 for (Weighted) Partial MaxSAT. - Carlos Ansótegui; Maria Luisa Bonet; Joel Gabàs; Jordi Levy (CP, 2013)

An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning (Extended Abstract). - Maria Luisa Bonet; Sam Buss (IJCAI, 2013)

SAT-based MaxSAT algorithms. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (Artif. Intell., 2013)

Resolution procedures for multiple-valued optimization. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy; Felip Manyà (Inf. Sci., 2013)

The Fractal Dimension of SAT Formulas. - Carlos Ansótegui; Maria Luisa Bonet; Jesús Giráldez-Cru; Jordi Levy (IJCAR, 2014)

Improved Separations of Regular Resolution from Clause Learning Proof Systems. - Maria Luisa Bonet; Sam Buss; Jan Johannsen (J. Artif. Intell. Res., 2014)

On the Classification of Industrial SAT Families. - Carlos Ansótegui; Maria Luisa Bonet; Jesús Giráldez-Cru; Jordi Levy (CCIA, 2015)

Community Structure in Industrial SAT Instances. - Carlos Ansótegui; Maria Luisa Bonet; Jesús Giráldez-Cru; Jordi Levy (CoRR, 2016)

Quasipolynomial Size Frege Proofs of Frankl's Theorem on the Trace of Sets. - James Aisenberg; Maria Luisa Bonet; Sam Buss (J. Symb. Log., 2016)

Structure features for SAT instances classification. - Carlos Ansótegui; Maria Luisa Bonet; Jesús Giráldez-Cru; Jordi Levy (J. Appl. Log., 2017)

MaxSAT Resolution With the Dual Rail Encoding. - Maria Luisa Bonet; Sam Buss; Alexey Ignatiev; João Marques-Silva 001; António Morgado 001 (AAAI, 2018)

Short proofs of the Kneser-Lovász coloring principle. - James Aisenberg; Maria Luisa Bonet; Sam Buss; Adrian Craciun; Gabriel Istrate (Inf. Comput., 2018)

Phase Transition in Realistic Random SAT Models. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (CCIA, 2019)

DRMaxSAT with MaxHS: First Contact. - António Morgado 001; Alexey Ignatiev; Maria Luisa Bonet; João Marques-Silva 001; Sam Buss (SAT, 2019)

Community Structure in Industrial SAT Instances. - Carlos Ansótegui; Maria Luisa Bonet; Jesús Giráldez-Cru; Jordi Levy; Laurent Simon 001 (J. Artif. Intell. Res., 2019)

Equivalence Between Systems Stronger Than Resolution. - Maria Luisa Bonet; Jordi Levy (SAT, 2020)

2-D Tucker is PPA complete. - James Aisenberg; Maria Luisa Bonet; Sam Buss (J. Comput. Syst. Sci., 2020)

Propositional proof systems based on maximum satisfiability. - Maria Luisa Bonet; Sam Buss; Alexey Ignatiev; António Morgado 001; João Marques-Silva 001 (Artif. Intell., 2021)

On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems. - Ilario Bonacina; Maria Luisa Bonet (Electron. Colloquium Comput. Complex., 2021)

Scale-Free Random SAT Instances. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (Algorithms, 2022)

On the Density of States of Boolean Formulas. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (CCIA, 2023)

Polynomial Calculus for MaxSAT. - Ilario Bonacina; Maria Luisa Bonet; Jordi Levy (SAT, 2023)

Weighted, Circular and Semi-Algebraic Proofs (Abstract Reprint). - Ilario Bonacina; Maria Luisa Bonet; Jordi Levy (IJCAI, 2024)

MaxSAT Resolution with Inclusion Redundancy. - Ilario Bonacina; Maria Luisa Bonet; Massimo Lauria (SAT, 2024)

Polynomial calculus for optimization. - Ilario Bonacina; Maria Luisa Bonet; Jordi Levy (Artif. Intell., 2024)

Redundancy for MaxSAT. - Ilario Bonacina; Maria Luisa Bonet; Sam Buss; Massimo Lauria (Electron. Colloquium Comput. Complex., 2024)

Weighted, Circular and Semi-Algebraic Proofs. - Ilario Bonacina; Maria Luisa Bonet; Jordi Levy (J. Artif. Intell. Res., 2024)

Redundancy Rules for MaxSAT. - Ilario Bonacina; Maria Luisa Bonet; Sam Buss; Massimo Lauria (SAT, 2025)

Strength and limitations of Sherali-Adams and Nullstellensatz proof systems. - Ilario Bonacina; Maria Luisa Bonet (Ann. Pure Appl. Log., 2025)