Maria Luisa Bonet

J. Artif. Intell. Res., 2024

Redundancy for MaxSAT.

[BibT_eX]

[DOI]

Electron. Colloquium Comput. Complex., 2024

Polynomial calculus for optimization.

[BibT_eX]

[DOI]

Artif. Intell., 2024

MaxSAT Resolution with Inclusion Redundancy.

[BibT_eX]

[DOI]

Massimo Lauria

Proceedings of the 27th International Conference on Theory and Applications of Satisfiability Testing, 2024

Weighted, Circular and Semi-Algebraic Proofs (Abstract Reprint).

[BibT_eX]

[DOI]

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, 2024

2023

Polynomial Calculus for MaxSAT.

[BibT_eX]

[DOI]

Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing, 2023

On the Density of States of Boolean Formulas.

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence Research and Development, 2023

2022

Scale-Free Random SAT Instances.

[BibT_eX]

[DOI]

Algorithms, 2022

2021

On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems.

[BibT_eX]

[DOI]

Electron. Colloquium Comput. Complex., 2021

Propositional proof systems based on maximum satisfiability.

[BibT_eX]

[DOI]

Artif. Intell., 2021

2020

2-D Tucker is PPA complete.

[BibT_eX]

[DOI]

James Aisenberg

J. Comput. Syst. Sci., 2020

Equivalence Between Systems Stronger Than Resolution.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2020, 2020

2019

Community Structure in Industrial SAT Instances.

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 2019

DRMaxSAT with MaxHS: First Contact.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

Phase Transition in Realistic Random SAT Models.

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence Research and Development, 2019

2018

Short proofs of the Kneser-Lovász coloring principle.

[BibT_eX]

[DOI]

Inf. Comput., 2018

MaxSAT Resolution With the Dual Rail Encoding.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, 2018

2017

Structure features for SAT instances classification.

[BibT_eX]

[DOI]

J. Appl. Log., 2017

2016

Quasipolynomial Size Frege Proofs of Frankl's Theorem on the Trace of Sets.

[BibT_eX]

[DOI]

James Aisenberg

J. Symb. Log., 2016

Community Structure in Industrial SAT Instances.

[BibT_eX]

[DOI]

CoRR, 2016

2015

On the Classification of Industrial SAT Families.

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence Research and Development, 2015

2014

Improved Separations of Regular Resolution from Clause Learning Proof Systems.

[BibT_eX]

[DOI]

Jan Johannsen

J. Artif. Intell. Res., 2014

The Fractal Dimension of SAT Formulas.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

Resolution procedures for multiple-valued optimization.

[BibT_eX]

[DOI]

Inf. Sci., 2013

SAT-based MaxSAT algorithms.

[BibT_eX]

[DOI]

Artif. Intell., 2013

An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the IJCAI 2013, 2013

Improving WPM2 for (Weighted) Partial MaxSAT.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2013

2012

The Complexity of Finding Multiple Solutions to Betweenness and Quartet Compatibility.

[BibT_eX]

[DOI]

Simone Linz

Katherine St. John

IEEE ACM Trans. Comput. Biol. Bioinform., 2012

An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012

Improving SAT-Based Weighted MaxSAT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2012

Analysis and Generation of Pseudo-Industrial MaxSAT Instances.

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence Research and Development, 2012

2010

On the Complexity of uSPR Distance.

[BibT_eX]

[DOI]

Katherine St. John

IEEE ACM Trans. Comput. Biol. Bioinform., 2010

A New Algorithm for Weighted Partial MaxSAT.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, 2010

2009

Efficiently Calculating Evolutionary Tree Measures Using SAT.

[BibT_eX]

[DOI]

Katherine St. John

Proceedings of the Theory and Applications of Satisfiability Testing, 2009

Solving (Weighted) Partial MaxSAT through Satisfiability Testing.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2009

Towards Industrial-Like Random SAT Instances.

[BibT_eX]

[DOI]

Proceedings of the IJCAI 2009, 2009

On the Structure of Industrial SAT Instances.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2009

On Solving MaxSAT Through SAT.

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence Research and Development, 2009

2008

