Logic-based encodings for ricochet robots

Abstract

Studying the performance of logic tools on solving a specific problem can bring new insights on the use of different paradigms. This paper provides an empirical evaluation of logic-based encodings for a well known board game: Ricochet Robots. Ricochet Robots is a board game where the goal is to find the smallest number of moves needed for one robot to move from the initial position to a target position, while taking into account the existing barriers and other robots. Finding a solution to the Ricochet Robots problem is NP-hard. In this work we develop logic-based encodings for the Ricochet Robots problem to feed into Boolean Satisfiability (SAT) solvers. When appropriate, advanced techniques are applied to further boost the performance of a solver. A comparison between the performance of SAT solvers and an existing ASP solution clearly shows that SAT is by far the more adequate technology to solve the Ricochet Robots problem.