How to translate Four-sided Dice Puzzle to a logical formula? The puzzle:
We have $3$ dice, each having $4$ sides. Every side of every dice has a single letter on it (rather than a number).
We want to be able to make each of the words CAT, SON, POD, RIG, PEG, TAP, DIN, APE by rolling all dice together and rearranging them in the right order.
Determine the symbols on each dice.
I need to use the logical formula (i.e. all the conditions the dice have to satisfy) to let an SMT solver solve the problem via Z3.
I can't figure out how to translate this into a logical formula.
 A: If there is a logical formula, it's going to be very long, because you have $12$ different locations to be filled with $12$ different letters.
Moreover, in terms of actually solving the problem, merely translating it into a logical formula is not necessarily going to make it any easier to solve, because the problem of satisfying a proposition in Boolean logic is one of the famous NP-complete problems. Informally you can take this as an indication that you might end up having to just brute-force the solution by very tedious trial and error.
But in this case there is almost a deterministic algorithm to solve the problem. Very little trial-and-error is really required.
Try making a grid of eight rows by four columns. Put the words you have to make in the first column. The letters to put on the dice will go in the other three columns, where each column contains all the letters that are on one die.
Since the columns can be exchanged without affecting what words can be made, we might as well start by filling in one of the words, say CAT, in the last three columns. So we start out like this:
\begin{array}{|c|c|c|c|}\hline
 CAT & C & A & T \\ \hline
 SON &  &  &  \\ \hline
 POD &  &  &  \\ \hline
 RIG &  &  &  \\ \hline
 PEG &  &  &  \\ \hline
 TAP &  &  &  \\ \hline
 DIN &  &  &  \\ \hline
 APE &  &  &  \\ \hline
\end{array}
Now since there are $12$ different letters that must fit on the $12$ sides of the three dice, we know that whenever a letter appears in a column, that letter must appear again in the same column on every row where that letter is used in the word in the first column. Doing this for the letters C, A, T, we get this result:
\begin{array}{|c|c|c|c|}\hline
 CAT & C & A & T \\ \hline
 SON &  &  &  \\ \hline
 POD &  &  &  \\ \hline
 RIG &  &  &  \\ \hline
 PEG &  &  &  \\ \hline
 TAP &  & A & T \\ \hline
 DIN &  &  &  \\ \hline
 APE &  & A &  \\ \hline
\end{array}
Another simple rule is that whenever we have just one empty cell in a given row, that cell must be filled with the remaining letter of the word that has not yet been written on that row:
\begin{array}{|c|c|c|c|}\hline
 CAT & C & A & T \\ \hline
 SON &  &  &  \\ \hline
 POD &  &  &  \\ \hline
 RIG &  &  &  \\ \hline
 PEG &  &  &  \\ \hline
 TAP & P & A & T \\ \hline
 DIN &  &  &  \\ \hline
 APE &  & A &  \\ \hline
\end{array}
Write the additional copies of the new letter where they must occur:
\begin{array}{|c|c|c|c|}\hline
 CAT & C & A & T \\ \hline
 SON &  &  &  \\ \hline
 POD & P &  &  \\ \hline
 RIG &  &  &  \\ \hline
 PEG & P &  &  \\ \hline
 TAP & P & A & T \\ \hline
 DIN &  &  &  \\ \hline
 APE & P & A &  \\ \hline
\end{array}
Continue applying these two simple rules. The next step is to write the remaining letter of APE, namely E, in the blank cell in that row, then write copies of E in the row for PEG; this leaves only one blank cell in the PEG row, which you fill with G, which you then copy in the RIG row. At this point the grid looks like this:
\begin{array}{|c|c|c|c|}\hline
 CAT & C & A & T \\ \hline
 SON &  &  &  \\ \hline
 POD & P &  &  \\ \hline
 RIG &  & G &  \\ \hline
 PEG & P & G & E \\ \hline
 TAP & P & A & T \\ \hline
 DIN &  &  &  \\ \hline
 APE & P & A & E \\ \hline
\end{array}
At this point all the letters in the grid have been copied wherever they can be, and there are no rows with only one blank cell, so we have to try something else.
We have six remaining letters to put in ten remaining empty cells. Four of the letters, D, I, N, and O, get written twice each, and the remaining two letters, R and S, get written once each. Three of the doubled letters occur in rows where there are only two empty cells, so if we choose one of these letters there are only two possible ways to fill that letter in the grid. Try each way an continue solving as before; only one of the attempts will work.
That's a little trial and error, but not much.
As an alternative to trial and error, let's start over with a new word.
There is one word, DIN, that contains three of the doubled letters left over from the first stage of the solution. If we fill these letters into the grid (not using any of the letters we used before), we get this:
\begin{array}{|c|c|c|c|}\hline
 CAT &  &  &  \\ \hline
 SON &  &  &  \\ \hline
 POD &  &  &  \\ \hline
 RIG &  &  &  \\ \hline
 PEG &  &  &  \\ \hline
 TAP &  &  &  \\ \hline
 DIN & D & I & N \\ \hline
 APE &  &  &  \\ \hline
