4 papers
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…
On Grid Graph Reachability and Puzzle Games
Miquel Bofill, Cristina Borralleras, Joan Espasa +1
Many puzzle video games, like Sokoban, involve moving some agent in a maze. The reachable locations are usually apparent for a human player, and the difficulty of the game is mainl…
Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers
Cristina Borralleras, Daniel Larraz, Albert Oliveras +2
We present new methods for solving the Satisfiability Modulo Theories problem over the theory of Quantifier-Free Non-linear Integer Arithmetic, SMT(QF-NIA), which consists in decid…
Resource Analysis driven by (Conditional) Termination Proofs
Elvira Albert, Miquel Bofill, Cristina Borralleras +2
When programs feature a complex control flow, existing techniques for resource analysis produce cost relation systems (CRS) whose cost functions retain the complex flow of the prog…