Research areas of interest

My research interest is related to Logic in Computer Science:

1. •term rewriting
   

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, Dídac Busquets, Víctor Muñoz, and Mateu Villaret

Reformulation based MaxSAT robustness

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

First published online: November 14, 2012

doi: 10.1007/s10601-012-9130-2

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

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

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

First published online: November 13, 2012

doi: 10.1007/s10601-012-9131-1

Miquel Bofill, Cristina Borralleras, Enric Rodríguez-Carbonell, and 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

doi: 10.1093/logcom/exs027

[BibTeX]

Miquel Bofill and 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

doi: 10.1007/s10817-011-9244-z

[BibTeX]

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

Solving constraint satisfaction problems with SAT modulo theories

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

doi: 10.1007/s10601-012-9123-1

[BibTeX]

Miquel Bofill and 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

doi: 10.1093/logcom/exn073

[Paper] [BibTeX]

Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, and 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

doi: 10.1023/A:1022515030222

[Paper] [BibTeX]

Conference and Workshop Papers

Miquel Bofill, Joan Espasa, Miquel Palahí, and 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.

[Proceedings]

Carlos Ansótegui, Miquel Bofill, Felip Manyà, and 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, and 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, and 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, and 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, and 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à, and 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, and 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] [Talk slides] [BibTeX]

Miquel Bofill, Josep Suy, and 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, and Mateu Villaret

Auction Robustness through Satisfiability Modulo Theories

In Workshop on Agreement Technologies (WAT - CAEPIA 2009)

Sevilla, Spain, November 2009.

[Paper] [Talk slides] [BibTeX]

Miquel Bofill, Miquel Palahí, Josep Suy, and 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í, and 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, and 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, and 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 and 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)] [Talk slides] [BibTeX]

Miquel Bofill and 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)] [Talk slides] [BibTeX]

Miquel Bofill and 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, and 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, and 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] [Slides]