\section{Introduction}
During the initial discussion, we came to two ideas of possible \textsc{NuSMV}
encoding of a \emph{sokoban} solver: an object-centered approach and a
coordinate-based one. We hypothesized that neither of them is universally
superior. To be more precise, the object-centered solution might be
advantageous in case of \emph{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 which can
help us building a more versatile hybrid solution later. For both approaches,
fully automated model generators were made.
