Automatsko rešavanje igre Sokoban pomoću veštačke inteligencije

Abstract

Igra Sokoban je pomerajuća slagalica u kojoj igrač, čuvar skladišta, pomera kutije po tabli za igru, u cilju njihovog postavljanja na unapred zadata mesta. Pored toga što je zanimljiva za ručno rešavanje, ova igra inspiriše mnoge istraživače da se bave efikasnom automatizacijom njenog rešavanja, s obzirom na izuzetno veliku algoritamsku složenost ovog problema. U ovom radu, prikazujemo novi pristup zasnovan na automatskom planiranju uz pomoć procedura za ispitivanje zadovoljivosti u odnosu na teorije prvog reda, poznatih i kao SMT rešavači.

The game of Sokoban is a sliding puzzle where a player, a warehouse keeper, pushes a number of boxes over the game board, in order to place them on the particular fields, given in advance. Besides the interest for manual solving, the game also attracts a great attention of the researchers to work on efficent automatization of its solving, because of the great algorithm complexity of the problem. In this paper, we propose a novel approach based on automated planning using procedures for checking satisfiability modulo first order theories, known as SMT solvers.