Research areas of interest

My research interest is related to Logic in Computer Science:

1. •AUTOMATED REASONING
   

2. •AUTOMATED PLANNING
   

3. 
   

Check the LAI research group web page for additional information (SOFTWARE, Etc.)

PUBLICATIONS (DBLP, GScholar)

Journal Articles

Josu Oca, Miquel Bofill, Cristina Borralleras

Efficient SMT formulations for classical planning

Journal of Logical and Algebraic Methods in Programming, Vol. 151, September 2026, 101145. © Elsevier Inc.

doi:10.1016/j.jlamp.2026.101145

Miquel Bofill, Jordi Coll, Jesús Giráldez-Cru, Josep Suy, Mateu Villaret

The Impact of Implied Constraints on MaxSAT B2B Instances

International Journal of Computational Intelligence Systems, Vol. 15, Article number: 63, August 2022. © Springer Nature

doi:10.1007/s44196-022-00121-5

Miquel Bofill, Jordi Coll, Gerard Martín, Josep Suy, Mateu Villaret

The Sample Analysis Machine Scheduling Problem: Definition and comparison of exact solving approaches

Computers & Operations Research, Vol. 142, June 2022, 105730. © Elsevier Ltd.

doi:10.1016/j.cor.2022.105730

Miquel Bofill, Jordi Coll, Marc Garcia, Jesús Giráldez-Cru, Gilles Pesant, Josep Suy, Mateu Villaret

Constraint Solving Approaches to the Business-to-Business Meeting Scheduling Problem

Journal of Artificial Intelligence Research, Vol. 74, pages 263–301, May 2022. © AI Access Foundation, Inc.

doi:10.1613/jair.1.12670

Miquel Bofill, Jordi Coll, Peter Nightingale, Josep Suy, Felix Ulrich-Oltean, Mateu Villaret

SAT encodings for Pseudo-Boolean constraints together with at-most-one constraints

Artificial Intelligence, Vol. 302, January 2022, 103604. © Elsevier Ltd.

Author’s version: [Paper]

The final publication is available online at doi: 10.1016/j.artint.2021.103604

Miquel Bofill, Joan Espasa, Mateu Villaret

Relaxing non-interference requirements in parallel plans

Logic Journal of the IGPL, Vol. 29(1), pages 45–71, February 2021. © Oxford University Press

Special issue on Logics and Artificial Intelligence, Published: 01 August 2019

doi:10.1093/jigpal/jzz026

Miquel Bofill, Jordi Coll, Josep Suy, Mateu Villaret

SMT encodings for Resource-Constrained Project Scheduling Problems

Computers & Industrial Engineering 149: 106777, November 2020. © Elsevier Ltd.

doi: 10.1016/j.cie.2020.106777

Miquel Bofill, Jordi Coll, Josep Suy, Mateu Villaret

An MDD-based SAT encoding for pseudo-Boolean constraints with at-most-one relations

Artificial Intelligence Review, Vol. 53(7), pages 5157–5188, October 2020. © Springer Nature

Author’s version: [Paper]

The final publication is available online at doi: 10.1007/s10462-020-09817-6

Elvira Albert, Miquel Bofill, Cristina Borralleras, Enrique Martin-Martin, Albert Rubio

Resource Analysis driven by (Conditional) Termination Proofs

Theory and Practice of Logic Programming, Vol. 19(5-6), pages 722–739, September 2019. © Cambridge University Press

doi: 10.1017/S1471068419000152

Miquel Bofill, Felip Manyà, Amanda Vidal, Mateu Villaret

New complexity results for Łukasiewicz logic

Soft Computing, Vol. 23(7), pages 2187–2197, April 2019. © Springer Berlin Heidelberg

doi: 10.1007/s00500-018-3365-9

Miquel Bofill, Joan Espasa, Mateu Villaret

The RANTANPLAN planner: system description

The Knowledge Engineering Review, Vol. 31(5), pages 452–464, November 2016. © Cambridge University Press

