| Solving constraint satisfaction problems with SAT modulo theories M Bofill, M Palahí, J Suy, M Villaret Constraints 17 (3), 273-303, 2012 | 70 | 2012 |
| An efficient nominal unification algorithm J Levy, M Villaret Proceedings of the 21st International Conference on Rewriting Techniques and …, 2010 | 68 | 2010 |
| Anti-unification for unranked terms and hedges T Kutsia, J Levy, M Villaret Journal of Automated Reasoning 52 (2), 155-190, 2014 | 60 | 2014 |
| Satisfiability modulo theories: An efficient approach for the resource-constrained project scheduling problem C Ansótegui, M Bofill, M Palahı, J Suy, M Villaret Proceedings of the 9th Symposium on Abstraction, Reformulation and …, 2011 | 56 | 2011 |
| Nominal unification from a higher-order perspective J Levy, M Villaret International Conference on Rewriting Techniques and Applications, 246-260, 2008 | 52 | 2008 |
| Nominal unification from a higher-order perspective J Levy, M Villaret ACM Transactions on Computational Logic (TOCL) 13 (2), 1-31, 2012 | 45 | 2012 |
| MaxSAT-based scheduling of B2B meetings M Bofill, M Garcia, J Suy, M Villaret International Conference on Integration of Constraint Programming …, 2015 | 41 | 2015 |
| Building automated theorem provers for infinitely-valued logics with satisfiability modulo theory solvers C Ansótegui, M Bofill, F Manyà, M Villaret 2012 IEEE 42nd International Symposium on Multiple-Valued Logic, 25-30, 2012 | 38 | 2012 |
| A system for solving constraint satisfaction problems with SMT M Bofill, J Suy, M Villaret International Conference on Theory and Applications of Satisfiability …, 2010 | 37 | 2010 |
| SMT encodings for resource-constrained project scheduling problems M Bofill, J Coll, J Suy, M Villaret Computers & Industrial Engineering 149, 106777, 2020 | 36 | 2020 |
| Nominal unification of higher order expressions with recursive let M Schmidt-Schauß, T Kutsia, J Levy, M Villaret International Symposium on Logic-Based Program Synthesis and Transformation …, 2016 | 35 | 2016 |
| Linear second-order unification and context unification with tree-regular constraints J Levy, M Villaret International Conference on Rewriting Techniques and Applications, 156-171, 2000 | 34 | 2000 |
| Higher-order pattern anti-unification in linear time A Baumgartner, T Kutsia, J Levy, M Villaret Journal of Automated Reasoning 58 (2), 293-310, 2017 | 32 | 2017 |
| Nominal anti-unification A Baumgartner, T Kutsia, J Levy, M Villaret arXiv preprint arXiv:2504.21097, 2025 | 31 | 2025 |
| New complexity results for Łukasiewicz logic M Bofill, F Manyà, A Vidal, M Villaret Soft Computing 23 (7), 2187-2197, 2019 | 27 | 2019 |
| The RANTANPLAN planner: system description M Bofill, J Espasa, M Villaret The Knowledge Engineering Review 31 (5), 452-464, 2016 | 26 | 2016 |
| SIMPLY: a Compiler from a CSP Modeling Language to the SMT-LIB Format M Bofill, M Palahı, J Suy, M Villaret Proceedings of the 8th international workshop on constraint modelling and …, 2009 | 26 | 2009 |
| Constraint solving approaches to the business-to-business meeting scheduling problem M Bofill, J Coll, M Garcia, J Giráldez-Cru, G Pesant, J Suy, M Villaret Journal of Artificial Intelligence Research 74, 263-301, 2022 | 23 | 2022 |
| On the complexity of bounded second-order unification and stratified context unification J Levy, M Schmidt-Schauß, M Villaret Logic Journal of IGPL 19 (6), 763-789, 2011 | 23 | 2011 |
| The complexity of monadic second-order unification J Levy, M Schmidt-Schauß, M Villaret SIAM Journal on Computing 38 (3), 1113-1140, 2008 | 23 | 2008 |