report1/intro.tex

   1 \section{Introduction}
   2 During the initial discussion, we came to two ideas of possible NuSMV encoding of a sokoban solver: an object-centered approach and a coordinate-based one. According to our hypothesis, neither of them is universally superior. To be more precise, the object-centered solution might be advantageous in case of sokoban fields with fewer boxes, but with bigger empty spaces, whereas the coordinate-based encoding might not be that limited with amounts of boxes, being more limited on the sizes of fields. The following hypothesis motivated us to try both approaches and conduct benchmarks wich can help us building a more versatile hybrid solution later. For both approaches, fully automated model generators were made.