29 citations · 64 across the 9 of their papers we have counts for
9 papers
SAT-IT: an Online Interactive SAT Tracer
Wilber Bermeo, Jordi Coll, Pau Ferrer +1
Modern Boolean Satisfiability (SAT) solvers, based on the Conflict-Driven Clause Learning (CDCL) paradigm, achieve state-of-the-art efficiency but present a steep learning curve du…
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…
A Good Snowman is Hard to Plan
Miquel Bofill, Cristina Borralleras, Joan Espasa +3
In this work we face a challenging puzzle video game: A Good Snowman is Hard to Build. The objective of the game is to build snowmen by moving and stacking snowballs on a discrete…
Challenges in Modelling and Solving Plotting with PDDL
Joan Espasa, Ian Miguel, Peter Nightingale +2
We study a planning problem based on Plotting, a tile-matching puzzle video game published by Taito in 1989. The objective of this game is to remove a target number of coloured blo…
A Preliminary Case Study of Planning With Complex Transitions: Plotting
Jordi Coll, Joan Espasa, Ian Miguel +1
Plotting is a tile-matching puzzle video game published by Taito in 1989. Its objective is to reduce a given grid of coloured blocks down to a goal number or fewer. This is achieve…
SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints
Miquel Bofill, Jordi Coll, Peter Nightingale +3
When solving a combinatorial problem using propositional satisfiability (SAT), the encoding of the problem is of vital importance. We study encodings of Pseudo-Boolean (PB) constra…
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…
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…
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…