Author’s version: [Paper] [BibTeX]

End-users may view and download the material for private research and study only.

The final publication is available online at doi: 10.1017/S0269888916000229

Carlos Ansótegui, Miquel Bofill, Felip Manyà, Mateu Villaret

Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers

Fuzzy Sets and Systems, Vol. 292, pages 32–48, June 2016. © Elsevier B.V.

doi: 10.1016/j.fss.2015.04.011

Marta Verdaguer, Josep Suy, Mateu Villaret, Narcís Clara, Miquel Bofill, Manel Poch

An exact approach for the prioritization process of industrial influents in wastewater systems

Clean Technologies and Environmental Policy, Volume 18, Issue 1, pages 339–346, January 2016. © Springer

First published online: June 18, 2015

doi: 10.1007/s10098-015-0992-z

Carlos Ansótegui, Miquel Bofill, Felip Manyà, Mateu Villaret

SAT and SMT Technology for Many-Valued Logics

Multiple-Valued Logic and Soft Computing, Vol. 24(1-4), pages 151–172, 2015. © Old City Publishing

Author’s version: [Paper] [BibTeX]

The final publication is available online at [URL]

Miquel Bofill, Ginés Moreno, Carlos Vázquez, Mateu Villaret

Automatic Proving of Fuzzy Formulae with Fuzzy Logic Programming and SMT

Electronic Communications of the EASST, Vol. 64: Programming and Computer Languages 2013, 1–19, 2014.

[URL]

Miquel Bofill, Dídac Busquets, Víctor Muñoz, Mateu Villaret

Reformulation based MaxSAT robustness

Constraints, Vol. 18(2), pages 202–235, April 2013. © Springer

First published online: November 14, 2012

Author’s version: [Paper] [BibTeX]

The final publication is available online at doi: 10.1007/s10601-012-9130-2

Carlos Ansótegui, Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret

Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories

Constraints, Vol. 18(2), pages 236–268, April 2013. © Springer

First published online: November 13, 2012

Author’s version: [Paper] [BibTeX]

The final publication is available online at doi: 10.1007/s10601-012-9131-1

Miquel Bofill, Cristina Borralleras, Enric Rodríguez-Carbonell, Albert Rubio

The recursive path and polynomial ordering for first-order and higher-order terms

Journal of Logic and Computation, Vol. 23(1), pages 263–305, February 2013.

First published online: June 22, 2012

Author’s version: [Paper] [BibTeX]

The final publication is available online at doi: 10.1093/logcom/exs027

Miquel Bofill, Albert Rubio

Paramodulation with Non-Monotonic Orderings and Simplification

Journal of Automated Reasoning, Vol. 50:1, pages 51–98, January 2013. © Springer

First published online: December 15, 2011

Author’s version: [Paper] [BibTeX]

The final publication is available online at doi: 10.1007/s10817-011-9244-z

Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret

Solving constraint satisfaction problems with SAT modulo theories

Constraints, Vol. 17(3), pages 273–303, July 2012. © Springer

Author’s version: [Paper] [BibTeX]

The final publication is available online at doi: 10.1007/s10601-012-9123-1

Miquel Bofill, Albert Rubio

Paramodulation with Well-founded Orderings

Journal of Logic and Computation, Vol. 19(2), pages 263–302, April 2009.

First published online: November 21, 2008

Author’s version: [Paper] [BibTeX]

The final publication is available online at doi: 10.1093/logcom/exn073

Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio

Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings

Journal of Automated Reasoning, Vol. 30:1, pages 99–120, January 2003. © Kluwer

Author’s version: [Paper] [BibTeX]

The final publication is available online at doi: 10.1023/A:1022515030222

Conference and Workshop Papers

Miquel Bofill, Cristina Borralleras, Josu Oca

A Simple Yet Efficient Lifted Formulation for Hard-to-Ground Planning Problems

In 25th Workshop on Constraint Modelling and Reformulation (ModRef 2026)

Co-located with the 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

Lisbon, Portugal, July 2026.