\end{array}
Copy the letters of DIN where they need to be copied:
\begin{array}{|c|c|c|c|}\hline
 CAT &  &  &  \\ \hline
 SON &  &  & N \\ \hline
 POD & D &  &  \\ \hline
 RIG &  & I &  \\ \hline
 PEG &  &  &  \\ \hline
 TAP &  &  &  \\ \hline
 DIN & D & I & N \\ \hline
 APE &  &  &  \\ \hline
\end{array}
There is one remaining doubled letter, O, which has to be written in the rows for SON and POD, in the same column both times. Only the second column is empty in these two rows, so O goes there:
\begin{array}{|c|c|c|c|}\hline
 CAT &  &  &  \\ \hline
 SON &  & O & N \\ \hline
 POD & D & O &  \\ \hline
 RIG &  & I &  \\ \hline
 PEG &  &  &  \\ \hline
 TAP &  &  &  \\ \hline
 DIN & D & I & N \\ \hline
 APE &  &  &  \\ \hline
\end{array}
We can now fill in the remaining letters of SON and POD.
Let's do this and then compare the grid we have so far (derived from DIN) side by side with the grid we derived earlier from CAT:
$$
\begin{array}{|c|c|c|c|}\hline
 CAT &  &  &  \\ \hline
 SON & S & O & N \\ \hline
 POD & D & O & P \\ \hline
 RIG &  & I &  \\ \hline
 PEG &  &  &  \\ \hline
 TAP &  &  &  \\ \hline
 DIN & D & I & N \\ \hline
 APE &  &  &  \\ \hline
\end{array}
\qquad
\begin{array}{|c|c|c|c|}\hline
 CAT & C & A & T \\ \hline
 SON &  &  &  \\ \hline
 POD & P &  &  \\ \hline
 RIG &  & G &  \\ \hline
 PEG & P & G & E \\ \hline
 TAP & P & A & T \\ \hline
 DIN &  &  &  \\ \hline
 APE & P & A & E \\ \hline
\end{array}
$$
Somehow we have to be able to reconcile these two grids into a third grid.
Obviously we cannot just copy the letters of the grid on the left to the grid on the right, because some copied letters would conflict with letters already written in the grid, but remember that the sequence of columns was arbitrary.
So we can shuffle columns of the left-hand grid to make it "fit" the right-hand grid.
Clearly the P of POD has to be in the same column in each grid, so let's take column $3$ of the left grid and put it before the other two columns. Now we have
$$
\begin{array}{|c|c|c|c|}\hline
 CAT &   &   &   \\ \hline
 SON & N & S & O \\ \hline
 POD & P & D & O \\ \hline
 RIG &   &   & I \\ \hline
 PEG &   &   &   \\ \hline
 TAP &   &   &   \\ \hline
 DIN & N & D & I \\ \hline
 APE &   &   &   \\ \hline
\end{array}
\qquad
\begin{array}{|c|c|c|c|}\hline
 CAT & C & A & T \\ \hline
 SON &  &  &  \\ \hline
 POD & P &  &  \\ \hline
 RIG &  & G &  \\ \hline
 PEG & P & G & E \\ \hline
 TAP & P & A & T \\ \hline
 DIN &  &  &  \\ \hline
 APE & P & A & E \\ \hline
\end{array}
$$
It is also clear that the last two columns of the left-hand grid have to be copied in the order shown above, because if we swapped them then the left-hand grid would have an I in column $2$ and this would conflict with the G of RIG in the right-hand grid.
Copying the letters from one grid to the other, we get
\begin{array}{|c|c|c|c|}\hline
 CAT & C & A & T \\ \hline
 SON & N & S & O \\ \hline
 POD & P & D & O \\ \hline
 RIG &  & G & I \\ \hline
 PEG & P & G & E \\ \hline
 TAP & P & A & T \\ \hline
 DIN & N & D & I \\ \hline
 APE & P & A & E \\ \hline
\end{array}
There's only one cell left and only one way to fill it:
\begin{array}{|c|c|c|c|}\hline
 CAT & C & A & T \\ \hline
 SON & N & S & O \\ \hline
 POD & P & D & O \\ \hline
 RIG & R & G & I \\ \hline
 PEG & P & G & E \\ \hline
 TAP & P & A & T \\ \hline
 DIN & N & D & I \\ \hline
 APE & P & A & E \\ \hline
\end{array}
Read off the unique letters from each column:
\begin{array}{c}
CNPR \\
ASDG \\
TOIE
\end{array}
Those are the letters on each die.
A: There are 12 unique letters, so each must appear exactly once.
answer set = {ASDG, TOIE, CNPR}
Arrange the words in a grid like so and then tally the unique contents of each column. Where a letter appears in more than one column, swap columns. This can happen recursively.
A: Let $c_1, c_2, c_3$ be the statements that letter C is on die #1, #2, or #3 respectively.  It must be at least one, so
$$c_1\lor c_2\lor c_3$$
and it can't be on more than one, so
$$(c_1\land\lnot c_2)\\
(c_1\land\lnot c_3)\\\vdots$$
We want CAT so these three letters must be on different dice:
$$(c_1\land a_2\land t_3)\lor\\
(c_1\land a_3\land t_2)\lor\\\vdots$$
Maybe you can take it from there.  As has been pointed out elsewhere, you can abbreviate this somewhat by arbitrarily assuming that $c_1, a_2, t_3$ are all true and simplifying the formulas accordingly.
