snippetMinor
How to generate snowflakes of a fixed area as challenges for the FridgeIQ puzzle?
Viewed 0 times
thefridgeiqsnowflakeschallengesgenerateforhowfixedpuzzlearea
Problem
I have been presented a set of FridgeIQ by a friend and she has planted an idea in my head.
FridgeIQ is a geometric disection puzzle consisting of 16 polygonal tiles as seen in the terrible picture near the bottom of this post
The shapes of the tiles are based on a square grid with the occasional diagonal across one of the grid fields. The total area of all the tiles is 40 such grid units. Each tile is identified by a single unique letter.
In the box comes a set of challenges, each giving a subset of the tiles and a shape to create. For example one challenge is: "construct a square using the tiles BDQSYJN". Which I have done in that picture and I have some left-over tiles that were not part of that particular challenge.
In addition to the standard challenges my friend has presented me with an extra set of target shapes which finally are the point of this question. I have attached another picture showing one of them in solved state.
These extra challenges all use the complete tile set, so their total area is 40 units, and they all have fourfold mirror-symmetry. Not all of them are as simple like the one in the picture, some have a hole or holes, but they are all connected.
I shall call these shapes "snowflakes" because they in a way resemble decorative snowflakes cut out of folded paper to generate the symmetries. Especially the ones with holes.
I have been asking myself: How many such shapes with these constraints are there that can actually be made from the given tiles?
Snowflakes per se there are infinitely man. But I believe the set of connected ones with finite area made only of half-unit triangles must be finite. Propably enormous, but finite. The solveable ones are a subset of those.
What would be a good algorithm to generate them? I do not expect there to be an efficient way, nor do I believe the universe has enough time left to actually make them all. But I would love to find at least some new ones.
Here's some unfinished thoughts so far:
As a fi
FridgeIQ is a geometric disection puzzle consisting of 16 polygonal tiles as seen in the terrible picture near the bottom of this post
The shapes of the tiles are based on a square grid with the occasional diagonal across one of the grid fields. The total area of all the tiles is 40 such grid units. Each tile is identified by a single unique letter.
In the box comes a set of challenges, each giving a subset of the tiles and a shape to create. For example one challenge is: "construct a square using the tiles BDQSYJN". Which I have done in that picture and I have some left-over tiles that were not part of that particular challenge.
In addition to the standard challenges my friend has presented me with an extra set of target shapes which finally are the point of this question. I have attached another picture showing one of them in solved state.
These extra challenges all use the complete tile set, so their total area is 40 units, and they all have fourfold mirror-symmetry. Not all of them are as simple like the one in the picture, some have a hole or holes, but they are all connected.
I shall call these shapes "snowflakes" because they in a way resemble decorative snowflakes cut out of folded paper to generate the symmetries. Especially the ones with holes.
I have been asking myself: How many such shapes with these constraints are there that can actually be made from the given tiles?
Snowflakes per se there are infinitely man. But I believe the set of connected ones with finite area made only of half-unit triangles must be finite. Propably enormous, but finite. The solveable ones are a subset of those.
What would be a good algorithm to generate them? I do not expect there to be an efficient way, nor do I believe the universe has enough time left to actually make them all. But I would love to find at least some new ones.
Here's some unfinished thoughts so far:
As a fi
Solution
SAT solvers are my favorite "big sledgehammer" to apply to this kind of problem, so let me describe how you could use a SAT solver for this problem.
Let's constrain the shape to fit within a 15x15 grid (say), and express the problem of finding a valid shape as a SAT problem. It gets a bit messy, so you'll have to be willing to tolerate that, but the approach is powerful. Introduce boolean variables $x_{i,j,k}$, with the intended meaning that $x_{i,j,k,r}=1$ means that we rotate tile $k$ into orientation $r$ and then put its upper-left corner in the grid cell at coordinates $(i,j)$. We'll now write down some boolean formulas that characterize what it means for this to be a valid snowflake.
There a bunch of requirements to count as a valid snowflake; I'll sketch how to express each one as a boolean formula:
-
Each tile must be used exactly once. In other words, for each $k$, exactly one of the $x_{i,j,k,r}$'s must be true; this is is a one-out-of-n constraint. See Encoding 1-out-of-n constraint for SAT solvers for some techniques for encoding this as a boolean formula (or if you use Z3, see https://stackoverflow.com/q/43081929/781723).
-
The shape must be symmetric. To help check this, let's introduce auxiliary boolean variables $y_{i,j}$, with the intended meaning that $y_{i,j}=1$ means that the grid cell at coordinates $(i,j)$ is covered by some tile. It is easy to express $y_{i,j}$ as a logical-or of a subset of the $x$'s (namely, all the $x_{i',j',k,r}$ such that placing tile $k$ in orientation $r$ at position $(i',j')$ will also cover $(i,j)$; knowing the shape of each tile, you can precompute all such $x$'s; there will be 160 of them). Moreover, let's require this to have fourfold symmetry around the origin. That means $y_{i,j} = y_{-i,j} = y_{i,-j} = y_{-i,-j}$ holds for all $i,j$.
-
No two pieces overlap. This involves a bunch of constraints of the form $(\neg x_{i,j,k,r}) \lor (\neg x_{i',j',k',r'})$, for all $i,j,k,r,i',j',k,k',r,r'$ such that placing tile $k$ at coordinates $(i,j)$ in orientation $r$ would overlap with placing tile $k'$ at coordinates $(i',j')$ in orientation $r'$. (This can be easily precomputed based on the shape of tiles $k$ and $k'$.)
This gives you a bunch of boolean formulas. Write down the conjunction of all of them, and then feed it to an off-the-shelf SAT solver and ask the SAT solver to find a satisfying solution for you. This will then correspond to a snowflake.
For implementing this stuff, I find Z3 a very convenient API to a SAT solver.
This will find one snowflake. What if you want multiple of them? There is a straightforward way to generate multiple solutions: after you have found one solution, you generate what's called a "blocking clause" and add it to the list of constraints (i.e., conjoin it to the formula). The "blocking clause" just says "not that one I already know of". For instance, if you already have a satisfying assignment that assigns values $c_{i,j,k,r}$ to each $x_{i,j,k,r}$, then the blocking clause is the formula $\lor_{i,j,k,r} (x_{i,j,k,r} \ne c_{i,j,k,r})$. You can repeat this to obtain multiple solutions: each time you find another solution, you generate another blocking clause, add it to the formula, and apply the SAT solver again. Some SAT solvers even have special support for incrementally adding additional constraints that is more efficient than starting the search from scratch, though that might not be necessary.
Well, that's the idea, anyway. But here I have to confess that I lied. There is one requirement that I've left out so far: connectivity. You said you want each snowflake to be connected. That's messier to implement in a boolean formula, though also possible. The crude hack is to generate many candidate snowflakes as above, check each for connectivity, and keep only the connected ones. However, this might not work very well. So, let me describe how to encode the connectivity constraint in SAT. Beware; it gets messy, so hold onto your hat.
The shape must be connected. The main idea will be to pick a particular grid cell, require that it be present, and require that every other covered grid cell be connected to it. Let's say we require that the grid cell at the origin $(0,0)$ be covered. Then we can introduce auxiliary variables $z_{i,j,s}$, with the intended meaning that $z_{i,j,s}=1$ means that grid cell $(i,j)$ can be reached by starting at the origin and then taking $s$ steps across adjacent covered grid cells. This constraint can be encoded in SAT by noting
$$z_{i,j,s} = y_{i,j} \land (z_{i-1,j,s-1} \lor z_{i,j-1,s-1} \lor z_{i+1,j,s-1} \lor z_{i,j+1,s-1}).$$
We'll adopt the convention that $z_{i,j,0}=1$, and if $(i,j)$ is outside of the 15x15 bounding box then by convention $y_{i,j,s}=z_{i,j,s}=0$ (we don't introduce extra variables for that, we just replace those terms with "false").
Finally, for each $i,j$, we add the constraint that $y_{i,j} \implies \lor_{s=0}^{39} z_{i,j,s}$. Th
Let's constrain the shape to fit within a 15x15 grid (say), and express the problem of finding a valid shape as a SAT problem. It gets a bit messy, so you'll have to be willing to tolerate that, but the approach is powerful. Introduce boolean variables $x_{i,j,k}$, with the intended meaning that $x_{i,j,k,r}=1$ means that we rotate tile $k$ into orientation $r$ and then put its upper-left corner in the grid cell at coordinates $(i,j)$. We'll now write down some boolean formulas that characterize what it means for this to be a valid snowflake.
There a bunch of requirements to count as a valid snowflake; I'll sketch how to express each one as a boolean formula:
-
Each tile must be used exactly once. In other words, for each $k$, exactly one of the $x_{i,j,k,r}$'s must be true; this is is a one-out-of-n constraint. See Encoding 1-out-of-n constraint for SAT solvers for some techniques for encoding this as a boolean formula (or if you use Z3, see https://stackoverflow.com/q/43081929/781723).
-
The shape must be symmetric. To help check this, let's introduce auxiliary boolean variables $y_{i,j}$, with the intended meaning that $y_{i,j}=1$ means that the grid cell at coordinates $(i,j)$ is covered by some tile. It is easy to express $y_{i,j}$ as a logical-or of a subset of the $x$'s (namely, all the $x_{i',j',k,r}$ such that placing tile $k$ in orientation $r$ at position $(i',j')$ will also cover $(i,j)$; knowing the shape of each tile, you can precompute all such $x$'s; there will be 160 of them). Moreover, let's require this to have fourfold symmetry around the origin. That means $y_{i,j} = y_{-i,j} = y_{i,-j} = y_{-i,-j}$ holds for all $i,j$.
-
No two pieces overlap. This involves a bunch of constraints of the form $(\neg x_{i,j,k,r}) \lor (\neg x_{i',j',k',r'})$, for all $i,j,k,r,i',j',k,k',r,r'$ such that placing tile $k$ at coordinates $(i,j)$ in orientation $r$ would overlap with placing tile $k'$ at coordinates $(i',j')$ in orientation $r'$. (This can be easily precomputed based on the shape of tiles $k$ and $k'$.)
This gives you a bunch of boolean formulas. Write down the conjunction of all of them, and then feed it to an off-the-shelf SAT solver and ask the SAT solver to find a satisfying solution for you. This will then correspond to a snowflake.
For implementing this stuff, I find Z3 a very convenient API to a SAT solver.
This will find one snowflake. What if you want multiple of them? There is a straightforward way to generate multiple solutions: after you have found one solution, you generate what's called a "blocking clause" and add it to the list of constraints (i.e., conjoin it to the formula). The "blocking clause" just says "not that one I already know of". For instance, if you already have a satisfying assignment that assigns values $c_{i,j,k,r}$ to each $x_{i,j,k,r}$, then the blocking clause is the formula $\lor_{i,j,k,r} (x_{i,j,k,r} \ne c_{i,j,k,r})$. You can repeat this to obtain multiple solutions: each time you find another solution, you generate another blocking clause, add it to the formula, and apply the SAT solver again. Some SAT solvers even have special support for incrementally adding additional constraints that is more efficient than starting the search from scratch, though that might not be necessary.
Well, that's the idea, anyway. But here I have to confess that I lied. There is one requirement that I've left out so far: connectivity. You said you want each snowflake to be connected. That's messier to implement in a boolean formula, though also possible. The crude hack is to generate many candidate snowflakes as above, check each for connectivity, and keep only the connected ones. However, this might not work very well. So, let me describe how to encode the connectivity constraint in SAT. Beware; it gets messy, so hold onto your hat.
The shape must be connected. The main idea will be to pick a particular grid cell, require that it be present, and require that every other covered grid cell be connected to it. Let's say we require that the grid cell at the origin $(0,0)$ be covered. Then we can introduce auxiliary variables $z_{i,j,s}$, with the intended meaning that $z_{i,j,s}=1$ means that grid cell $(i,j)$ can be reached by starting at the origin and then taking $s$ steps across adjacent covered grid cells. This constraint can be encoded in SAT by noting
$$z_{i,j,s} = y_{i,j} \land (z_{i-1,j,s-1} \lor z_{i,j-1,s-1} \lor z_{i+1,j,s-1} \lor z_{i,j+1,s-1}).$$
We'll adopt the convention that $z_{i,j,0}=1$, and if $(i,j)$ is outside of the 15x15 bounding box then by convention $y_{i,j,s}=z_{i,j,s}=0$ (we don't introduce extra variables for that, we just replace those terms with "false").
Finally, for each $i,j$, we add the constraint that $y_{i,j} \implies \lor_{s=0}^{39} z_{i,j,s}$. Th
Context
StackExchange Computer Science Q#104820, answer score: 2
Revisions (0)
No revisions yet.