[Paper]

Mustafa F. Abdelwahed, Miquel Bofill, Joan Espasa, Mateu Villaret

On-Demand Mutex Constraints for Numeric Planning as SMT

In Procs. 36th International Conference on Automated Planning and Scheduling (ICAPS 2026)

pages 362–366, Dublin, Ireland, July 2026. © AAAI

[URL]

Miquel Bofill, Cristina Borralleras, Josu Oca

Lifted Planning as SMT

In Constraint And Satisfiability-based Planning: an Exploratory Research Workshop (CASP:ER 2026)

Co-located with the 36th International Conference on Automated Planning and Scheduling (ICAPS 2026)

Dublin, Ireland, June 2026.

[Paper]

Miquel Bofill, Cristina Borralleras, Joan Espasa, Mateu Villaret

A Spanning Tree-Based SAT Encoding for Reachability in Undirected Graphs

In Procs. 56th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2026)

pages 37-42, Sendai, Japan, May 2026.

Author’s version: [Paper] [BibTeX]

© IEEE, 2026. doi: 10.1109/ISMVL68998.2026.00016

Miquel Bofill, Josu Oca

Towards Compact and Efficient SMT Formulations for AI Planning

In Actas de las XXIV Jornadas de Programación y Lenguajes (PROLE 2025). Sistedes (2025).

Córdoba, Spain, September 2025.

[Paper] [BibTeX]

Miquel Bofill, Jordi Coll, Marc Garcia, Jesús Giráldez-Cru, Gilles Pesant, Josep Suy, Mateu Villaret

Constraint Solving Approaches to the Business-to-Business Meeting Scheduling Problem (Extended Abstract)

In Procs. 32nd International Joint Conference on Artificial Intelligence (IJCAI 2023)

pages 6851-6852, Macao, SAR, China, August 2023. ijcai.org

[Paper]

Miquel Bofill, Jordi Coll, Peter Nightingale, Jesús Giráldez-Cru, Josep Suy, Felix Ulrich-Oltean, Mateu Villaret

SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints (Extended Abstract)

In Procs. 32nd International Joint Conference on Artificial Intelligence (IJCAI 2023)

pages 6853-6857, Macao, SAR, China, August 2023. ijcai.org

[Paper]

Miquel Bofill, Cristina Borralleras, Joan Espasa, Mateu Villaret

On Grid Graph Reachability and Puzzle Games

In 22nd Workshop on Constraint Modelling and Reformulation (ModRef 2023)

Co-located with the 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)

Toronto, Canada, August 2023.

[Paper]

Miquel Bofill, Cristina Borralleras, Joan Espasa, Gerard Martin, Gustavo Patow, Mateu Villaret

A Good Snowman is Hard to Plan

In 2023 Workshop on Knowledge Engineering for Planning and Scheduling (KEPS 2023)

Co-located with the 33rd International Conference on Automated Planning and Scheduling (ICAPS 2023)

Prague, Czech Republic, July 2023.

[Paper]

Miquel Bofill, Jesús Giráldez-Cru, Josep Suy, Mateu Villaret

A Study on Implied Constraints in a MaxSAT Approach to B2B Problems

In Procs. 22nd International Conference of the Catalan Association for Artificial Intelligence (CCIA 2019)

Artificial Intelligence Research and Development

Frontiers in Artificial Intelligence and Applications, Vol. 319, pages 183–192. © IOS Press

Author’s version: [Paper] [BibTeX]

The final publication is available at IOS Press through https://dx.doi.org/10.3233/FAIA190123

Carlos Ansótegui, Miquel Bofill, Jordi Coll, Nguyen Dang, Juan Luis Esteban, Ian Miguel, Peter Nightingale, András Z. Salamon, Josep Suy, Mateu Villaret

Automatic Detection of At-Most-One and Exactly-One Relations for Improved SAT Encodings of Pseudo-Boolean Constraints

In Procs. 25th International Conference on Principles and Practice of Constraint Programming (CP 2019)

