report1/intro.tex

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