Paramodulation with Non-Monotonic Orderings. - Miquel Bofill; Guillem Godoy; Robert Nieuwenhuis; Albert Rubio (LICS, 1999)

Modular Redundancy for Theorem Proving. - Miquel Bofill; Guillem Godoy; Robert Nieuwenhuis; Albert Rubio (FroCoS, 2000)

On the Completeness of Arbitrary Selection Strategies for Paramodulation. - Miquel Bofill; Guillem Godoy (ICALP, 2001)

Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation. - Miquel Bofill; Albert Rubio (CADE, 2002)

Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings. - Miquel Bofill; Guillem Godoy; Robert Nieuwenhuis; Albert Rubio (J. Autom. Reason., 2003)

Redundancy Notions for Paramodulation with Non-monotonic Orderings. - Miquel Bofill; Albert Rubio (IJCAR, 2004)

The Barcelogic SMT Solver. - Miquel Bofill; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (CAV, 2008)

A Write-Based Solver for SAT Modulo the Theory of Arrays. - Miquel Bofill; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (FMCAD, 2008)

Auction Robustness through Satisability Modulo Theories. - Miquel Bofill; Dídac Busquets; Mateu Villaret (WAT, 2009)

Paramodulation with Well-founded Orderings. - Miquel Bofill; Albert Rubio (J. Log. Comput., 2009)

A declarative approach to robust weighted Max-SAT. - Miquel Bofill; Dídac Busquets; Mateu Villaret (PPDP, 2010)

A System for Solving Constraint Satisfaction Problems with SMT. - Miquel Bofill; Josep Suy; Mateu Villaret (SAT, 2010)

Extending Multiple-Valued Clausal Forms with Linear Integer Arithmetic. - Carlos Ansótegui; Miquel Bofill; Felip Manyà; Mateu Villaret (ISMVL, 2011)

Satisfiability Modulo Theories: An Efficient Approach for the Resource-Constrained Project Scheduling Problem. - Carlos Ansótegui; Miquel Bofill; Miquel Palahí; Josep Suy; Mateu Villaret (SARA, 2011)

Building Automated Theorem Provers for Infinitely-Valued Logics with Satisfiability Modulo Theory Solvers. - Carlos Ansótegui; Miquel Bofill; Felip Manyà; Mateu Villaret (ISMVL, 2012)

Solving constraint satisfaction problems with SAT modulo theories. - Miquel Bofill; Miquel Palahí; Josep Suy; Mateu Villaret (Constraints An Int. J., 2012)

Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories. - Carlos Ansótegui; Miquel Bofill; Miquel Palahí; Josep Suy; Mateu Villaret (Constraints An Int. J., 2013)

Reformulation based MaxSAT robustness. - Miquel Bofill; Dídac Busquets; Víctor Muñoz; Mateu Villaret (Constraints An Int. J., 2013)

Paramodulation with Non-Monotonic Orderings and Simplification. - Miquel Bofill; Albert Rubio (J. Autom. Reason., 2013)

The recursive path and polynomial ordering for first-order and higher-order terms. - Miquel Bofill; Cristina Borralleras; Enric Rodríguez-Carbonell; Albert Rubio (J. Log. Comput., 2013)

A System for Generation and Visualization of Resource-Constrained Projects. - Miquel Bofill; Jordi Coll; Josep Suy; Mateu Villaret (CCIA, 2014)

Reformulation Based MaxSAT Robustness - (Extended Abstract). - Miquel Bofill; Dídac Busquets; Mateu Villaret (CP, 2014)

Scheduling B2B Meetings. - Miquel Bofill; Joan Espasa; Marc Garcia; Miquel Palahí; Josep Suy; Mateu Villaret (CP, 2014)

Solving Intensional Weighted CSPs by Incremental Optimization with BDDs. - Miquel Bofill; Miquel Palahí; Josep Suy; Mateu Villaret (CP, 2014)

MaxSAT-Based Scheduling of B2B Meetings. - Miquel Bofill; Marc Garcia; Josep Suy; Mateu Villaret (CPAIOR, 2015)

Finding Hard Instances of Satisfiability in Lukasiewicz Logics. - Miquel Bofill; Felip Manyà; Amanda Vidal; Mateu Villaret (ISMVL, 2015)

The Complexity of 3-Valued Łukasiewicz Rules. - Miquel Bofill; Felip Manyà; Amanda Vidal; Mateu Villaret (MDAI, 2015)

Fuzzy XPath for the Automatic Search of Fuzzy Formulae Models. - Jesús Manuel Almendros-Jiménez; Miquel Bofill; Alejandro Luna Tedesqui; Ginés Moreno; Carlos Vázquez; Mateu Villaret (SUM, 2015)

SAT and SMT Technology for Many-Valued Logics. - Carlos Ansótegui; Miquel Bofill; Felip Manyà; Mateu Villaret (J. Multiple Valued Log. Soft Comput., 2015)

A Semantic Notion of Interference for Planning Modulo Theories. - Miquel Bofill; Joan Espasa; Mateu Villaret (ICAPS, 2016)