LNCS 11802, pages 20–36, Stamford, CT, USA, September 30 – October 4, 2019. © Springer-Verlag

Author’s version: [Paper] [BibTeX]

The final authenticated publication is available at doi: 10.1007/978-3-030-30048-7_2

Miquel Bofill, Jordi Coll, Josep Suy, Mateu Villaret

SAT Encodings of Pseudo-Boolean Constraints with At-Most-One Relations

In Procs. 16th International Conference on Integration of Constraint Programming, Artificial Intelligence and Operations Research (CPAIOR 2019)

LNCS 11494, pages 112–128, Thessaloniki, Greece, June 2019. © Springer

Author’s version: [Paper] [BibTeX]

The final authenticated publication is available online at doi: 10.1007/978-3-030-19212-9_8

Miquel Bofill, Joan Espasa, Mateu Villaret

Relaxed Exists-Step Plans in Planning as SMT

In Procs. 26th International Joint Conference on Artificial Intelligence (IJCAI 2017)

pages 563–570, Melbourne, Australia, August 2017. ijcai.org

[Paper]

Miquel Bofill, Jordi Coll, Josep Suy, Mateu Villaret

Compact MDDs for Pseudo-Boolean Constraints with At-Most-One Relations in Resource-Constrained Scheduling Problems

In Procs. 26th International Joint Conference on Artificial Intelligence (IJCAI 2017)

pages 555–562, Melbourne, Australia, August 2017. ijcai.org

[Paper]

Miquel Bofill, Jordi Coll, Josep Suy, Mateu Villaret

An Efficient SMT Approach to Solve MRCPSP/max Instances with Tight Constraints on Resources

In Procs. 23rd International Conference on Principles and Practice of Constraint Programming (CP 2017)

LNCS 10416, pages 71–79, Melbourne, VIC, Australia, August 28 – September 1, 2017. © Springer-Verlag

Author’s version: [Paper] [BibTeX]

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-66158-2_5

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

The Spanish Kidney Exchange Model: Study of Computation-Based Alternatives to the Current Procedure

In Procs. 16th Conference on Artificial Intelligence in Medicine (AIME 2017)

LNCS 10259, pages 272–277, Vienna, Austria, June 2017. © Springer

Author’s version: [Paper] [BibTeX]

The final publication is available at doi: 10.1007/978-3-319-59758-4

Miquel Bofill, Jordi Coll, Josep Suy, Mateu Villaret

Solving the Multi-Mode Resource-Constrained Project Scheduling Problem with SMT

In Procs. 28th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2016)

pages 239–246, San José, CA, USA, November 2016.

© IEEE, 2016. doi: 10.1109/ICTAI.2016.0045

[Paper] [BibTeX]

Miquel Bofill, Marc Garcia, Jesús Giráldez-Cru, Mateu Villaret

A Study on Implied Constraints in a MaxSAT Approach to B2B Problems

Workshop on Pragmatics of SAT (POS 2016)

Co-located with the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016)

Bordeaux, France, July 2016.

[URL] [BibTeX]

Miquel Bofill, Joan Espasa, Mateu Villaret

A Semantic Notion of Interference for Planning Modulo Theories

In Procs. 26th International Conference on Automated Planning and Scheduling (ICAPS 2016)

pages 56–64, London, UK, June 2016. © AAAI

[URL] [BibTeX]

Miquel Bofill, Felip Manyà, Amanda Vidal, Mateu Villaret

The Complexity of 3-Valued Łukasiewicz Rules

In Procs. 12th International Conference on Modeling Decisions for Artificial Intelligence (MDAI 2015)

LNCS 9321, pages 221–229, Skövde, Sweden, September 2015. © Springer

Author’s version: [Paper] [BibTeX]

The final publication is available at doi: 10.1007/978-3-319-23240-9_18

Jesús Manuel Almendros-Jiménez, Miquel Bofill, Alejandro Luna Tedesqui, Ginés Moreno, Carlos Vázquez, Mateu Villaret

