Jordi Levy Diaz

Jordi Levy's research has always revolved around logic. During his doctoral thesis he studied how rewriting, and other techniques to automate first-order logic with equality, can be used to automate deduction in theories with non-reflective and transitive relationships, such as inclusion.

Later, Jordi worked on higher-order logics. Focused on the unification problem, he analyzed restrictions in the number of variables, occurrences and arity, that may make the problem decidable, as well as on the proposal of some variants as Context and Bounded Second-Order Unification.

In recent years, he has been interested in real-world problems encoded in propositional logic. In the case of MaxSAT, he contributed to set the bases of the SAT-based MaxSAT method, where we solve optimization problems through successive calls to a SAT solver.

In the case of SAT, by encoding the problems using bipartite variable-clause graphs, Jordi analyzed the structure of the industrial problems discovering that these problems have a scale-free graph structure and show how modern SAT solvers exploit this structure. He has also analyzed the modular structure and the fractal dimension of these problems and proposed new models of random SAT formulas that reproduce the characteristics of real-world formulas.

Currently, Jordi is a permanent Researcher at the Artificial Intelligence Research Institute (IIIA) of the Spanish Research Council (CSIC).