Random SAT Instances à la Carte.

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence Research and Development, 2008

Measuring the Hardness of SAT Instances.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, 2008

2007

Resolution for Max-SAT.

[BibT_eX]

[DOI]

Felip Manyà

Artif. Intell., 2007

Mapping CSP into Many-Valued SAT.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2007

A Complete Resolution Calculus for Signed Max-SAT.

[BibT_eX]

[DOI]

Proceedings of the 37th International Symposium on Multiple-Valued Logic, 2007

The Logic Behind Weighted CSP.

[BibT_eX]

[DOI]

Proceedings of the IJCAI 2007, 2007

What Is a Real-World SAT Instance?

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence Research and Development, 2007

Inference Rules for High-Order Consistency in Weighted CSP.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence, 2007

2006

Approximating Subtree Distances Between Phylogenies.

[BibT_eX]

[DOI]

J. Comput. Biol., 2006

A Complete Calculus for Max-SAT.

[BibT_eX]

[DOI]

Felip Manyà

Proceedings of the Theory and Applications of Satisfiability Testing, 2006

2004

Non-Automatizability of Bounded-Depth Frege Proofs.

[BibT_eX]

[DOI]

Comput. Complex., 2004

2003

On Chvatal Rank and Cutting Planes Proofs

[BibT_eX]

[DOI]

Electron. Colloquium Comput. Complex., 2003

Degree complexity for a modified pigeonhole principle.

[BibT_eX]

[DOI]

Arch. Math. Log., 2003

2002

Lower Bounds for the Weak Pigeonhole Principle and Random Formulas beyond Resolution.

[BibT_eX]

[DOI]

Juan Luis Esteban

Inf. Comput., 2002

On the Automatizability of Resolution and Related Propositional Proof Systems

[BibT_eX]

[DOI]

Electron. Colloquium Comput. Complex., 2002

2001

Optimality of size-width tradeoffs for resolution.

[BibT_eX]

[DOI]

Comput. Complex., 2001

Lower Bounds for the Weak Pigeonhole Principle Beyond Resolution.

[BibT_eX]

[DOI]

Juan Luis Esteban

Proceedings of the Automata, Languages and Programming, 28th International Colloquium, 2001

2000

On Interpolation and Automatization for Frege Systems.

[BibT_eX]

[DOI]

Toniann Pitassi

Ran Raz

SIAM J. Comput., 2000

On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems.

[BibT_eX]

[DOI]

SIAM J. Comput., 2000

1999

Constructing Evolutionary Trees in the Presence of Polymorphic Characters.

[BibT_eX]

[DOI]

SIAM J. Comput., 1999

A Study of Proof Search Algorithms for Resolution and Polynomial Calculus.

[BibT_eX]

[DOI]

Proceedings of the 40th Annual Symposium on Foundations of Computer Science, 1999

1998

Better Methods for Solving Parsimony and Compatibility.

[BibT_eX]

[DOI]

J. Comput. Biol., 1998

Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems

[BibT_eX]

[DOI]

Electron. Colloquium Comput. Complex., 1998

1997

Lower Bounds for Cutting Planes Proofs with Small Coefficients.

[BibT_eX]

[DOI]

Toniann Pitassi

Ran Raz

J. Symb. Log., 1997

No Feasible Interpolation for TC0-Frege Proofs.

[BibT_eX]

[DOI]

Toniann Pitassi

Ran Raz

Proceedings of the 38th Annual Symposium on Foundations of Computer Science, 1997

Linear Lower Bounds and Simulations in Frege Systems with Substitutions.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 11th International Workshop, 1997

1996

Inferring evolutionary trees from polymorphic characters, and an analysis of the Indo-European family of languages.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Hierarchies and Biology, 1996

1995

The Serial Transitive Closure Problem for Trees.

[BibT_eX]

[DOI]

SIAM J. Comput., 1995

1994

Size-Depth Tradeoffs for Boolean Fomulae.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1994

1993

The Deduction Rule and Linear and Near-Linear Proof Simulations.

[BibT_eX]

[DOI]

J. Symb. Log., 1993

1991

On the Deduction Rule and the Number of Proof Lines

[BibT_eX]

[DOI]