Fuzzy XPath for the Automatic Search of Fuzzy Formulae Models

In Procs. 9th International Conference on Scalable Uncertainty Management (SUM 2015)

LNCS 9310, pages 385–398, Québec City, QC, Canada, September 2015. © Springer

Author’s version: [Paper] [BibTeX]

The final publication is available at doi: 10.1007/978-3-319-23540-0_26

Miquel Bofill, Felip Manyà, Amanda Vidal, Mateu Villaret

Finding Hard Instances of Satisfiability in Łukasiewicz Logics

In Procs. 45th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2015)

pages 30-35, Waterloo, Ontario, Canada, May 2015.

© IEEE, 2015. doi: 10.1109/ISMVL.2015.10

[Paper] [BibTeX]

Miquel Bofill, Marc Garcia, Josep Suy, Mateu Villaret

MaxSAT-Based Scheduling of B2B Meetings

In Procs. 12th International Conference on Integration of AI and OR Techniques in Constraint Programming (CPAIOR 2015)

LNCS 9075, pages 65–73, Barcelona, Spain, May 2015. © Springer

Author’s version: [Paper] [BibTeX]

The final publication is available at doi: 10.1007/978-3-319-18008-3_5

Miquel Bofill, Joan Espasa, Mateu Villaret

The RANTANPLAN planner: System description

In Workshop on Constraint Satisfaction Techniques for Planning and Scheduling Problems (COPLAS 2015)

Co-located with the 25th International Conference on Automated Planning and Scheduling (ICAPS 2015)

Jerusalem, Israel, June 2015.

[Paper]

Miquel Bofill, Jordi Coll, Josep Suy, Mateu Villaret

A System for Generation and Visualization of Resource-Constrained Projects

In Procs. 17th International Conference of the Catalan Association for Artificial Intelligence (CCIA 2014)

Artificial Intelligence Research and Development - Recent Advances and Applications

Frontiers in Artificial Intelligence and Applications, Vol. 269, pages 237–246. © IOS Press

Author’s version: [Paper] [BibTeX]

The final publication is available at doi: 10.3233/978-1-61499-452-7-237

Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret

Solving Intensional Weighted CSPs by Incremental Optimization with BDDs

In Procs. 20th International Conference on Principles and Practice of Constraint Programming (CP 2014)

LNCS 8656, pages 207–223, Lyon, France, September 2014. © Springer-Verlag

Author’s version: [Paper] [BibTeX]

The final publication is available at doi: 10.1007/978-3-319-10428-7_17

Miquel Bofill, Joan Espasa, Marc Garcia, Miquel Palahí, Josep Suy, Mateu Villaret

Scheduling B2B Meetings

In Procs. 20th International Conference on Principles and Practice of Constraint Programming (CP 2014)

LNCS 8656, pages 781–796, Lyon, France, September 2014. © Springer-Verlag

Author’s version: [Paper] [BibTeX]

The final publication is available at doi: 10.1007/978-3-319-10428-7_56

Miquel Bofill, Dídac Busquets, Mateu Villaret

Reformulation Based MaxSAT Robustness - (Extended Abstract)

In Procs. 20th International Conference on Principles and Practice of Constraint Programming (CP 2014)

LNCS 8656, pages 908–912, Lyon, France, September 2014. © Springer-Verlag

Author’s version: [Paper] [BibTeX]

The final publication is available at doi: 10.1007/978-3-319-10428-7_65

Miquel Bofill, Joan Espasa, Mateu Villaret

Efficient SMT Encodings for the Petrobras Domain

In Procs. 13th International Workshop on Constraint Modelling and Reformulation (ModRef 2014)

Co-located with the 20th International Conference on Principles and Practice of Constraint Programming (CP 2014)

pages 68–84, Lyon, France, September 2014.

[Paper] [BibTeX]

Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret

Boosting Weighted CSP Resolution with Shared BDDs

In Procs. 12th International Workshop on Constraint Modelling and Reformulation (ModRef 2013)

