29 citations · 78 across the 10 of their papers we have counts for
10 papers
Nominal anti-unification
Alexander Baumgartner, Temur Kutsia, Jordi Levy +1
We study nominal anti-unification, which is concerned with computing least general generalizations for given terms-in-context. In general, the problem does not have a least general…
General Boolean Formula Minimization with QBF Solvers
Eduardo Calò, Jordi Levy
The minimization of propositional formulae is a classical problem in logic, whose first algorithms date back at least to the 1950s with the works of Quine and Karnaugh. Most previo…
Reducing SAT to Max2XOR
Carlos Ansótegui, Jordi Levy
Representing some problems with XOR clauses (parity constraints) can allow to apply more efficient reasoning techniques. In this paper, we present a gadget for translating SAT clau…
Nominal Unification and Matching of Higher Order Expressions with Recursive Let
Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy +2
A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in nondeterministic polynomial time. We also…
The Impact of Heterogeneity and Geometry on the Proof Complexity of Random Satisfiability
Thomas Bläsius, Tobias Friedrich, Andreas Göbel +2
Satisfiability is considered the canonical NP-complete problem and is used as a starting point for hardness reductions in theory, while in practice heuristic SAT solving algorithms…
Scale-Free Random SAT Instances
Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy
We focus on the random generation of SAT instances that have properties similar to real-world instances. It is known that many industrial instances, even with a great number of var…
Nominal Unification of Higher Order Expressions with Recursive Let
Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy +1
A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in non-deterministic polynomial time. We also…
Community Structure in Industrial SAT Instances
Carlos Ansótegui, Maria Luisa Bonet, Jesús Giráldez-Cru +2
Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been developed after an intensive experimental process. It is…
The Fractal Dimension of SAT Formulas
C. Ansótegui, M. L. Bonet, J. Giráldez-Cru +1
Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been developed after an intensive experimental testing proces…
Nominal Unification from a Higher-Order Perspective
Jordi Levy, Mateu Villaret
Nominal Logic is a version of first-order logic with equality, name-binding, renaming via name-swapping and freshness of names. Contrarily to higher-order logic, bindable names, ca…