Implementing Inequality and Non-Deterministic Specifications with Bi-Rewriting Systems. - Jordi Levy; Jaume Agustí-Cullell (COMPASS/ADT, 1992)

Bi-rewriting, a Term Rewriting Technique for Monotonic Order Relations. - Jordi Levy; Jaume Agustí-Cullell (RTA, 1993)

Expressing Program Requirements Using Refinement Lattices. - David Stuart Robertson 001; Jaume Agustí-Cullell; Jane Hesketh; Jordi Levy (Fundam. Informaticae, 1994)

A Decidable Second-Order Unification Problem. - Jordi Levy (UNIF, 1995)

Linear Second-Order Unification. - Jordi Levy (RTA, 1996)

Bi-Rewrite Systems. - Jordi Levy; Jaume Agustí-Cullell (J. Symb. Comput., 1996)

Decidable and Undecidable Second-Order Unification Problems. - Jordi Levy (RTA, 1998)

Linear Second-Order Unification and Context Unification with Tree-Regular Constraints. - Jordi Levy; Mateu Villaret (RTA, 2000)

On the Undecidability of Second-Order Unification. - Jordi Levy; Margus Veanes (Inf. Comput., 2000)

Context Unification and Traversal Equations. - Jordi Levy; Mateu Villaret (RTA, 2001)

Currying Second-Order Unification Problems. - Jordi Levy; Mateu Villaret (RTA, 2002)

On Chvatal Rank and Cutting Planes Proofs - Albert Atserias; Maria Luisa Bonet; Jordi Levy (Electron. Colloquium Comput. Complex., 2003)

Monadic Second-Order Unification Is NP-Complete. - Jordi Levy; Manfred Schmidt-Schauß; Mateu Villaret (RTA, 2004)

Well-Nested Context Unification. - Jordi Levy; Joachim Niehren; Mateu Villaret (CADE, 2005)

Stratified Context Unification Is NP-Complete. - Jordi Levy; Manfred Schmidt-Schauß; Mateu Villaret (IJCAR, 2006)

Bounded Second-Order Unification Is NP-Complete. - Jordi Levy; Manfred Schmidt-Schauß; Mateu Villaret (RTA, 2006)

A Complete Calculus for Max-SAT. - Maria Luisa Bonet; Jordi Levy; Felip Manyà (SAT, 2006)

Inference Rules for High-Order Consistency in Weighted CSP. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy; Felip Manyà (AAAI, 2007)

What Is a Real-World SAT Instance? - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy; Felip Manyà (CCIA, 2007)

The Logic Behind Weighted CSP. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy; Felip Manyà (IJCAI, 2007)

A Complete Resolution Calculus for Signed Max-SAT. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy; Felip Manyà (ISMVL, 2007)

Sequence Unification Through Currying. - Temur Kutsia; Jordi Levy; Mateu Villaret (RTA, 2007)

Mapping CSP into Many-Valued SAT. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy; Felip Manyà (SAT, 2007)

Resolution for Max-SAT. - Maria Luisa Bonet; Jordi Levy; Felip Manyà (Artif. Intell., 2007)

Measuring the Hardness of SAT Instances. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy; Felip Manyà (AAAI, 2008)

Random SAT Instances à la Carte. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (CCIA, 2008)

The Complexity of Monadic Second-Order Unification. - Jordi Levy; Manfred Schmidt-Schauß; Mateu Villaret (SIAM J. Comput., 2008)

On Solving MaxSAT Through SAT. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (CCIA, 2009)

On the Structure of Industrial SAT Instances. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (CP, 2009)

Towards Industrial-Like Random SAT Instances. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (IJCAI, 2009)

Solving (Weighted) Partial MaxSAT through Satisfiability Testing. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (SAT, 2009)

Simplifying the signature in second-order unification. - Jordi Levy; Mateu Villaret (Appl. Algebra Eng. Commun. Comput., 2009)