Co-located with the 19th International Conference on Principles and Practice of Constraint Programming (CP 2013)

pages 57–73, Uppsala, Sweden, September 2013.

[Paper] [BibTeX]

Miquel Bofill, Ginés Moreno, Carlos Vázquez, Mateu Villaret

Automatic Proving of Fuzzy Formulae with Fuzzy Logic Programming and SMT

In Procs. XIII Spanish Conference on Programming and Computer Languages (PROLE 2013)

pages 151–165, Madrid, Spain, September 2013.

[Paper] [BibTeX]

Miquel Bofill, Joan Espasa, Miquel Palahí, Mateu Villaret

An extension to Simply for solving Weighted Constraint Satisfaction Problems with Pseudo-Boolean Constraints

In Procs. XII Spanish Conference on Programming and Computer Languages (PROLE 2012)

pages 141–155, Almería, Spain, September 2012.

[Paper] [BibTex]

Carlos Ansótegui, Miquel Bofill, Felip Manyà, Mateu Villaret

Building Automated Theorem Provers for Infinitely-Valued Logics with Satisfiability Modulo Theory Solvers

In Procs. 42nd IEEE International Symposium on Multiple-Valued Logic (ISMVL 2012)

pages 25–30, Victoria, BC, Canada, May 2012.

© IEEE, 2012. doi: 10.1109/ISMVL.2012.63

[Paper] [BibTeX]

Miquel Bofill, Cristina Borralleras, Enric Rodríguez-Carbonell, Albert Rubio

The recursive path and polynomial ordering

In Procs. 12th International Workshop on Termination (WST 2012)

pages 29–33, Obergurgl, Austria, February 2012.

[Paper] [BibTeX]

Carlos Ansótegui, Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret

A Proposal for Solving Weighted CSPs with SMT

In Procs. 10th International Workshop on Constraint Modelling and Reformulation (ModRef 2011)

Co-located with the 17th International Conference on Principles and Practice of Constraint Programming (CP 2011)

pages 5–19, Perugia, Italy, September 2011.

[Paper] [BibTeX]

Carlos Ansótegui, Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret

W-MiniZinc: A Proposal for Modeling Weighted CSPs with MiniZinc

In Procs. 1st International Workshop on MiniZinc (MZN 2011)

Co-located with the 17th International Conference on Principles and Practice of Constraint Programming (CP 2011)

Perugia, Italy, September 2011.

[Paper] [BibTeX]

Carlos Ansótegui, Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret

Satisfiability Modulo Theories: an Efficient Approach for the Resource-Constrained Project Scheduling Problem

In Procs. 9th Symposium on Abstraction, Reformulation and Approximation (SARA 2011)

pages 2–9, Cardona, Spain, July 2011.

© AAAI Press, 2011.

[Paper] [BibTeX]

Carlos Ansótegui, Miquel Bofill, Felip Manyà, Mateu Villaret

Extending Multiple-Valued Clausal Forms with Linear Integer Arithmetic

In Procs. 41st IEEE International Symposium on Multiple-Valued Logic (ISMVL 2011)

pages 230–235, Tuusula, Finland, May 2011.

© IEEE, 2011. doi: 10.1109/ISMVL.2011.53

[Paper] [BibTeX]

Miquel Bofill, Dídac Busquets, Mateu Villaret

A Declarative Approach to Robust Weighted Max-SAT

In Procs. 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2010)

pages 67–76, Hagenberg, Austria, July 2010.

© ACM, 2010. This is the author’s version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in the Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming (PPDP 2010), Hagenberg, Austria, 26-28 July 2010.

doi: 10.1145/1836089.1836098

[Paper] [BibTeX]

Miquel Bofill, Josep Suy, Mateu Villaret

A System for Solving Constraint Satisfaction Problems with SMT

In Procs. 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010)

LNCS 6175, pages 300–305, Edinburgh, UK, July 2010. © Springer-Verlag

doi: 10.1007/978-3-642-14186-7_25

