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.