\myheading{Tiling puzzle (SAT)}
\label{tiling_SAT}

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

This is the same problem, rewritten to be used with SAT solver.

This is different solution: it uses exact cover problem solver which function is in \verb|SAT_lib.py|.
(It is better to \emph{offload} it to library.)

The exact cover problem is also used in another example: ``Mutually orthogonal Latin squares: finding via transversals'': \ref{MOLS_transv}.

What is also different: now a polyomino can be reused many times.
(This is configurable.)

Also, the \emph{mutilated chessboard problem}\footnote{\url{https://en.wikipedia.org/wiki/Mutilated_chessboard_problem}} can be proven.
Of course, no solution would be produced.
But SAT solver can produce a proof.
Resulting CNF file is very compact: 346 clauses, 110 variables.
(This is an exact cover problem, of course.)
If Kissat is used, the proof file size is only 14KiB.

The source code: \url{\RepoURL/\CURPATH/tiling.py}.