Bart Massey
Given these four pieces
+-----+ +-----+ +-----+ +-----+
| 3 | | 3 | | 2 | | 1 |
|4 1| |2 4| |4 1| |2 4|
| 2 | | 1 | | 3 | | 3 |
+-----+ +-----+ +-----+ +-----+
we can rearrange and rotate them arbitrarily and assemble them into a square
+-----+-----+
| 4 | 3 |
|3 1|1 4|
| 2 | 2 |
+-----+-----+
| 2 | 4 |
|3 1|2 3|
| 4 | 1 |
+-----+-----+
Can we make a square such that all the edges match?
Our solution strategy will involve:
- Creating a SAT formula from the instance
- Solving that formula with an off-the-shelf solver
- Interpreting the SAT soln as an instance solution
You must have picosat
installed to use this code as-is. It
can be easily modified for other DIMACS-format SAT
solvers. To try it out:
sh foursquare-sat.sh puzzles/orig.txt
You should see the puzzle and its solution.
You can say python3 puzgen.py
to get more puzzles. Puzzle
format is one piece per row with the edge numbers listed in
counterclockwise order.
-
Number the pieces 1..4, the positions in the square 1..4. We will number the square positions clockwise starting from the upper left. We will number the edges of the piece counterclockwise starting from the right edge.
l(s, p) iff piece p is in square s (location)
-
Number the coordinates of the edges of each square 1..4
m(s, e, n) iff piece in square s at edge e is n (match)
-
Number the edges of each piece 1..4
v(p, e, n) iff piece p at edge e is n (value)
-
Number the rotations of each piece 0..3. Rotations will be counterclockwise.
r(p, k) iff piece p has rotation k
-
Every piece is at some location
forall s . exists p . l(s, p)
-
No location contains more than one piece
forall s . forall p1, p2 | p1 =/= p2 . not l(s, p1) or not l(s, p2)
-
First piece is in first corner (remove rotational symmetry)
l(1, 1)
-
Every location has a piece
forall p . exists s . l(s, p)
-
No piece is at more than one location
forall p . forall s1, s2 | s1 =/= s2 . not l(s1, p) or not l(s2, p)
-
Every piece is at some rotation
forall p . exists k . r(p, k)
-
No piece has more than one rotation
forall p . forall k1, k2 | k1 =/= k2 . not r(p, k1) or not r(p, k2)
-
Square coordinates are a function of piece location and rotation
forall s, p, k, e, n . m(s, e, n) if l(p, s) and r(p, k) and v(p, (4 - k + e) mod 4, n)
-
No square edge can have more than one value
forall s, e . forall n1, n2 | n1 =/= n2 . not m(s, e, n1) or not m(s, e, n2)
-
Edges must match
forall s1, e1, s2, e2 | s1 = 1 and e1 = 1 and s2 = 2 and e2 = 3 or … . forall n . m(s1, e1, n) iff m(s2, e2, n)