A New Algorithm for Weighted Partial MaxSAT. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (AAAI, 2010)

An Efficient Nominal Unification Algorithm. - Jordi Levy; Mateu Villaret (RTA, 2010)

On the relation between Context and Sequence Unification. - Temur Kutsia; Jordi Levy; Mateu Villaret (J. Symb. Comput., 2010)

On the Modularity of Industrial SAT Instances. - Carlos Ansótegui; Jordi Levy (CCIA, 2011)

On the complexity of Bounded Second-Order Unification and Stratified Context Unification. - Jordi Levy; Manfred Schmidt-Schauß; Mateu Villaret (Log. J. IGPL, 2011)

Analysis and Generation of Pseudo-Industrial MaxSAT Instances. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy; Chu Min Li 001 (CCIA, 2012)

Improving SAT-Based Weighted MaxSAT Solvers. - Carlos Ansótegui; Maria Luisa Bonet; Joel Gabàs; Jordi Levy (CP, 2012)

The Community Structure of SAT Formulas. - Carlos Ansótegui; Jesús Giráldez-Cru; Jordi Levy (SAT, 2012)

Nominal Unification from a Higher-Order Perspective. - Jordi Levy; Mateu Villaret (ACM Trans. Comput. Log., 2012)

Improving WPM2 for (Weighted) Partial MaxSAT. - Carlos Ansótegui; Maria Luisa Bonet; Joel Gabàs; Jordi Levy (CP, 2013)

A Variant of Higher-Order Anti-Unification. - Alexander Baumgartner; Temur Kutsia; Jordi Levy; Mateu Villaret (RTA, 2013)

SAT-based MaxSAT algorithms. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (Artif. Intell., 2013)

Resolution procedures for multiple-valued optimization. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy; Felip Manyà (Inf. Sci., 2013)

The Fractal Dimension of SAT Formulas. - Carlos Ansótegui; Maria Luisa Bonet; Jesús Giráldez-Cru; Jordi Levy (IJCAR, 2014)

Nominal Anti-Unification. - Alexander Baumgartner; Temur Kutsia; Jordi Levy; Mateu Villaret (UNIF, 2014)

On the Limits of Second-Order Unification. - Jordi Levy (UNIF, 2014)

Anti-unification for Unranked Terms and Hedges. - Temur Kutsia; Jordi Levy; Mateu Villaret (J. Autom. Reason., 2014)

On the Classification of Industrial SAT Families. - Carlos Ansótegui; Maria Luisa Bonet; Jesús Giráldez-Cru; Jordi Levy (CCIA, 2015)

A Modularity-Based Random SAT Instances Generator. - Jesús Giráldez-Cru; Jordi Levy (IJCAI, 2015)

Using Community Structure to Detect Relevant Learnt Clauses. - Carlos Ansótegui; Jesús Giráldez-Cru; Jordi Levy; Laurent Simon 001 (SAT, 2015)

Nominal Unification of Higher Order Expressions with Recursive Let. - Manfred Schmidt-Schauß; Temur Kutsia; Jordi Levy; Mateu Villaret (LOPSTR, 2016)

Generating SAT instances with community structure. - Jesús Giráldez-Cru; Jordi Levy (Artif. Intell., 2016)

Community Structure in Industrial SAT Instances. - Carlos Ansótegui; Maria Luisa Bonet; Jesús Giráldez-Cru; Jordi Levy (CoRR, 2016)

Exploiting subproblem optimization in SAT-based MaxSAT algorithms. - Carlos Ansótegui; Joel Gabàs; Jordi Levy (J. Heuristics, 2016)

Locality in Random SAT Instances. - Jesús Giráldez-Cru; Jordi Levy (IJCAI, 2017)

Percolation and Phase Transition in SAT. - Jordi Levy (CoRR, 2017)

Structure features for SAT instances classification. - Carlos Ansótegui; Maria Luisa Bonet; Jesús Giráldez-Cru; Jordi Levy (J. Appl. Log., 2017)

