## Appendix A Satisfiability Problem (SAT) Approach  
If a tiling problem is formulated in the ILP format, assume there are \(m\) equations labeled \(E_{1}\) through \(E_{m}\), each corresponding to a cell in the target region to be covered, and \(k\) equations, labeled \(T_{1}\) through \(T_{k}\), each specifying the number of times we use a particular tile. Assume there are \(n\) variables, each associated with a placement of a particular tile in the region. This results in a (typically sparse) linear system of size \((m+k)\times n\), to which we must impose the additional constraints that the entries of the solution \(x\) are binary.  
From a satisfiability problem (SAT) standpoint, the variables \(x\) are Boolean, so this constraint is automatically imposed. Each covering equation becomes a clause, joined by AND operators (\(\cap\)) in a single Boolean formula, whose first part is as follows:  
\[(E_{1}\cap E_{2}\cap\cdots\cap E_{m}\cap\cdots).\]  
For example, if a covering equation \(E_{1}\) had the form:  
\[x_{1}+x_{3}+x_{7}+x_{9}=1,\]  
then the corresponding Boolean clause combines these variables using the OR operator (\(\cup\)) is as follows:  
\[(x_{1}\cup x_{3}\cup x_{7}\cup x_{9}).\]  
In fact, if the Boolean statement \((E_{1}\cap E_{2}\cap\cdots\cap E_{m})\) is true, then we have guaranteed that we have covered all the cells in the region. However, in fact, SAT seeks _any and all_ values of the variables that make the statement true; one such value has all the variables true, resulting in all the cells being covered, but many times. The correct formulation of the problem must impose the additional constraint that each tile can only be used a certain number of times, which guarantees that any solution will cover each cell exactly once. Thus, it is crucial to specify the number of times we use each tile.  
If for a given tile, this limit is 1, then we could replace each \(\cup\) in the Boolean clause by an exclusive OR operator, and we would be done. However, SAT has no exclusive OR operator. Moreover, this idea would fail if the limit was greater than 1.  
Thus, for each tile, we need to impose a corresponding count constraint within the limited grammar allowed by SAT. If a tile count constraint is 1, and the tile has 100 possible placements in the region, this means we need to attach 100 clauses to the SAT formula for this single tile. Suppose we represent these tile placements by the variables \(x_{1}\) through \(x_{100}\), these clauses become:  
\[(x_{1}\cup\
eg x_{2}\cup\cdots\cup\
eg x_{99}\cup\
eg x_{100})\cap(\
eg x_{1} \cup x_{2}\cup\
eg x_{3}\cup\cdots\cup\
eg x_{100})\cap\cdots\] \[\cap(\
eg x_{1}\cup\
eg x_{2}\cup\cdots\cup\
eg x_{99}\cup x_{100}).\]  
Of course, we will need to add such a string of clauses for every single tile. However, if a tile with 100 configurations has a larger count constraint, say 2, then we need to write \({100\choose 2}\) such clauses and append these to our Boolean sentence. Things grow radically worse as the constraint and tile placement counts grow. In some of our problems, the number of tile placements of a single tile may run into the thousands, and the number of count constraints may be in the hundreds.  
Thus, the SAT formulation of our problem would only be suitable for problems of very restricted size, and much smaller than we can handle using the ILP approach.