Note: This is a continuation and revision of my other answer.
Problems with the reduction
Recall the decision problem:
Is there a perfect tiling covering a given a $(n+1) \times (n+2)$ grid with $n$ unique tiles?
So for an $(n+1) \times (n+2)$ grid, we can only use $n$ variables.
But:
- Our reduction requires a lot of unique variables, much more than $\mathcal O(n)$.
- Furthermore, our wires are open ended, which leads to:
- How do we know we can tile the open areas?
To solve the first problem, we artificially make the game-board much larger; essentially we make $n$ equal to the number of variables we actually require, then create a grid of size $(n+1)\times(n+2)$, and place our grid in the lower left corner. This will lead to a quadratic blowup.
For the second problem, we must rethink our gadgets a bit.
It can seem a little daunting to prove that we can successfully tile the rest of the board according to the rule. So we start off with the same strategy one would use to actually generate game-boards of size $(n+1)\times(n+2)$:
First we generate a set of all possible tiles. All of these tiles will have to be placed on the board. Then we remove the tiles, and leave behind their squares.
However, our gadgets don't guarantee a particular set of tiles will be placed; the tiles placed depend on the state. So we must carefully modify the gadgets to guarantee particular tiles will be removed, no matter which state is chosen.
Let's go over our gadgets then.
The wire and clause-gate are problematic for two reasons.
- We don't know that the squares surrounding a wire or clause-gate can be tiled correctly; after all, some wires can be pushed to the left, others to the right, and tiling the remaining white-space squares becomes non-trivial. We'll refer to this problem as the "flow" problem.
- There is no way of knowing which tiles to remove from the tile-set; in one state, one set of squares, in the wire or clause-gate, will be tiled, in another state, an entirely different set of squares will be tiled.
To solve these issues:
- First, we generate a set of all possible tiles. All of these tiles will have to be placed on the board; as we place them on the board, we will remove the tile from the set. Though we might not at first know $n$, since we have yet to fully describe the formulation, we can add all the new tile possibilities as we increment $n$, as needed. All of the tiles we remove from this set must guaranteed be placeable (at least, be guaranteed to be placeable if the formula is satisfiable). We call removing a tile from the tile-set, to "discharge" the tile from the tile-set, as in to discharge our obligation to place it on the game-board.
- We must carefully design the gadgets to guarantee particular tiles will be removed, no matter which state is chosen.
- We must close our gadgets, so that they don't push tiles all around the board depending on their state; rather all of their states must only take up a particular well defined area.
- Alternatively, all of their states must be guaranteed to be able to take up a well defined area; this guarantees a satisfiable tiling, but does not guarantee that a particular tiling will occur. This is the same way a Dominosa game is made:
- First the tiles are generated into a set;
- Then the tiles are placed down in a random configuration,
- As each tile is placed, it is removed from the tile-set.
- Then the tiles are removed from the board, leaving behind their squares.
- This does not guarantee that the intended configuration will be chosen,
- Rather, it guarantees that the intended configuration is able to be chosen, and thus a solution exists. We can do the same thing here.
- After placing all the gadgets of the formulation, instead of placing unique ${\star}$ squares by default, i.e. on all "whitespace", we make sure the whitespace is a rectangular area with one even dimension, or break down the whitespace into rectangles with one even dimension, and we simply tile the whitespace with the remaining tiles in the tile-set.
- After placing all the tiles from the set, we know everything is placeable.
- Some tiles will be obviously placeable, such as those in walls, others will be placeable only iff the formula is satisfiable, due to the nature of the relationships between the gadgets.
- Then we remove the tiles, and leave behind their squares.
Let's go over our gadgets then.
Forcing gadget
We can make an arbitrary number of building blocks by making sure they each can't be paired with themselves.
For example, let us say we want to force a $\mathbf{({1}{\star},{1}{\star})}$ tile, so that we can use $\mathbf{1}{\star}$ as a building block. (note, ${1}{\star}$ is an arbitrary variable, which we want to force as pair to itself, not necessarily a building block as we used the $1$ value previously)
To guarantee that our $\mathbf {1}{\star}$-building-block reserves $\mathbf{({1}{\star},{1}{\star})}$, we will place it against the bottom wall in the following configuration: we will place the reserved number, let us call it $\mathbf{1}{\star}$ against the wall like an up-tack (shaped like $\bot$); $3$ against the wall, and one in the 2nd row in the middle. Then we will place another two numbers, let us call them ${\mathbf 2}{\star}$ and ${\mathbf 3}{\star}$; these are unique to this gadget. We place these on top of the left and right $\mathbf{1}{\star}$.
Illustrated below, shared black border is the bottom of the game-board, description from left-to-right.
- Configuration of the gadget. Each ${\mathbf 2}{\star}$ and ${\mathbf 3}{\star}$ here are unique to this gadget.
- The 3 possible states of tiling the center $\mathbf{1}{\star}$.

