# How to generate snowflakes of a fixed area as challenges for the FridgeIQ puzzle?

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 first step I have built a simple recursive-backtracking solver that reproduced my manual solutions (and found loads of alternative ones). So even if it would be terribly inefficient I could just generate snowflake-shapes at will and use my solver to check them.

I have been thinking that it would suffice to generate one eighth of the shape, one half-quadrant, with a total area of 10 units. Symmetry provides the rest. Note that the solution does not have the same symmetry when considering individual tiles, only when the complete shape is taken into account.

To generate candidate shapes I could just put 20 half-unit-triangles into the half-quadrant. Hopefully in some systematic fashion. Most of those arrangements will not be compact enough and be unsolvable, though. And without a good idea for weeding them out their numbers are absolutely intractable.

Another approach would be to just generate combinations of the tiles and check them for symmetry. Again the algorithm would have to favour symmetric layouts or the exploding combinatorics mean I can never hope to find even a single new layout.

Any ideas? Keywords for searches and/or pointers to literature are also appreciated.

Thank you very much.

• I'm not completely sure how pattern construction works: are those tiles only placed next to eachother, or do they have to be attached in some particular way? In any case, this sounds like a tricky problem, so it may be hard to get more problem-specific insights. You could try to improve your uniformed search method of recursive backtracking by modeling your problem as a constraint satisfaction problem and letting specialized solver software find solutions to your modeled problem. – Discrete lizard Feb 25 '19 at 11:46

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}$$. This ensures that every covered cell is reachable. (Note that if it is reachable, it is reachable in at most 39 steps, so we only need to go up that high. In practice, I suspect that 19 or even 9 are probably large enough.)

That ensures connectivity. However, there's a potential catch: this requires everything to be connected to the origin, so it only generates snowflakes that cover the origin. We also want snowflakes that have a hole at the origin. I think you can fix this by iterating over all possibilities for the 'anchor point' (one grid cell that you'll require to be covered and require everything to be connected to), and solving the SAT instance for each possible anchor point. (To avoid duplicates, if you like you can add additional constraints to ensure disjointness of solutions. For instance, solve one SAT system where you require $$(0,0)$$ to be covered and everything to be connected to $$(0,0)$$; solve another where you require $$(0,1)$$ to be covered and everything to be connected to $$(0,1)$$ and you require $$(0,0)$$ to be uncovered; another where you require $$(0,2)$$ to be covered and everything to be connected to $$(0,2)$$ and you require $$(0,0)$$ and $$(0,1)$$ to be uncovered; and so on.)

Lastly, in the above I assumed that your shapes are collections of squares, i.e., they either completely cover a grid cell or don't touch it at all. Of course, this isn't valid for your tiles, due to those diagonal pieces. So, I suggest that after breaking down the 15x15 region into 225 small squares, you break down each square into four triangles. Then, instead of using the $$y$$'s to record which grid squares are covered, you'll need to adjust the definition of the $$y$$'s and the above formulas to record which triangles are covered. Everything should go through with some straightforward adjustments.

Phew. I told you it would get messy. The basic idea here is that we are taking each of the conditions for a shape to count as a valid snowflake, writing them down in boolean logic, and then letting the SAT solver find solutions that meet all of those requirements. SAT solvers today are amazing and contain clever and powerful strategies to automatically find solutions that meet your requirements. Researchers have spent decades coming up with better algorithms and improving the engineering of the tools; you can't hope to duplicate that, so rather than trying, you can build on all of their work and apply it to your specific situation.

• Love your answer, exactly what I was looking for and very well written up. Now I have some reading and learning to do. Thank you very much! – Marian Aldenhövel Feb 26 '19 at 8:39
• I have a follow-up-question, maybe you are around to give me a nudge: Your writeup disregards a vital condition (I think), namely that the pieces may not overlap. The conditions you listed could yield a solution where they are all just stacked on top of each other in a small space. Granted, I did not make that explicit, and it may yield interesting results if allowed. To add this constraint could I compute your y's as integers and sum up all the x's that cover each of them? And then add a condition stating that sum to be either 1 or 0 for each y? Or as another k-out-of-n constraint? – Marian Aldenhövel Feb 28 '19 at 11:00
• @MarianAldenhövel, oh, good point! You're absolutely right, I missed another requirement. I edited the answer to add that missing piece -- see the bullet point labelled "No two pieces overlap". – D.W. Mar 1 '19 at 6:35