\myheading{Kangaroo: Optimizing production of a cardboard toy using SAT-solver}

\renewcommand{\CURPATH}{other/tiling/kangaroo}

This is a do-it-yourself toy kangaroo I once bought, made of cardboard parts:

\begin{figure}[H]
\centering
\begin{subfigure}{.5\textwidth}
  \centering
  \includegraphics[width=0.9\linewidth]{\CURPATH/3.jpg}
  \caption{Final view}
\end{subfigure}%
\begin{subfigure}{.5\textwidth}
  \centering
  \includegraphics[width=0.9\linewidth]{\CURPATH/2.jpg}
  \caption{Assembly guide}
\end{subfigure}
\end{figure}


\clearpage
All parts came in 3 plates:

\begin{figure}[H]
\centering
\begin{subfigure}{.5\textwidth}
  \centering
  \includegraphics[width=0.9\linewidth]{\CURPATH/1.jpg}
  \caption{A guide}
\end{subfigure}%
\begin{subfigure}{.5\textwidth}
  \centering
  \includegraphics[width=0.9\linewidth]{\CURPATH/4.jpg}
  \caption{3 cardboards}
\end{subfigure}
\end{figure}

Now the question: can we put all the parts needed on smaller plates?
To save some cardboard material?

\clearpage
I \textit{digitized} all parts using usual notebook:

\begin{figure}[H]
\centering
\includegraphics[width=0.5\linewidth]{\CURPATH/digitized-25.jpg}
\end{figure}

\begin{figure}[H]
\centering
\begin{subfigure}{.25\textwidth}
  \centering
  \includegraphics[width=0.9\linewidth]{\CURPATH/digitized-20-24.jpg}
\end{subfigure}%
\begin{subfigure}{.25\textwidth}
  \centering
  \includegraphics[width=0.9\linewidth]{\CURPATH/digitized-36.jpg}
\end{subfigure}%
\begin{subfigure}{.25\textwidth}
  \centering
  \includegraphics[width=0.9\linewidth]{\CURPATH/digitized-26.jpg}
\end{subfigure}%
\begin{subfigure}{.25\textwidth}
  \centering
  \includegraphics[width=0.9\linewidth]{\CURPATH/digitized-35.jpg}
\end{subfigure}
\end{figure}

I don't know a real size of a square in notebook, probably, ~5mm.
I would call it \textit{one [square] unit}.

Then I took the same piece of Python code I used before: \ref{tiling_SAT}.

It was easy: there are just (a big) pack of Boolean variables and AMO1/ALO1 constraints,
or, as I called them before, POPCNT1.

Thanks to parallelized Plingeling SAT-solver, I could
find a solution for a 43*34 [units] plate in ~10 minutes\footnote{4 threads on Intel Xeon CPU E3-1270 v3 @ 3.50GHz}:

\begin{figure}[H]
\centering
\includegraphics[width=0.7\linewidth]{\CURPATH/1plate.png}
\caption{All parts on a single 43*34 plate}
\end{figure}

Probably this is smallest plate possible. When I try smaller dimensions, SAT solver stuck.
But if you wish, you can decrease dimensions and run it again and again...

Now the question: the toy factory wants to ship all parts in several (smaller) plates.
Like, 3 of them.
Because one plate is impractical for shipping, handling, etc.

To put all parts on 3 plates, I can just add 2 borders between them:

\begin{lstlisting}[style=custompy]
board=["*"*BOARD_SMALL_WIDTH + " " + "*"*BOARD_SMALL_WIDTH + " " + "*"*BOARD_SMALL_WIDTH]*BOARD_SMALL_HEIGHT
\end{lstlisting}

Smallest (3) plates I found: 19*27 [units]:

\begin{figure}[H]
\centering
\includegraphics[width=\linewidth]{\CURPATH/3plates.png}
\caption{All parts on a three 19*27 plates}
\end{figure}

This is slightly better than what was produced by the toy factory (20*30 [units], as measured by my notebook).

Now you can see there are two $2 \cdot 1$ notches at each \textit{plate}:

\begin{figure}[H]
\centering
\includegraphics[width=\linewidth]{\CURPATH/5.jpg}
\caption{Note notches: upper left and bottom left}
\end{figure}

I don't know why they been cut. Probably for easier stacking at factory? Who knows.
Anyway, I think I can add this constraint to my solver.
These are 3 initial plates:

\begin{lstlisting}[style=custompy]
board=["*****************   *****************   *****************  ",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       " ******************  ******************  ******************",
       " ******************  ******************  ******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************",
       "******************* ******************* *******************"]
\end{lstlisting}

\begin{figure}[H]
\centering
\includegraphics[width=\linewidth]{\CURPATH/3plates_notches.png}
\caption{All parts on a three 19*27 plates with notches}
\end{figure}

Keep in mind, how coarse my \textit{units} are (~5mm).
You can \textit{digitize} better if you use a
millimeter paper\footnote{\url{https://en.wikipedia.org/wiki/Graph_paper}}, but such a problem
would be more hard for SAT solver, of course.

What I also did: this problem required huge AMO1/ALO1 constraints (several thousands
Boolean variables).
Naive quadratic encoding can't manage this, also, CNF instances growing greatly.

I used \textit{commander} encoding this time.
For example, you need to add AMO1/ALO1 constraint to 100 variables.
Divide them by 10 parts.
Add naive/quadratic AMO1/ALO1 for each of these 10 parts.
Add \textit{OR} for each parts.
Then you get 10 \textit{OR result}.
Each \textit{OR result} is a \textit{commander}, like, a commander of a squad.
Join them together with quadratic AMO1/ALO1 constraint again.

I do this recursively, so it looks like a multi-tiered tree of \textit{commanders}.
Also, changing these constants (5 and 10) influences SAT solver's performance significantly,
probably, tuning is required for each type of task...

(The constants defines breadth and depth of a tree.)

\begin{lstlisting}[style=custompy]
    # naive/pairwise/quadratic encoding
    def AtMost1_pairwise(self, lst:List[str]):
        for pair in itertools.combinations(lst, r=2):
            self.add_clause([self.neg(pair[0]), self.neg(pair[1])])

    # "commander" (?) encoding
    def AtMost1_commander(self, lst:List[str]) -> str:
        parts=my_utils.partition(lst, 5)
        c=[] # type: List[str]
        for part in parts:
            if len(part)<10:
                self.AtMost1_pairwise(part)
                c.append(self.OR_list(part))
            else:
                c.append(self.AtMost1_commander(part))
        self.AtMost1_pairwise(c)
        return self.OR_list(c)

    def AtMost1(self, lst:List[str]):
        if len(lst)<=10:
            self.AtMost1_pairwise(lst)
        else:
            self.AtMost1_commander(lst)

    # previously named POPCNT1 
    # make one-hot (AKA unitary) variable
    def make_one_hot(self, lst:List[str]):
        self.AtMost1(lst)
        self.OR_always(lst)
\end{lstlisting}
( \url{\RepoURL/libs/SAT_lib.py} )

The files: \url{\RepoURL/\CURPATH}.