I just noticed John Carmack's tweet about solving the Tantrix puzzle in Racket. I like solving puzzles with Cryptol and this seemed like a good opportunity for a non-cherry-picked problem.
Cryptol started as a domain specific language for cryptography. It has native support for arbitrary bit-width words and a built in bridge to automated (SMT) solvers. Each word is represented as a bit array which can be trivially permuted, split, joined, and indexed. These days, many people think of Cryptol as a convenient high-level language for running SAT or SMT solvers.
I didn't know what Tantrix was, but the above link has a decent explanation. In short, there are ten hexagonal shaped puzzle pieces with 3 different colored lines on each. The task is to make a loop out of a particular color using a particular number of tiles. For example, it should be simple to use three tiles and create a loop for the yellow line.
In contrast with general purpose languages in which you'd probably make an A* or similar search procedure, the solution strategy with Cryptol is almost always to describe the problem and define a boolean test that returns true for a valid solution. After we have a way to recognize the final solution just ask one of the satisfiability solvers to find the assignment that makes this function return true.
A more subtle contrast illuminates the method along with its relative strengths and weaknesses. Solutions that use SAT to recognize a valid solution require the developer to make an exhaustive set of rules or checks for each necessary condition. Solutions involving construction, testing, and back-tracking search encode some requirements implicitly in the construction and omit some checks in the final valid solution test. As a result, it can be conceptually hard to identify and write all necessary constraints of the solution but the reward is a concise description of valid solutions that is more amenable to later adjustment or application to related problems.
We've established that we'll be defining the Tantrix puzzle in Cryptol then using SAT to find the valid solution, so let's get to it. First we need to define the puzzle pieces and some basic operations.
Since there are only three colors we'll use 2 bits for color:
type Color = [2]
type Tile = [6]ColorOur puzzle has ten hexagonal tiles. Each Tile has three colored lines connecting two of the sides. Each side has exactly one color. Borrowing significantly from John Carmack's code mentioned in the introduction, our pieces start with the right-most color and go clock-wise from there.
tiles : [10]Tile
tiles = [ [r, y, y, b, r, b]
, [b, r, r, b, y, y]
, [r, r, b, b, y, y]
, [b, r, y, b, y, r]
, [r, y, y, r, b, b]
, [y, b, r, y, r, b]
, [r, b, b, y, r, y]
, [y, b, b, r, y, r]
, [r, b, y, r, y, b]
, [b, y, y, r, b, r]
]
where (r,b,y) = (red,blue,yellow)
red,blue,yellow : Color
(red,blue,yellow) = (0,1,2)Placements, the below Pt type, are a collection of a tile, location on the grid, and a rotation.
type Pos = ([8],[8])
type Dir = [3]
type Rot = Dir
type Pt = (Pos,Tile,Rot)
// Completed boards are n placements
type Board n = [n]PtWe can now add some simple helper functions to obtain the neighbor positions, test for neighbors, and get the color of a particular placed piece at a particular point (0 is right, working clockwise).
directions : [6]Dir
directions = [0..5]
neighbor : Pos -> Dir -> Pos
neighbor (x,y) dir = ns @ dir
where
ns = [ (x+1, y )
, (x+1, y-1)
, (x, y-1)
, (x-1, y )
, (x-1, y+1)
, (x, y+1)
]
isAdjacent : Pos -> Pos -> Bit
isAdjacent p0 p1 = or [neighbor p0 d == p1 | d <- directions] && noOverflow
where
noOverflow = and [~zero != v | v <- [p0.0,p0.1,p1.0,p1.1] ]
dirColor : Dir -> Pt -> Color
dirColor dir (_l, tile, rot) = tile @ ((extend dir + extend rot : [4]) % 6)We've ran across our first gotchas! A first attempt might check adjacency and calculate dirColor through simple arithmetic such as a.x == b.x + 1 but that doesn't account for overflow. Without these checks SAT will result in more interesting solutions than most people like. In the case of adjacency we cheat by not allowing the maximum index and use an excessively large grid.
Now that we have the structure, the solution starts to deviate from what Carmack pasted. What's left for us is not a construction of lines and tree search but "merely" describing a valid board. Valid boards for a given color have to 1. Have only valid placements 2. Use each tile only once 3. No tiles overlap 4. when considering the line it must form a loop. Let's focus on the first three and break 4 down in a minute.
Step 1: Placement validation is a check that each tile is from the original game - the tiles array.
Steps 2 and 3: Uniqueness testing of the tiles, their positions, or anything else can be done in a few ways. Conceptually we can just test each element for equality with all elements in the set and ensure only one was equal (e.g. to itself). While this appears inefficient two things to remember are that this toy problem is small and there is an army of optimizations just under the surface. We do have to pay the cost of syntactically reforming the problem but many duplicated and excess terms will be handled by the solver.
We also require the board to include the origin. Requiring a tile at the origin is without loss of generality (I think) because the whole board can be rotated till a tile fits in the origin's corner, but I have not proven this to be the case.
validSolution : {n} (n >= 3, n <= 10) => Color -> Board n -> Bit
validSolution c brd =
hasOrigin && validTileSet brd &&
uniquePositions brd && boardIsLoop c brd
where
validTileSet bs = unique && fromBag
where unique = and [ uniquely (\x -> x.1 == b.1) bs | b <- bs ]
fromBag = and [ elem b.1 tiles | b <- bs ]
uniquePositions bs = and [uniquely (\x -> x.0 == b.0) bs | b <- bs]
hasOrigin = or [b.0 == zero | b <- brd]The simplest method I found for loop checking breaks the problem down in three ways 1. Ensure the board is ordered such that each tile adjacent in the array is conceptually adjacent on the board 2. Walking the path forward from the current tile, the direction of the next neighbor is also a direction of the color of interest 3. Walking the path backward from the current tile, the direction of the neighbor is also the direction of the color of interest.
All three of these requirements can be expressed by the same path traversal that takes a predicate and tests every pair of neighbors. We must make sure the last tile and first tile are paired too so we have a loop instead of an uninterrupted line. I handled this with an excessive, but sufficient, extra lap around the loop.
boardIsLoop : {n} (fin n, n >= 3, n <= 10) => Color -> Board n -> Bit
boardIsLoop c bs =
forPath adjacentPl bs &&
forPath colorsMatch bs &&
forPath colorsMatch (reverse bs)
where
forPath pred xs = and [pred b0 b1 | b0 <- (xs # xs)
| b1 <- drop `{1} (xs # xs) ]
adjacentPl a b = isAdjacent a.0 b.0
colorsMatch a b = and [b.0 == neighbor a.0 d ==> dirColor d a == c
| d <- directions]And that's the entirety of the solution. We can get a little prettier (and smaller) by 1. Pushing lots of the helper functions into Cryptol and 2. Defining a pretty printing function. Item 1 is done - pull request 299 on github and would benefit actual project, not just toys. Cryptol needs a larger Prelude. Item 2 is small unless you want something graphical or colored text, which Cryptol as a DSL can not do. My pretty printer performs the rotations and presents the color values in a normalized form:
pretty : {n} (fin n) => Board n -> [n](Pos, [6]Color)
pretty bs = [ (b.0, b.1 <<< b.2) | b <- bs ]Now we can run code to obtain solutions:
:sat (validSolution `{3} yellow)
pretty (it.arg1)
[((0x00, 0x01), [0x0, 0x2, 0x2, 0x1, 0x0, 0x1]),
((0x00, 0x00), [0x2, 0x0, 0x1, 0x1, 0x0, 0x2]),
((0x01, 0x00), [0x0, 0x0, 0x1, 0x2, 0x2, 0x1])]Solving all 10 versions of the problem takes a heart-beat. Not surprising, but fun and educational for the kids at Christmas.