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. Schmidt-Schauß, Manfred; Kutsia, Temur;|Levy, Jordi; Villaret, Mateu; Kutz, Yunus "Nominal Unification and Matching of Higher Order Expressions with Recursive Let." Fundamenta Informaticae 185 (2022): 247-283. 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. 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. Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu "Higher-Order Pattern Anti-Unification in Linear Time." Journal of Automated Reasoning 58 (2017): 293-310. Bofill, M.; Espasa, J.; Villaret, M. "The RANTANPLAN planner: system description." Knowledge Engineering Review 31 (2016): 452-464. 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. Kutsia T.; Levy J.; Villaret M. "Anti-unification for Unranked Terms and Hedges." Journal of Automated Reasoning 52 (2014): 155-190. 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.; Palahí, M., Suy, J.; Villaret, M. "Solving Constraint Satisfaction Problems with SAT Modulo Theories." Constraints 17 (2012): 273-303. Levy J.; Villaret M. "Nominal Unification from a Higher-Order Perspective." ACM Transactions on Computational Logic 13 (2012): 1-31. Levy J.; Schmidt-Schauss M.; Villaret M. "On the Complexity of Bounded and Stratified Second-order Unification." Logic Journal of the IGPL 19 (2011): 763-789. Kutsia T.; Levy J.; Villaret M. "On the relation between Context and Sequence Unification." Journal of Symbolic Computation 45 (2010): 74-95. Ruíz, D; Villaret, M. "TILC: The Interactive Lambda-Calculus Tracer." Electronic Notes in Theoretical Computer Science 248 (2009): 173-183. Levy J.; Villaret M. "Simplifying the signature in second-order unification." Applicable Algebra in Engineering Communication and Computing 20 (2009): 427-445. Lopez, B. ; Muñoz, V.; Murillo, J.; Barber, F.; Salido, M.A.; Abril, M.; Cervantes, M.; Caro, L.F.; Villaret, M. "Experimental analysis of optimization techniques on the road passenger transportation problem ." Engineering Applications of Artificial Intelligence 22 (2009): 374-388. Levy, J.; Schmidt-Schauss, M.; Villaret, M. "The complexity of monadic second-order unification." SIAM Journal on Computing 38 (2008): 1113-1140.
Baumgartner, A.; Kutsia, T.; Levy, J.; Villaret, M. "A Variant of Higher-Order Anti-Unification." Leibniz International Proceedings in Informatics 21 (2013): 113-127. Ansótegui C.; Bofill M.; Manyà F.; Villaret, M. "Building Automated Theorem Provers for Infinitely-Valued Logics with Satisfiability Modulo Theory Solvers." Proceedings of The International Symposium on Multiple-Valued Logic (2012): 25-30. Kutsia, T.; Levy, J.; Villaret, M. "Anti-Unification for Unranked Terms and Hedges." Leibniz International Proceedings in Informatics 10 (2011): 219-234. 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): -. Ansótegui C.; Bofill M.; Manyà F.; Villaret, M. "Extending Multi-Valued Clausal Forms with Linear Integer Arithmetic." Multi-Valued Logic, 41st IEEE International Symposium (2011): 230-235. Ansótegui, C.; Bofill, M.; Palahí, M.; Suy, J.; Villaret, M. "A Proposal for Solving Weighted CSPs with SMT." Constraint Modelling and Reformulation, 10th International Workshop (2011): 5-19. Ansótegui, C.; Bofill, M.; Palahí, M.; Suy, J.; Villaret, M. "Satisfiability Modulo Theories: an Efficient Approach for the Resource-Constrained Project Scheduling Problem." Abstraction, Reformulation and Abstraction, 9th Symposium (2011): 2-9. 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. Levy, J.; Villaret, M. "An Efficient Nominal Unification Algorithm." Leibniz International Proceedings in Informatics 6 (2010): 209-226. 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.; Palahí, M.; Villaret, M. "A System for CSP solving through Satisfiability Modulo Theories ." Programación y Lenguajes, IX Jornadas (2009): 303-312. 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. Levy, J.; Villaret, M. "Nominal unification from a higher-order perspective." Lecture Notes in Computer Science 5117 (2008): 246-260. Kutsia, T.; Levy, J.; Villaret, M. "Sequence unification through currying." Lecture Notes in Computer Science 4533 (2007): 288-302. Levy, J.; Schmidt-Schauss, M.; Villaret, M. "Stratified Context Unification is NP-Complete." Lecture Notes in Artificial Intelligence 4130 (2006): 82-96. Levy, J.; Schmidt-Schauss, M.; Villaret, M. "Bounded Second-Order Unification is NP-Complete." Lecture Notes in Computer Science 4098 (2006): 400-414. Niehren, J.; Villaret, M. "Describing Lambda-Terms in Context Unification." Lecture Notes in Artificial Intelligence 3492 (2005): 221-237. Levy, J.; Niehren, J.; Villaret, M. "Well-nested Context Unification ." Lecture Notes in Artificial Intelligence 3632 (2005): 149-163. Levy, J.; Schmidt-Schauss, M.; Villaret, M. "Monadic second-order unification is NP-complete." Lecture Notes in Computer Science 3091 (2004): 55-69. Levy, J.; Villaret, M. "Currying Second-Order Unification Problems." Lecture Notes in Computer Science 2378 (2002): 326-339. Niehren, J.; Villaret, M. "Parallelism and Tree Regular Constraints." Lecture Notes in Artificial Intelligence 2514 (2002): 311-326. Levy, J.; Villaret, M. "Context unification and traversal equations." Lecture Notes in Computer Science 2051 (2001): 169-184. Levy, J.; Villaret, M. "Linear second-order unification and context unification with tree-regular constraints." Lecture Notes in Computer Science 1833 (2000): 156-171.