After doing this, we can guarantee that our gadget can be tiled with a specific set of tiles, while guaranteeing that our gadget must force the $\mathbf{({1}{\star},{1}{\star})}$ pair.
- We know that $\mathbf{({1}{\star},{1}{\star})}$ must occur, because all 3 possible tiling states of the lower middle $\mathbf{1}{\star}$, tile as $\mathbf{({1}{\star},{1}{\star})}$, as illustrated in the figure on the right, above.
- The remaining tiles can be tiled as $({1}{\star},{2}{\star})$ and $({1}{\star},{3}{\star})$, covering the gadget. Thus, we can remove those tiles from our global tile-set. Illustrated below.
Description, left to right:
- Left, top: Left state, Left, bottom: A valid tiling of the remaining squares.
- Middle, top: Middle state, Middle, bottom: A valid tiling of the remaining squares.
- Right, top: Right state, Right, bottom: A valid tiling of the remaining squares.

Note, that the tiling of the remaining squares isn't forced, since they can tile with nearby neighbors instead of $\mathbf{1}{\star}$, but since it is a valid tiling of the game-board in all of the states, we can remove them from the tile-set, and assume they will be tiled in exactly that way. Since we know there is a valid possible tiling, we have at least one possible tiling of the game-board, if the formula is satisfiable. Though there is no guarantee that these will be tiled this way, there is a guarantee that the $\mathbf{({1}{\star},{1}{\star})}$ tile will be forced.
Note: if you aren't satisfied with this, or are confused by the difference of "being able to tile" vs. "being forced to tile", you can simply place a wall around the $3\times 2$ gadget, the same way we make a $3\times 2$ wall below for the clause-gadget.
This gadget is not closed, because it doesn't need to be (but you can if you want to). It doesn't need to be, because it has a feasible configuration, which we can remove from the tile-set. Although it might be possible to do a different configuration, this does not affect the satisfiability of the problem.
The following tiles are guaranteed to be to be tiled (thus can be removed from the tile-set): $\mathbf{({1}{\star},{1}{\star})}$
The following tiles are guaranteed to be able to be tiled (thus can be removed from the tile-set): $({1}{\star},{2}{\star}), ({1}{\star},{3}{\star})$
If you choose to close this gadget with a wall, then $({1}{\star},{2}{\star}), ({1}{\star},{3}{\star})$ will also be guaranteed to be covered.
New Wire and Clause gates
Because of the problems of flowing, and the emptying the tile-set, we need to redesign the wire a bit.
One way to solve the flow problem, is to make the wire a circuit, instead of just simple left-right states; that is, it would be circular instead of a line, and therefore if the top part of the circle is pushed right, the bottom will be pushed left. This solves the flow problem.
Following this route, we can change the wire and clause gate to solve both problems.
Reserving $\mathcal T$ and $\mathcal F$
Let us introduce two new universal values, $\mathcal T$ and $\mathcal F$. These two values are universal; actual values in the grid, such as square-values $2$ and $3$ (since by convention, we reserved $1$ as a building block for walls), or whatever you choose. They represent true and false, respectively.
We force-reserve the tiles $(\mathcal T, \mathcal F)$, $(\mathcal T, \mathcal T)$, $(\mathcal F, \mathcal F)$, as follows; illustration below, description from left to right:
- We use the same scheme as forcing any $\mathbf{({1}{\star},{1}{\star})}$ tile, using $\mathcal T$ as $\mathbf{1}{\star}$. Each ${\mathbf 2}{\star}$ and ${\mathbf 3}{\star}$ here are unique to this gadget.
- We use the same scheme as forcing any $\mathbf{({1}{\star},{1}{\star})}$ tile, using $\mathcal F$ as $\mathbf{1}{\star}$ Each ${\mathbf 2}{\star}$ and ${\mathbf 3}{\star}$ here are unique to this gadget.
- We use the same scheme as forcing a $\mathbf{({1}{\star},{1}{\star})}$ tile, using $\mathcal F$ as $\mathbf{1}{\star}$ in the center, and using $\mathcal T$ in the other locations of the up-tack. This forces $(\mathcal F, \mathcal T)$ to tile. ${\mathbf 2}{\star}$ and ${\mathbf 3}{\star}$ are able to tile with $\mathcal T$, so we remove them from the tile-set. Each ${\mathbf 2}{\star}$ and ${\mathbf 3}{\star}$ here are unique to this gadget.