[Paper] [BibTeX]

Miquel Bofill, Dídac Busquets, Mateu Villaret

Auction Robustness through Satisfiability Modulo Theories

Proceedings of the Second Workshop on Agreement Technologies (WAT 2009)

Volume 635 of CEUR Workshop Proceedings, pages 33-44

Sevilla, Spain, November 2009

[Paper] [BibTeX]

Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret

SIMPLY: a Compiler from a CSP Modeling Language to the SMT-LIB Format

In Procs. 8th International Workshop on Constraint Modelling and Reformulation (ModRef 2009)

Co-located with the 15th International Conference on Principles and Practice of Constraint Programming (CP 2009)

pages 30–44, Lisbon, Portugal, September 2009.

[Paper] [Paper (long version)] [BibTeX]

Miquel Bofill, Miquel Palahí, Mateu Villaret

A System for CSP Solving through Satisfiability Modulo Theories

In Procs. IX Jornadas sobre Programación y Lenguajes (PROLE 2009)

pages 303–312, Donostia, Spain, September 2009.

[Paper] [BibTeX]

Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio

A Write-Based Solver for SAT Modulo the Theory of Arrays

In Procs. 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2008)

pages 1–8, Portland, USA, November 2008.

© IEEE, 2008. This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

doi: 10.1109/FMCAD.2008.ECP.18

[Paper] [BibTeX]

Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio

The Barcelogic SMT Solver

In Procs. 20th International Conference on Computer Aided Verification (CAV 2008)

LNCS 5123, pages 294–298, Princeton, USA, July 2008. © Springer-Verlag

doi: 10.1007/978-3-540-70545-1_27

[Paper] [BibTeX]

Miquel Bofill, Albert Rubio

Redundancy Notions for Paramodulation with Non-Monotonic Orderings

In Procs. 2nd International Joint Conference on Automated Reasoning (IJCAR 2004)

LNAI 3097, pages 107–121, Cork, Ireland, July 2004. © Springer-Verlag

doi: 10.1007/978-3-540-25984-8_6

[Paper] [Paper (long version)] [BibTeX]

Miquel Bofill, Albert Rubio

Well-foundedness is Sufficient for Completeness of Ordered Paramodulation

In Procs. 18th International Conference on Automated Deduction (CADE 2002)

LNAI 2392, pages 456–470, Copenhagen, Denmark, July 2002. © Springer-Verlag

doi: 10.1007/3-540-45620-1_36

[Paper] [Paper (long version)] [BibTeX]

Miquel Bofill, Guillem Godoy

On the Completeness of Arbitrary Selection Strategies for Paramodulation

In Procs. 28th International Colloquium on Automata, Languages and Programming (ICALP 2001)

LNCS 2076, pages 951–962, Crete, Greece, July 2001. © Springer-Verlag

doi: 10.1007/3-540-48224-5_77

[Paper] [Paper (long version)] [BibTeX]

Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio

Modular Redundancy for Theorem Proving

In Procs. 3rd International Workshop on Frontiers of Combining Systems (FroCoS 2000)

LNAI 1794, pages 186–199, Nancy, France, April 2000. © Springer-Verlag

doi: 10.1007/10720084_13

[Paper] [BibTeX]

Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio

Paramodulation with Non-Monotonic Orderings

In Procs. 14th Annual IEEE Symposium on Logic in Computer Science (LICS 1999)

pages 225–234, Trento, Italy, July 1999. © IEEE Comp. Sc. Press

doi: 10.1109/LICS.1999.782618 

[Paper] [BibTeX]

PhD thesis

Equational Reasoning with Non-Monotonic Orderings

Technical University of Catalonia, July 2004.

Supervisor: Albert Rubio

[Thesis]

ADVISEES

Josu Oca, ongoing

Joan Espasa, PhD (grad. 2018, co-advised, later at University of St Andrews)

Miquel Palahí, PhD (grad. 2015, co-advised, later at Unipart Group)

Josep Suy, PhD (grad. 2012, co-advised)