Solving the Multi-Mode Resource-Constrained Project Scheduling Problem with SMT. - Miquel Bofill; Jordi Coll; Josep Suy; Mateu Villaret (ICTAI, 2016)

Solving the Wastewater Treatment Plant Problem with SMT. - Miquel Bofill; Víctor Muñoz; Javier Murillo (CoRR, 2016)

Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers. - Carlos Ansótegui; Miquel Bofill; Felip Manyà; Mateu Villaret (Fuzzy Sets Syst., 2016)

The RANTANPLAN planner: system description. - Miquel Bofill; Joan Espasa; Mateu Villaret (Knowl. Eng. Rev., 2016)

The Spanish Kidney Exchange Model: Study of Computation-Based Alternatives to the Current Procedure. - Miquel Bofill; Marcos Calderón; Francesc Castro; Esteve del Acebo; Pablo Delgado; Marc Garcia; Marta García; Marc Roig; María O. Valentín; Mateu Villaret (AIME, 2017)

An Efficient SMT Approach to Solve MRCPSP/max Instances with Tight Constraints on Resources. - Miquel Bofill; Jordi Coll; Josep Suy; Mateu Villaret (CP, 2017)

Compact MDDs for Pseudo-Boolean Constraints with At-Most-One Relations in Resource-Constrained Scheduling Problems. - Miquel Bofill; Jordi Coll; Josep Suy; Mateu Villaret (IJCAI, 2017)

Relaxed Exists-Step Plans in Planning as SMT. - Miquel Bofill; Joan Espasa; Mateu Villaret (IJCAI, 2017)

A Study on Implied Constraints in a MaxSAT Approach to B2B Problems. - Miquel Bofill; Jesús Giráldez-Cru; Josep Suy; Mateu Villaret (CCIA, 2019)

Automatic Detection of At-Most-One and Exactly-One Relations for Improved SAT Encodings of Pseudo-Boolean Constraints. - Carlos Ansótegui; Miquel Bofill; Jordi Coll; Nguyen Dang 001; Juan Luis Esteban; Ian Miguel; Peter Nightingale; András Z. Salamon; Josep Suy; Mateu Villaret (CP, 2019)

SAT Encodings of Pseudo-Boolean Constraints with At-Most-One Relations. - Miquel Bofill; Jordi Coll; Josep Suy; Mateu Villaret (CPAIOR, 2019)

New complexity results for Łukasiewicz logic. - Miquel Bofill; Felip Manyà; Amanda Vidal; Mateu Villaret (Soft Comput., 2019)

Resource Analysis driven by (Conditional) Termination Proofs. - Elvira Albert; Miquel Bofill; Cristina Borralleras; Enrique Martin-Martin; Albert Rubio (Theory Pract. Log. Program., 2019)

An MDD-based SAT encoding for pseudo-Boolean constraints with at-most-one relations. - Miquel Bofill; Jordi Coll; Josep Suy; Mateu Villaret (Artif. Intell. Rev., 2020)

SMT encodings for Resource-Constrained Project Scheduling Problems. - Miquel Bofill; Jordi Coll; Josep Suy; Mateu Villaret (Comput. Ind. Eng., 2020)

Relaxing non-interference requirements in parallel plans. - Miquel Bofill; Joan Espasa; Mateu Villaret (Log. J. IGPL, 2021)

SAT encodings for Pseudo-Boolean constraints together with at-most-one constraints. - Miquel Bofill; Jordi Coll; Peter Nightingale; Josep Suy; Felix Ulrich-Oltean; Mateu Villaret (Artif. Intell., 2022)

The Sample Analysis Machine Scheduling Problem: Definition and comparison of exact solving approaches. - Miquel Bofill; Jordi Coll; Gerard Martín; Josep Suy; Mateu Villaret (Comput. Oper. Res., 2022)

The Impact of Implied Constraints on MaxSAT B2B Instances. - Miquel Bofill; Jordi Coll; Jesús Giráldez-Cru; Josep Suy; Mateu Villaret (Int. J. Comput. Intell. Syst., 2022)

Constraint Solving Approaches to the Business-to-Business Meeting Scheduling Problem. - Miquel Bofill; Jordi Coll; Marc Garcia; Jesús Giráldez-Cru; Gilles Pesant; Josep Suy; Mateu Villaret (J. Artif. Intell. Res., 2022)

Constraint Solving Approaches to the Business-to-Business Meeting Scheduling Problem (Extended Abstract). - Miquel Bofill; Jordi Coll; Marc Garcia; Jesús Giráldez-Cru; Gilles Pesant; Josep Suy; Mateu Villaret (IJCAI, 2023)

SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints (Extended Abstract). - Miquel Bofill; Jordi Coll; Peter Nightingale; Josep Suy; Felix Ulrich-Oltean; Mateu Villaret (IJCAI, 2023)

On Grid Graph Reachability and Puzzle Games. - Miquel Bofill; Cristina Borralleras; Joan Espasa; Mateu Villaret (CoRR, 2023)

A Good Snowman is Hard to Plan. - Miquel Bofill; Cristina Borralleras; Joan Espasa; Gerard Martín; Gustavo Patow; Mateu Villaret (CoRR, 2023)