Bofill, M.; Coll, J.; Giráldez-Cru, J.; Suy, J.; Villaret, M. "The Impact of Implied Constraints on MaxSAT B2B Instances." International Journal Of Computational Intelligence Systems 15 (2022): -. Bofill, M.; Coll J.; Martín, G; Suy J.; Villaret M "The Sample analyzis machine scheduling problem: definition and comparison of exact solving approaches." Computers & Operations Research 142 (2022): -. Bofill, M.; Coll J.; Carcia, M.; Giráldez-Cru, J.; Pesant, G.; Suy, J.; Villaret, M. "Constraint solving approaches to the business-to-business meeting sheduling problem." Journal of Artificial Intelligence Research 74 (2022): 263-301. Bofill, M.; Coll J.; Nightingale P.; Suy J.; Ulrich-Oltean F.; Villaret M "SAT encodings for Pseudo-Boolean constraints together with at-most-one constraints." Artificial Intelligence 302 (2022): -. Bofill, M.; Coll, J.; Suy, J.; Villaret, M. "SMT encodings for Resource-Constrained Project Scheduling Problems." Computers & Industrial Engineering 149 (2020): 106777-. Bofill, M.; Coll, J.; Suy, J.; Villaret, M. "An MDD-based SAT encoding for pseudo-Boolean constraints with at-most-one relations." Artificial Intelligence Review 53 (2020): 5177-5188. Albert, E.; Bofill, M.; Borralleras, C.; Martin-Martin, E.; Rubio, A. "Resource Analysis driven by (Conditional) Termination Proofs." Theory And Practice Of Logic Programming 19 (2019): 722-739. Bofill, M.; Espasa, J.; Villaret, M. "Relaxing non-interference requirements in parallel plans." Logic Journal of the IGPL 29 (2019): 45-71. Miquel Bofill; Felip Manyà; Amanda Vidal; Mateu Villaret "New complexity results for Łukasiewicz logic." Soft Computing 23 (2019): 2187-2197. Bofill, M.; Espasa, J.; Villaret, M. "The RANTANPLAN planner: system description." Knowledge Engineering Review 31 (2016): 452-464. Bofill, M.; Muñoz, V.; Murillo, J. "Solving the Wastewater Treatment Plant Problem with SMT." Computing Reseach Repository - arXiv abs/1609.05367 (2016): -. Ansótegui, C.; Bofill, M.; Manyà, F.; Villaret, M. "Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers." Fuzzy Sets and Systems 292 (2016): 32-48. Verdaguer, M.; Suy, J.; Villaret, M.; Clara, N.; Bofill, M.; Poch, M. "An exact approach for the prioritization process of industrial influents in wastewater systems." Clean Technologies and Environmental Policy 18 (2016): 339-346. Bofill, M; Moreno, G.; Vázquez, C.; Villaret, M. "Automatic Proving of Fuzzy Formulae with Fuzzy Logic Programming and SMT." Electronic Communications of the EASST 64 (2015): 1-19. Ansótegui C.; Bofill M.; Manyà F.; Villaret, M. "SAT and SMT Technology for Many-Valued Logics." Journal of Multiple-Valued Logic And Soft Computing 24 (2015): 151-172. Ansótegui, C.; Bofill, M.; Palahí, M., Suy, J.; Villaret, M. "Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories." Constraints 18 (2013): 236-268. Bofill, M.; Busquets, D.; Muñoz, V.; Villaret, M. "Reformulation based MaxSAT robustness." Constraints 18 (2013): 202-235. Bofill, M.; Borralleras, C.; Rodríguez-Carbonell, E.; Rubio, A. "The recursive path and polynomial ordering for first-order and higher-order terms." Journal of Logic and Computation 23 (2013): 263-305. Bofill, M.; Rubio, A. "Paramodulation with Non-Monotonic Orderings and Simplification." Journal of Automated Reasoning 50 (2013): 51-98. Bofill, M.; Palahí, M., Suy, J.; Villaret, M. "Solving Constraint Satisfaction Problems with SAT Modulo Theories." Constraints 17 (2012): 273-303. Bofill, M.; Rubio, A. "Paramodulation with well-founded orderings." Journal of Logic and Computation 19 (2009): 263-302. Bofill, M.; Godoy, G.; Nieuwenhuis, R.; Rubio, A. "Paramodulation and knuth-bendix completion with nontotal and nonmonotonic orderings." Journal of Automated Reasoning 30 (2003): 99-120.
Ansótegui, C.; Bofill, M.; Palahí, M.; Suy, J.; Villaret, M. "W-MiniZinc: A Proposal for Modeling Weighted CSPs with MiniZinc." 1st International Workshop on MiniZinc (MZN 2011) (2011): -. Bofill, M.; Suy, J.; Villaret, M. "A system for solving constraint satisfaction problems with SMT." Lecture Notes in Computer Science 6175 (2010): 300-305. Bofill, M.; Busquets, D.; Villaret, M. "A declarative approach to robust weighted max-SAT ." Principles and Practice of Declarative Programming, 12th International ACM SIGPLAN Symposium (2010): 67-76. Bofill, M.; Palahí, M.; Suy, J.; Villaret, M. "Simply: a Compiler from a CSP Modeling Language to the SMT-LIB Format." Constraint Modelling and Reformulation, 8th International Workshop (2009): 30-44. Bofill, M.; Palahí, M.; Villaret, M. "A System for CSP solving through Satisfiability Modulo Theories ." Programación y Lenguajes, IX Jornadas (2009): 303-312. Bofill, M.; Nieuwenhuis, R.; Oliveras, A.; Rodríguez-Carbonell, E.; Rubio, A. "The Barcelogic SMT solver." Lecture Notes in Computer Science 5123/2008 (2008): 294-298. Bofill, M.; Nieuwenhuis, R.; Oliveras, A.; Rodríguez-Carbonell, E.; Rubio, A. "A write-based solver for SAT modulo the theory of arrays ." Proceedings of the International Conference on Formal Methods in Computer-Aided Design. FMCAD (2008): 1-8. Bofill, M.; Rubio, A. "Redundancy notions for paramodulation with non-monotonic orderings." Lecture Notes in Artificial Intelligence 3097 (2004): 107-121. Bofill, M.; Rubio, A. "Well-Foundedness is Sufficient for Completeness of Ordered Paramodulation." Lecture Notes in Artificial Intelligence 2392 (2002): 456-470.