Wire
Each wire will start and end with a value, let us call it ${A}{\star}$, which is unique the to wire. For each clause the wire participates in, the wire will have two wire-values, ${x}{\star}$, and ${x'}{\star}$, which are unique to each wire, and participate in the same clause. Illustration below, with description from left to right.
- A wire that participates in one clause. The wire has a height of $2$, and has a length of $2*p+3$, where $p$ is the number of clauses the wire participates in. The wire is padded by two ${A}{\star}$ squares on the left, and two on the right. It is, of course, surrounded by a wall on all sides, indicated by the blue outline. Note, that the ${1}{\star}$ is unique to this wire, and will only be used in the wire, and the clause it participates in.

Illustrated below are the two states, descriptions from left to right.
- A wire that participates in one clause, in the true state. The wire is considered true, when the ${x}{\star}$ squares are paired with a $\mathcal T$ squares, and the ${x'}{\star}$ squares are paired with $\mathcal F$ squares. It is considered false in the other state, where the tiling is reversed. Note how the tiling is forced once the ${A}{\star}$ tile is selected: $(\mathcal T,\mathcal F)$ are already forced earlier, thus the rest of the tiles must be horizontal.
- The same wire in the false state.

When participating in more clauses, there are more value ${x}{\star}$, and ${x'}{\star}$, one pair for each clause the wire participates in. They alternate being on top and bottom, as does the $\mathcal T$ and $\mathcal F$ squares that separate each ${x}{\star}, {x'}{\star}$ pair.

The two corresponding states.

This gadget is closed, thus there is no "flow problem".
Note how in either state, we collect the following tiles, no matter the state: $({A}{\star},{A}{\star})$, $({A}{\star},\mathcal T)$, $({A}{\star},\mathcal F)$.
There are some tiles however, that we are unsure of; in one state we can remove $({1}{\star}, \mathcal T), ({1'}{\star},\mathcal F), ({2}{\star},\mathcal T), ({2'}{\star},\mathcal F) ...$ from the tile-set, while in another state we can remove $({1}{\star}, \mathcal F), ({1'}{\star},\mathcal T), ({2}{\star},\mathcal F), ({2'}{\star},\mathcal T) ...$ from the tile-set, so which tiles can we actually remove? The answer is: the clause gate has the same problem, but with the opposite set of tiles. It will always collect the remaining, opposite, and uncollected tiles, as we will see in the next section. Since each of these is paired with a clause gate, we will be able to remove them both.
Clause
Next we will create the first iteration of the new clause gate. It consists of a $2\times 3$ gadget, enclosed by walls. Inside the gadget, we place one $\mathcal F$ in the top-center, and two $\mathcal T$ squares in the lower corners; one in the lower-left, and one in the lower-right. The remaining squares will be values representing wire-variables of three different wires. Let us call these ${a}{\star}, {b}{\star},$ and ${c}{\star}$. The $\mathcal F$ will be forced to pair with one of the wire-variables, and the remaining wire-variables will pair with the $\mathcal T$ values. Illustrations below, descriptions from left to right.
- Left: The configuration for the first iteration of the new clause-gate.
- Right The three possible states of the $\mathcal F$ tiling.

These three states leads to three possible tilings. Illustration below, descriptions from left to right.
- Left, top: $\mathcal F$ tiled left, Left, bottom: Tiling the remaining squares.
- Middle, top: $\mathcal F$ tiled right, Middle, bottom: Tiling the remaining squares.
- Right, top: $\mathcal F$ tiled down, Right, bottom: Tiling the remaining squares.

Since the $\mathcal F$ will be paired with one of the wire-variables in the clause, that wire-variable can no longer be paired with $\mathcal F$ in the wire; thus forcing the wire to true. Conversely, the remaining wire-variables that tile with $\mathcal T$ will be forced to tile with $\mathcal F$ within their wires. This is exactly the same constraints as a $\rm 1\text{-in-}3\text{-}S{\small AT}$ clause.
Note, ${a}{\star}, {b}{\star},$ and ${c}{\star}$ are wire-variables, but they could each refer to an ${x}{\star}$ or an ${x'}{\star}$ wire-variable; using an ${x'}{\star}$ is essentially negating the wire-variable.
One addition: to discharge the obligation of knowing which tiles can be removed from the tile-set, we have to "double and contrapositive" the clause. What I mean by this, is to make another $3\times 2$ gadget, with $3$ additional variables representing the negations of ${a}{\star}, {b}{\star},$ and ${c}{\star}$. Let us call these ${a'}{\star}, {b'}{\star},$ and ${c'}{\star}$. These must be the negated variable-wire values of ${a}{\star}, {b}{\star},$ and ${c}{\star}$. This $3\times 2$ gadget is different, in that it will have a $\mathcal T$ at the center, and two $\mathcal F$ values at the corners; exactly the opposite of the clause gadget described thus far. By "doubling" the clause like this, we re-add the same constraints as the gadget described above. However, we also discharge all the combinations of $(\mathcal T, {x}{\star}), (\mathcal T, {x'}{\star}), (\mathcal F, {x}{\star}), (\mathcal F, {x'}{\star})$ from the tile-set, for each variable (and thus for ${a}{\star}, {b}{\star},$ and ${c}{\star}$ as well, because they are after all, wire-variables). Illustrated below, descriptions from left to right.
- A "double and contrapositive" clause. The bottom section is the clause described above; the top section is the newly described contrapositive clause. The new clause has exactly the same logical constraints; it is the contrapositive of the bottom clause. Together, these combined gadgets and the wire discharge all of the combinations of $(\mathcal T, {x}{\star}), (\mathcal F, {x}{\star}), (\mathcal T, {x'}{\star}), (\mathcal F, {x'}{\star})$ from the tile-set, for each wire-variable participating in the clause.
- The blue line in the middle of the left-most figure is there for ease-of-viewing; in reality it can be removed without allowing any more states.

So, let us take an example, to show that all the tiles get discharged as promised. Illustrated below, description from left to right.
- Figure of a wire participating in a single clause; a state is chosen for the clause. Here, we are using ${1}{\star}={b}{\star}$, while ${a}{\star}$ and ${b}{\star}$ are representing other wire-values in this clause.
- For the given state in the clause, the ${1}{\star}$ value is forced to be paired with the neighboring $\mathcal T$.
- This causes the wire to be forced to be true-valued (you can tell as the positive variable of the wire is forced to pair with the $\mathcal T$, and the negative variable is forced to pair with the $\mathcal F$, as explained above).
- This forces the ${1'}{\star}$ in the contrapositive clause (the upper section of the clause) to be paired with $\mathcal T$ within the clause. Now if you look at the wire, every tile within the wire is guaranteed to be discharged: either discharged in the wire itself, or in the corresponding clause-gadget. In this state, we have the tiles, $({A}{\star},{A}{\star})$, $({A}{\star},\mathcal T)$, $({A}{\star},\mathcal F)$, $({1}{\star},\mathcal T)$, $({1}{\star},\mathcal F)$, $({1'}{\star},\mathcal F)$, and $({1'}{\star},\mathcal T)$.

Trying the other state, we get the illustration below, description from left to right.
- The clause is in the other state, tiling $({1}{\star},\mathcal T$ in one of two ways.
- Therefore, $({1}{\star},\mathcal F$ is forced on the wire,
- Leading the rest of the wire to tile correspondingly, and value the wire as false.
- Finally, in the contrapositive/upper section of the clause-gadget, $({1'}{\star},\mathcal F)$ must tile, because $({1'}{\star},\mathcal T)$ is taken in the wire. In this state, we have the tiles, $({A}{\star},{A}{\star})$, $({A}{\star},\mathcal T)$, $({A}{\star},\mathcal F)$, $({1}{\star},\mathcal T)$, $({1}{\star},\mathcal F)$, $({1'}{\star},\mathcal F)$, and $({1'}{\star},\mathcal T)$. These are the same tiles discharged as in the other state.

Thus in either state, we discharge the same tiles. Therefore, the wire and clause together successfully discharge specific tiles iff there is a satisfying assignment.
This gadget is closed, so there won't be a flow problem.
The clause-gadget together with the wire gadget are guaranteed to always discharge the same tile-pair values, and thus we can discharge these even if we don't know which way it will tile.
Now all of our gadgets fulfill the criteria.
Formulation
In our final formulation, we create three rows of gadgets, each separated by a horizontal wall.
- On the bottom, we place the forcing-gadgets, which are two tiles tall. We need a forcing gadget for the building block, and for combinations of $\mathcal T$ and $\mathcal F$. We place the forcing gadgets directly next to each-other.
- In the middle row, we place the wire gadgets, horizontally, which are two tiles tall. The wire gadgets should be separated from each-other with a vertical wall.
- In the top row, we place clause gadgets, which are four tiles tall. The clause gadgets should be separated from each-other by a vertical wall.
Illustrations follow, descriptions above each figure. Click images for full resolution. Source code to reproduce/generate the images is listed at the bottom of the page.
Using the formula $\Phi(\mathbf x)= (x_1,\neg x_2, x_3) \wedge (x_2,\neg x_3,x_4) \wedge (x_1,x_2,\neg x_4)$ as an example, we have a satisfying solution $(\neg x_1,x_2,x_3,\neg x_4)$ as a witness.
First we start with the horizontal walls separating the rows of gadgets. We show the squares, and the pairs that are forced to tile within the walls.

Next, we show the gadgets. The blue outline represents the borders of the gadgets; dashed blue for the forcing-gadgets, since they will not be surrounded by walls. Note the line in the middle of the clause gadget is not surrounded by a wall; it is there for ease-of-viewing; taking the line away does not allow any more states to occur in the clause, as explained above, but we show the blue line for this demonstration. Note: that we use square-names to give the numbers semantic readability, when applicable. Each name represents a numeric value.

Here we fill in the vertical walls.

Here we fill in the witness solution; i.e this is the tiling solution if using the SAT solution to generate it.

Next we tile the filler-area; the rest of the board, as large as needed, for as large as $n$ is required to tile thus-far. Thus we discharge the remaining pairs in the tile-set. The dashed lines here represent a valid-but-not-forced tiling; there might be another way of tiling these. Here we show the lower-left corner.

Here we fill in the remaining squares with a trivial valid tiling.

Here we show the lower right corner of the grid.

Here we show the upper right corner of the grid. Note how the vertical tiles no longer fit; so we tile the top row horizontally, if necessary.

And finally the top-left corner.

Generating the entire game-board at once via TeX fails with out-of-memory errors from pdflatex, so if you want to see it, you would have to generate clips and patch them together. Be sure to check out the notebook viewer.
TikZ sources
Game generator:
graphtex.py
Converts TeX to svg, using pdflatex, pdfcairo (poppler), and rsvg-convert (libsvg)
dominosa.py
Contains the conversion logic, game-solution verification, and drawing logic
dominosa_demo.py
An executable demo that generates the images used in the answer above. Dumps images to the current-working-directory.
dominosa_demo.ipynb
An ipython demo that generates the images used in the answer above.