Miquel Bofill Arasa

 

ACTING ASSOCIATE PROFESSOR


depT. informàtica, matemàtica aplicada I ESTADÍSTICA

Escola politècnica superior

Universitat de girona

C/ universitat de girona, 6

e-17003 girona - catalunya (spain)


How to get there


office p-IV 254

tel. (+34) 618 260 252

fax (+34) 972 418 792



PGP Public key

FINGERPRINT: 7D1A 93C4 54C7 E6FC A450 F193 5842 AE36 8240 C149

Research areas of interest

My research interest is related to Logic in Computer Science:

  1. AUTOMATED REASONING

  2. AUTOMATED THEOREM PROVING

  3. Satisfiability modulo theories


Check the L /\ P research group web page for additional information (SOFTWARE, ...)

PUBLICATIONS (DBLP, GScholar)


Journal Articles


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

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

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



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

In Workshop on Agreement Technologies (WAT - CAEPIA 2009)

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]