Dave De Jonge; Filippo Bistaffa; Jordi Levy (2021). A Heuristic Algorithm for Multi-Agent Vehicle Routing with Automated Negotiation. Proc. of the 20th Int. Conf. on Autonomous Agents and Multiagent Systems, AAMAS'21. [PDF]
Thomas Bläsius; Tobias Friedrich; Andreas Göbel; Jordi Levy; Ralf Rothenberger (2021). The Impact of Heterogeneity and Geometry on the Proof Complexity of Random Satisfiability. Proc. of the 2021 ACM-SIAM Symposium on Discrete Algorithms, SODA'21. DOI: https://doi.org/10.1137/1.9781611976465.4. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jesús Giráldez-Cru; Jordi Levy (2020). The Self-Similarity of Industrial SAT Instances. Preprints 2020, 2020100560. DOI: https://doi.org/10.20944/preprints202010.0560.v1. [PDF]
María Luisa Bonet; Jordi Levy (2020). Equivalence Between Systems Stronger Than Resolution. Proc. of the 23rd Int. Conf. on Theory and Applications of Satisfiability Testing, SAT'20. LNCS 12178, pp 166-181, Springer. DOI: https://doi.org/10.1007/978-3-030-51825-7_13. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy (2019). Scale-Free Random SAT Instances. arXiv:1708.06805. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jesús Giráldez-Cru; Jordi Levy Laurent Simon (2019). Community Structure in Industrial SAT Instances. Journal of Artificial Intelligence Research 66(10):443-472. DOI: https://doi.org/10.1613/jair.1.11741. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy (2019). Phase Transition in Realistic Random SAT Models. Proc. of the 22nd Int. Conf. of the Catalan Association for Artificial Intelligence, CCIA'19. Frontiers in Artificial Intelligence and Applications. IOS Press. DOI: https://doi.org/10.3233/FAIA190126. [PDF]
Alexander Baumgartner; Temur Kutsia; Jordi Levy; Mateu Villaret (2018). Term-Graph Anti-Unification. Proc. of the 3rd Int. Conf. on Formal Structures for Computation and Deduction, FSCD'18. Leibniz International Proceedings in Informatics (LIPIcs), Vol. 108. DOI: 10.4230/LIPIcs.FSCD.2018.9. [PDF]
Jordi Levy (2017). Popularity and Similarity in SAT. Proc. of the Mapping Complexity Foundations and Applications of Network Geometry Workshop, MACFANG'17. [PDF] [slides]
Jesús Giráldez-Cru; Jordi Levy (2017). Locality in Random SAT Instances. Proc. of the 26th Int. Joint Conf on Artificial Intelligence, IJCAI'17, pp. 638-644. [PDF] [software][slides]
Alexander Baumgartner; Temur Kutsia; Jordi Levy; Mateu Villaret (2017). Higher-Order Pattern Anti-Unification in Linear Time. Journal of Automated Reasoning, Vol. 58, Num. 2, pp. 293-310. DOI: 10.1007/s10817-016-9383-3. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jesús Giráldez-Cru; Jordi Levy (2017). Structure Features for SAT Instances Classification. Journal of Applied Logic, Vol. 23, pp. 27-39. DOI: 10.1016/j.jal.2016.11.004. [PDF]
Jordi Levy (2017). Percolation and Phase Transition in SAT. arXiv:1708.06805.pdf [PDF]
Manfred Schmidt-Schauss; Temur Kutsia; Jordi Levy; Mateu Villaret (2016). Nominal Unification of Higher Order Expressions with Recursive Let. 26th Int. Symp. on Logic-Based Program Synthesis and Transformation, LOPSTR 2016. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jesús Giráldez-Cru; Jordi Levy (2016). Community Structure in Industrial SAT Instances. arXiv:1606.03329. [PDF]
Jesús Giráldez-Cru; Jordi Levy (2016). Generating SAT instances with community structure. Artificial Intelligence, Vol. 238, pp. 119-134. DOI: 10.1016/j.artint.2016.06.001. [PDF]
Carlos Ansótegui; Joel Gabàs; Jordi Levy (2016). Exploiting subproblem optimization in SAT-based MaxSAT algorithms. J. Heuristics, Vol. 22, Num. 1, pp. 1-53. DOI: 10.1007/s10732-015-9300-7. [PDF]
Carlos Ansótegui; Jesús Giráldez-Cru; Jordi Levy; Laurent Simon (2015). Using Community Structure to Detect Relevant Learnt Clauses. Proc. of the 18th Int. Conf. on Theory and Applications of Satisfiability Testing, SAT'15. DOI: 10.1007/978-3-319-24318-4_18. [PDF] [slides]
Jesús Giráldez-Cru; Jordi Levy (2015). A Modularity-based Random SAT Instances Generator. Proc. of the 24th Int. Joint Conf on Artificial Intelligence, IJCAI'15. AAAI Press, pp. 1952-1958. [PDF] [slides] [software]
Alexander Baumgartner; Temur Kutsia; Jordi Levy; Mateu Villaret (2015). Nominal Anti-Unification. Proc. of the 26th Int. Conf. on Rewriting Techniques and Applications, RTA'15. DOI: 10.4230/LIPIcs.RTA.2015.57. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jesús Giráldez-Cru; Jordi Levy (2015). On the Classification of Industrial SAT Families. Proc. of the 18th Int. Conf. of the Catalan Association for Artificial Intelligence, CCIA'15. Frontiers in Artificial Intelligence and Applications, Vol. 277, pp. 163-172. IOS Press. DOI: 10.3233/978-1-61499-578-4-163. [PDF] [slides]
Temur Kutsia; Jordi Levy; Mateu Villaret (2014). Anti-unification for Unranked Terms and Hedges. Journal of Automated Reasoning, Vol. 52, Num. 2, pp. 155-190. DOI: 10.1007/s10817-013-9285-6. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jesús Giráldez-Cru; Jordi Levy (2014). The Fractal Dimension of SAT Formulas. Proc. of the 7th Int. Joint Conf. on Automated Reasoning, IJCAR'14. DOI: 10.1007/978-3-319-08587-6_8. [PDF] [slides]
Alexander Baumgartner; Temur Kutsia; Jordi Levy; Mateu Villaret (2014). Nominal Anti-Unification. Proc. of the 28th Int. Workshop on Unification, UNIF'14. [PDF]
Jordi Levy (2014). On the Limits of Second-Order Unification. Proc. of the 28th Int. Workshop on Unification, UNIF'14. [PDF] [slides]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy (2013). SAT-Based MaxSAT Algorithms. Artificial Intelligence, Vol. 196, pp. 77-105. DOI: 10.1016/j.artint.2013.01.002. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy; Felip Manyà (2013). Resolution Procedures for Multiple-Valued Optimization. Information Sciences, Vol. 227, pp. 43-59. DOI: 10.1016/j.ins.2012.12.004. [PDF]
Carlos Ansótegui; María Luisa Bonet; Joel Gabàs; Jordi Levy (2013). Improving WPM2 for (Weighted) Partial MaxSAT. Proc of the 19th Int. Conf. on Principles and Practice of Constraint Programming, CP'13. Lecture Notes in Computer Science, Vol. 8124, pp. 117-132. DOI: 10.1007/978-3-642-40627-0_12. [PDF]
Alexander Baumgartner; Temur Kutsia; Jordi Levy; Mateu Villaret (2013). A Variant of Higher-Order Anti-Unification. Proc. of the 24st Int. Conf. on Rewriting Techniques and Applications, RTA'13. LIPIcs 21, pp. 113-127. DOI: 10.4230/LIPIcs.RTA.2013.113. [PDF]
Jordi Levy; Mateu Villaret (2012). Nominal Unification from a Higher-Order Perspective. ACM Transactions on Computational Logics, Vol. 13, Num. 2, pp. 10. DOI: 10.1145/2159531.2159532. [PDF]
Carlos Ansótegui; Jesús Giráldez-Cru; Jordi Levy (2012). The Community Structure of SAT Formulas. Proc. of the 15th Int. Conf. on Theory and Applications of Satisfiability Testing, SAT'12. Lecture Notes in Computer Science, Vol. 7317, pp. 410-423. Springer. [PDF] [slides]
Carlos Ansótegui; María Luisa Bonet; Joel Gabàs; Jordi Levy (2012). Improving SAT-Based Weighted MaxSAT Solvers. Proc. of the 18th Int. Conf. on Principles and Practice of Constraint Programming, CP'12. Lecture Notes in Computer Science, Vol. 7514, pp. 86-101. Springer. [PDF] [slides]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy; Chu Min Li (2012). Analysis and Generation of Pseudo-Industrial MaxSAT Instances. Proc. of the 15th Int. Conf. of the ACIA, CCIA'12. IOS Press, pp. 173-184. [PDF] [slides]
Jordi Levy; Manfred Schmidt-Schauss; Mateu Villaret (2011). On the complexity of Bounded Second-Order Unification and Stratified Context Unification. Logic Journal of the IGPL, Vol. 19, Num. 6, pp. 763-789. DOI: 10.1093/jigpal/jzq010. [PDF]
Temur Kutsia; Jordi Levy; Mateu Villaret (2011). Anti-Unification for Unranked Terms and Hedges. Proc. of the 22st International Conference on Rewriting Techniques and Applications, RTA'11. LIPIcs 10, pp. 219-234. [PDF]
Carlos Ansótegui; Jordi Levy (2011). On the Modularity of Industrial SAT Instances. Proc. of the 14th Int. Conf. of the ACIA, CCIA'11. IOS Press, pp. 11-20. [PDF] [slides]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy (2010). A New Algorithm for Weighted Partial MaxSAT. Proc. of the 24th AAAI Conf. on Artificial Intelligence, AAAI'10. [PDF]
Jordi Levy; Mateu Villaret (2010). An Efficient Nominal Unification Algorithm. Proc. of the 21st International Conference on Rewriting Techniques and Applications, RTA'10. LIPIcs 6, pp. 209-226. [PDF] [slides]
Kutsia, Temur; Jordi Levy; Mateu Villaret (2010). On the relation between Context and Sequence Unification. Journal of Symbolic Computation Vol. 45, Num. 1, pp. 74-95. DOI: 10.1016/j.jsc.2009.07.001. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy (2010). On Solving MaxSAT Through SAT. Pragmatics of SAT, POS-10. EPiC Series 8, pp 41-48. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy. On the Structure of Industrial SAT Instances. Proc. of the 15th Int. Conf. on Principles and Practice of Constraint Programming, CP'09. Lecture Notes in Computer Science, Vol. 5732, pp. 127-141. Springer. [PDF] [slides] [software]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy. Towards Industrial-Like Random SAT Instances. Proc. of the 21st Int. Joint Conf. on Artificial Intelligence, IJCAI'09, AAAI Press, pp. 387-392. [PDF] [slides] [software]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy. Solving (Weighted) Partial MaxSAT Through Satisfiability Testing. Proc. of the 12th Int. Conf. on Theory and Applications of Satisfiability Testing, SAT'09. Lecture Notes in Computer Science, Vol. 5584, pp. 427-440. Springer. [PDF] [slides]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy. On Solving MaxSAT Throught SAT Proc. of the 12th Int. Conf. of the ACIA, CCIA'09. IOS Press. [PDF]
Jordi Levy; Mateu Villaret (2009). Simplifying the Signature in Second-Order Unification. Applicable Algebra in Engineering, Communication and Computing, Vol. 20, Num. 5, pp. 427-445. DOI: 10.1007/s00200-009-0106-4. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy; Felip Manyà (2008). Measuring the Hardness of SAT Instances. Proc. of the 23th AAAI Conference on Artificial Intelligence, AAAI'08. AAAI Press, pp. 222-228. [PDF] [software]
Jordi Levy; Mateu Villaret (2008). Nominal Unification from a Higher-Order Perspective. Proc. of the 19th International Conference on Rewriting Techniques and Applications, RTA'08. Lecture Notes in Computer Science, Vol. 5117, pp. 246-260. Springer. [PDF]
Jordi Levy; Manfred Schmidt-Schauss; Mateu Villaret (2008). The Complexity of Monadic Second-Order Unification. SIAM Journal on Computing, Vol. 38, Num. 3 pp. 1113-1140. DOI: 10.1137/050645403. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy; Felip Manyà (2007). The Logic behind Weighted CSP. Proc. of the 20th International Joint Conference on Artificial Intelligence, IJCAI'07. AAAI Press, pp. 32-37. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy; Felip Manyà (2007). A Complete Resolution Calculus for Signed Max-SAT. Proc. of the 37th International Symposium on Multiple-Valued Logic, ISMVL'07. IEEE, pp. 22. [PDF]
María Luisa Bonet; Jordi Levy; Felip Manyà (2007). Resolution for Max-SAT. Artificial Intelligence, Vol. 171, Num. 8-9, pp. 606-618. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy; Felip Manyà (2007). Mapping CSP into Many-Valued SAT. Proc. of the 10th International Conference on Theory and Applications of Satisfiability Testing, SAT'07. Lecture Notes in Computer Science, Vol. 4501, pp. 10-15. Springer. [PDF]
Kutsia, Temur; Jordi Levy; Mateu Villaret (2007). Sequence Unification Through Currying. Proc. of the 18th International Conference on Rewriting Techniques and Applications, RTA'07. Lecture Notes in Computer Science, Vol. 4533, pp. 288-302. Springer. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy; Felip Manyà (2007). The Logic Behind Weighted CSP. Future and Trends in Constraint Programming. Frederic Benhamou, Narendra Jussien and Barry O'Sullivan eds., pp. 307-320. ISTE. [PDF]
Carlos Ansótegui; María Luisa Bonet; Jordi Levy; Felip Manyà (2007). Inference Rules for High-Order Consistency in Weighted CSP. Proc. of the 22th AAAI Conference on Artificial Intelligence. pp. 167-172. AAAI Press. [PDF]
María Luisa Bonet; Jordi Levy; Felip Manyà (2006). A Complete Calculus for Max-SAT. Proc. of the 9th International Conference on Theory and Applications of Satisfiability Testing, SAT'06. Lecture Notes in Computer Science, Vol. 4121, pp. 240-251. Springer-Verlag. [PDF]
Jordi Levy; Manfred Schmidt-Schauss; Mateu Villaret (2006). Bounded Second-Order Unification Is NP-Complete. Proc. of the 17th International Conference on Rewriting Techniques and Applications, RTA'06. Lecture Notes in Computer Science, Vol. 4098, pp. 400-414. Springer-Verlag. [PDF]
Jordi Levy; Manfred Schmidt-Schauss; Mateu Villaret (2006). Stratified Context Unification is NP-complete. Proc. of the 3rd International Joint Conference on Automated Reasoning, IJCAR'06. Lecture Notes in Computer Science, Vol. 4130, pp. 82-96. Springer-Verlag. [PDF]
Jordi Levy; Joachim Niehren (2005). Well-Nested Context Unification. Proc. of the 20th International Conference on Automated Deduction, CADE-20. Lecture Notes in Artificial Intelligence, Vol. 3632, pp. 149-163. Springer-Verlag. [PDF]
Jordi Levy; Manfred Schmidt-Schauss; Mateu Villaret (2004). Monadic Second-Order Unifications is NP Complete. Proc. of the 15th International Conference on Rewriting Techniques and Applications, RTA'04. Lecture Notes in Computer Science, Vol. 3091, pp. 55-69. Springer-Verlag. [PDF]
Atserias, Albert; María Luisa Bonet; Jordi Levy (2003). On chvátal rank and cutting planes proofs. Electronic Colloquium on Computational Complexity, Vol. 41, Num. Report TR03-041, pp. 12. [PDF]
Jordi Levy; Mateu Villaret (2002). Currying Second-Order Unification Problems. Proc. of the 13th International Conference on Rewriting Techniques and Applications, RTA'02. Lecture Notes in Computer Science, Vol. 2378, pp. 326-339. Springer-Verlag. [PDF]
Jordi Levy; Mateu Villaret (2001). Context unification and Traversal Equations. Proc. of the 12th International Conference on Rewriting Techniques and Applications, RTA'01. Lecture Notes in Computer Science, Vol. 2051, pp. 169-184. Springer-Verlag. [PDF]
Jordi Levy; Mateu Villaret (2000). Linear Second-Order Unification and Context Unification with Tree-Regular Constraints. Proc. of the 11th Int. Conf. on Rewriting Techniques and Applications, RTA'00. Lecture Notes in Computer Science, Vol. 1833, pp. 156-171. Springer-Verlag. [PDF]
Jordi Levy; Margus Veanes (2000). On the Undecidability of Second-Order Unification. Information and Computation, Vol. 159, Num. 1-2, pp. 125-150. [PDF]
Jordi Levy; Margus Veanes (1998). On Unification Problems in Restricted Second-Order Languages. Annual Conference of the European Association for Computer Science Logic, CSL'98. [PDF]
Jordi Levy (1998). Decidable and Undecidable Second-Order Unification Problems. Proc. of the 9th International Conference on Rewriting Techniques and Applications, RTA'98. Lecture Notes in Computer Science, Vol. 1379, pp. 47-60. Springer-Verlag. [PDF]
Jordi Levy; Jaume Agustí-Cullell (1996). Bi-rewrite Systems. Journal of Symbolic Computation, Vol. 22, Num. 3, pp. 279-314. [PDF]
Jordi Levy (1996). Linear Second Order Unification. Proc. of the 7th International Conference on Rewriting Techniques and Applications, RTA'96. Lecture Notes in Computer Science, Vol. 1103, pp. 332-346. Springer-Verlag. [PDF]
David Robertson; Jaume Agustí-Cullell; Jane Hesketh; Jordi Levy (1994). Expressing Program Requirements using Refinement Lattices. Fundamenta Informaticae, Vol. 21, Num. 3, pp. 163-182. [PDF]
Jordi Levy (1994). The Calculus of Refinements, a Formal Specification Model Based on Inclusions. Doctoral Thesis. Universitat Politècnica de Catalunya. [PDF]
David Robertson; Jaume Agustí-Cullell; Jane Hesketh; Jordi Levy (1993). Expressing Program Requirements using Refinement Lattices. Proc. of the 7th Int. Symp. on Metodologies for Intelligent Systems, ISMIS'93. Lecture Notes in Artificial Intelligence, Vol. 689, pp. 245-254. Springer-Verlag. [PDF]
Jordi Levy; Jaume Agustí-Cullell (1993). Bi-rewriting, a Term Rewriting Technique for Monotonic Order Relations. Proc. of the 5th Int. Conf. on Rewriting Techniques and Applications, RTA'93. Lecture Notes in Computer Science, Vol. 690, pp. 17-31. Springer-Verlag. [PDF]
Jordi Levy; Jaume Agustí-Cullell (1992). Implementing Inequality and Nondeterministic Specifications with Bi-rewriting Systems. Proc. of the 4th Int. Workshop on Recent Trends in Data Type Specification, COMPASS'92. Lecture Notes in Computer Science, Vol. 785, pp. 252-267. Springer-Verlag. [PDF]