Higher-Order Pattern Anti-Unification in Linear Time. - Alexander Baumgartner; Temur Kutsia; Jordi Levy; Mateu Villaret (J. Autom. Reason., 2017)

Term-Graph Anti-Unification. - Alexander Baumgartner; Temur Kutsia; Jordi Levy; Mateu Villaret (FSCD, 2018)

Phase Transition in Realistic Random SAT Models. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (CCIA, 2019)

Community Structure in Industrial SAT Instances. - Carlos Ansótegui; Maria Luisa Bonet; Jesús Giráldez-Cru; Jordi Levy; Laurent Simon 001 (J. Artif. Intell. Res., 2019)

Equivalence Between Systems Stronger Than Resolution. - Maria Luisa Bonet; Jordi Levy (SAT, 2020)

A Heuristic Algorithm for Multi-Agent Vehicle Routing with Automated Negotiation. - Dave de Jonge; Filippo Bistaffa; Jordi Levy (AAMAS, 2021)

Reducing SAT to Max2SAT. - Carlos Ansótegui; Jordi Levy (IJCAI, 2021)

Popularity-similarity random SAT formulas. - Jesús Giráldez-Cru; Jordi Levy (Artif. Intell., 2021)

Yet Another (Fake) Proof of P=NP. - Carlos Ansótegui; Jordi Levy (CCIA, 2022)

Scale-Free Random SAT Instances. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (Algorithms, 2022)

Multi-objective vehicle routing with automated negotiation. - Dave de Jonge; Filippo Bistaffa; Jordi Levy (Appl. Intell., 2022)

Reducing SAT to Max2XOR. - Carlos Ansótegui; Jordi Levy (CoRR, 2022)

Nominal Unification and Matching of Higher Order Expressions with Recursive Let. - Manfred Schmidt-Schauß; Temur Kutsia; Jordi Levy; Mateu Villaret; Yunus D. K. Kutz (Fundam. Informaticae, 2022)

On the Density of States of Boolean Formulas. - Carlos Ansótegui; Maria Luisa Bonet; Jordi Levy (CCIA, 2023)

General Boolean Formula Minimization with QBF Solvers. - Eduardo Calò; Jordi Levy (CCIA, 2023)

Polynomial Calculus for MaxSAT. - Ilario Bonacina; Maria Luisa Bonet; Jordi Levy (SAT, 2023)

Is Shortest Always Best? The Role of Brevity in Logic-to-Text Generation. - Eduardo Calò; Jordi Levy; Albert Gatt; Kees van Deemter (*SEM@ACL, 2023)

The impact of heterogeneity and geometry on the proof complexity of random satisfiability. - Thomas Bläsius; Tobias Friedrich 001; Andreas Göbel 001; Jordi Levy; Ralf Rothenberger (Random Struct. Algorithms, 2023)

Implementing 3-SAT Gadgets for Quantum Annealers with Random Instances. - Pol Rodríguez-Farrés; Rocco Ballester; Carlos Ansótegui; Jordi Levy; Jesús Cerquides (ICCS (6), 2024)

Weighted, Circular and Semi-Algebraic Proofs (Abstract Reprint). - Ilario Bonacina; Maria Luisa Bonet; Jordi Levy (IJCAI, 2024)

Polynomial calculus for optimization. - Ilario Bonacina; Maria Luisa Bonet; Jordi Levy (Artif. Intell., 2024)

SAT, Gadgets, Max2XOR, and Quantum Annealers. - Carlos Ansótegui; Jordi Levy (CoRR, 2024)

Weighted, Circular and Semi-Algebraic Proofs. - Ilario Bonacina; Maria Luisa Bonet; Jordi Levy (J. Artif. Intell. Res., 2024)

An Algebraic Approach to MaxCSP. - Ilario Bonacina; Jordi Levy (SAT, 2025)