2020-05-26

Judging by the recent surge in popularity of the excellent Cracking the Cryptic YouTube channel, I’m not the only person for who recent circumstances have led them to rediscover logic puzzles. There is an entire art to hand-crafting these Puzzles that I never appreciated, complete with world-famous “setters”, and it makes for a perfect nerdy rabbit hole for people suddenly spending a lot of time inside. There are classic puzzles, like the Sudoku, but things become especially interesting when you start playing with the rule set. For example, you might have seen the viral “Miracle Sudoku” that has only 2 given digits (on which more later).

The same goes for writing solvers: writing a Sudoku solver is trivial, but can we make one in which we can easily play with the rules? Designing an interesting puzzle becomes a lot easier if you can freely experiment with rules while making sure that you still have a unique solution.

It turns out you can, and it’s a great exercise in higher-order functions and composition. So, in this post, we’re going to write a solver.

A `Rule`

tells us whether, given a *partial* solution to a puzzle, we can put an answer `a`

in some cell `i`

(for *index*). Once we manage to assign an answer to *every* cell in the puzzle, we have a (hopefully unique) solution.

```
type Solution i a = i -> a
type Rule i a = Solution i (Maybe a) -> i -> a -> All
```

`All`

is a monoid over `Bool`

where `(<>) == (&&)`

and using it here also makes `Rule i a`

a monoid. It gives us a way to compose rules for free, with `rule1 <> rule2`

meaning that both `rule1`

and `rule2`

must hold, and `mempty`

being a rule that always passes.

For the initial given digits/answers, we’ll keep it simple and just use a list of pairs.

`type Givens i a = [(i, a)]`

We also need a way to list all inhabitants of our `i`

and `a`

types. There are libraries that do this for you, but I like to avoid the dependency and just leverage the `Ix`

^{1} type class from `base`

.

```
type Universe a = (Bounded a, Ix a)
universe :: Universe a => [a]
= range (minBound, maxBound) universe
```

With the types taken care of, the solver practically writes itself. For each cell, we try to assign an answer that satisfies the rule, and the list monad takes care of backtracking if there are no more valid answers:

```
solve ::
forall i a.
Universe i, Universe a) =>
(Rule i a ->
Givens i a ->
Solution i a]
[= go (filter (`Map.notMember` m0) universe) m0
solve rule given where
m0 :: Map i a
= Map.fromList given
m0 go :: [i] -> Map i a -> [Solution i a]
= pure (m Map.!)
go [] m : is) m = do
go (i <- universe
a . getAll $ rule (m Map.!?) i a
guard go is (M.insert i a m)
```

As an initial exercise/proof-of-concept, we’ll try the classic *n* queens puzzle. The object is to place *n* queens on an *n* × *n* chess board, such that none is under attack by another. Our domain `i`

consists of the indices of the columns of the board, and our range `a`

is the row at which there is a queen in that column. Both of these are integers in the range 0…*n* − 1. We’ll use the `finite-typelits`

package to represent bounded finite integers^{2}.

We then write a rule that expresses that to place a queen in (*x*,*y*), none of the other columns can have a queen in row *y* or any of the diagonals of (*x*,*y*):

```
nqueens :: KnownNat n => Rule (Finite n) (Finite n)
= All . and $ do
nqueens f x y <- universe
qx <- toList (f qx)
qy /= y, difference qx x /= difference qy y]
[qy
difference :: KnownNat n => Finite n -> Finite n -> Finite n
= max a b - min a b difference a b
```

If we now ask GHCi how many ways there are to place the *n* queens on the board, we get the expected answers^{3}:

```
λ> length $ solve (nqueens @8) []
92
λ> length $ solve (nqueens @4) []
2
λ> length $ solve (nqueens @12) []
14200
```

Now that we know the solver works, we can turn our attention towards Sudoku solving.

One thing that will come up *a lot* in these puzzles is the concept of a cell “seeing” other cells. For example, in normal Sudoku rules a cell “sees” all cells in its row, column, and 3 × 3 box. We express this as a function, from a cell to a set of all the cells it sees:

```
type Sees i = i -> Set i
row :: (Universe x, Ord y) => Sees (x, y)
= Set.fromList $ (,y) <$> universe
row (_, y)
column :: (Universe y, Ord x) => Sees (x, y)
= Set.fromList $ (x,) <$> universe
column (x, _)
type F9 = Finite 9
box :: Sees (F9, F9)
= Set.fromList . bitraverse (group 3) (group 3)
box where
group n d = let b = div d n * n in [b .. b + (n -1)]
```

Since `Set`

is a monoid, `Sees`

is also monoid, and it composes beautifully:

```
λ> (column <> row <> box) (3,2)
fromList [(0,2),(1,2),(2,2),(3,0),(3,1),(3,2),(3,3),(3,4),(3,5),(3,6),(3,7),(3,8),(4,0),(4,1),(4,2),(5,0),(5,1),(5,2),(6,2),(7,2),(8,2)]
```

The single rule of Sudoku is that a cell must be unique among the cells that it sees. We will call this concept, of a property that holds between a cell and those it sees, a *relation*, and together with `Sees`

we can turn them into *rules*:

```
type Relation a = a -> [a] -> All
unique :: Eq a => Relation a
= (All .) . notElem
unique
withSeen :: forall i a. Sees i -> Relation a -> Rule i a
= go
withSeen sees rel where
go :: Solution i (Maybe a) -> i -> a -> All
= rel a $ Set.toList (sees i) >>= toList . f go f i a
```

We now have two equivalent ways of expressing the rules of Sudoku:

```
sudokuRules :: Rule (F9, F9) F9
= withSeen row unique <> withSeen column unique <> withSeen box unique
sudokuRules = withSeen (row <> column <> box) unique sudokuRules
```

The only thing that’s left is to find a Sudoku to solve. From now on, I’ll start using some functions whose implementations are neither interesting nor particularly relevant. If you see a naked type signature its implementation can be found in the appendix.

```
printSolution :: (Solution i a -> String) -> [Solution i a] -> IO ()
showGrid :: (Universe x, Universe y) => (a -> Char) -> Solution (x, y) a -> String
showF9 :: F9 -> Char
parseSudoku :: [String] -> Givens (F9, F9) F9
normalSudoku :: Givens (F9, F9) F9
=
normalSudoku
parseSudoku"5 3 . . 7 . . . .",
[ "6 . . 1 9 5 . . .",
". 9 8 . . . . 6 .",
"8 . . . 6 . . . 3",
"4 . . 8 . 3 . . 1",
"7 . . . 2 . . . .",
". 6 . . . . 2 8 .",
". . . 4 1 9 . . 5",
". . . . 8 . . 7 ."
]
```

And sure enough:

```
λ> printSolution (showGrid showF9) (solve sudokuRules normalSudoku)
5 3 4 6 7 8 9 1 2
6 7 2 1 9 5 3 4 8
1 9 8 3 4 2 5 6 7
8 5 9 7 6 1 4 2 3
4 2 6 8 5 3 7 9 1
7 1 3 9 2 4 8 5 6
9 6 1 5 3 7 2 8 4
2 8 7 4 1 9 6 3 5
3 4 5 2 8 6 1 7 9
```

It looks like our solver works, so let’s write some Sudoku variations. For example, one popular variation is anti-knight Sudoku, in which, in addition to the normal Sudoku rules, a cell cannot contain the same digit as any cell a chess knight’s move away:

```
fromOffsets :: KnownNat n => [(Integer, Integer)] -> Sees (Finite n, Finite n)
= Set.fromList $ do
fromOffsets offsets (x, y) <- offsets
(dx, dy) <$> asInt (+ dx) x <*> asInt (+ dy) y
(,) where
= maybe [] pure . packFinite . f . getFinite
asInt f
knight :: KnownNat n => Sees (Finite n, Finite n)
= fromOffsets $ [(2, 1), (1, 2)] >>= bitraverse f f
knight where
= [x, -x]
f x
antiknightSudoku :: Givens (F9, F9) F9
=
antiknightSudoku
parseSudoku". 3 . . 4 1 . . 7",
[ ". . . 5 3 . . 4 .",
"4 . . 8 . 9 . 3 .",
"6 . 3 . . . . 7 .",
". . . 6 . 3 . . 4",
". 4 . . . . . . .",
"3 . . . . . . . .",
". . . . 6 . . 5 .",
". 6 4 3 . . . . ."
]
= sudokuRules <> withSeen knight unique antiknightRules
```

If we attempt to solve this with regular Sudoku rules it’s ambiguous, but as expected, adding the anti-knight rule gives us the following unique solution:

```
λ> printSolution (showGrid showF9) (solve antiknightRules antiknightSudoku)
5 3 6 2 4 1 8 9 7
9 7 8 5 3 6 2 4 1
4 2 1 8 7 9 6 3 5
6 1 3 4 8 5 9 7 2
7 8 9 6 2 3 5 1 4
2 4 5 9 1 7 3 6 8
3 5 7 1 9 8 4 2 6
8 9 2 7 6 4 1 5 3
1 6 4 3 5 2 7 8 9
```

We’re ready for the “Miracle” Sudoku we talked about in the introduction. The Miracle Sudoku has extremely few givens, but makes up for it in rules. The rules are

- Normal Sudoku
- Antiknight
- Anti
*king* - No two consecutive digits can be orthogonally adjacent

```
=
miracleSudoku
parseSudoku". . . . . . . . .",
[ ". . . . . . . . .",
". . . . . . . . .",
". . . . . . . . .",
". . 1 . . . . . .",
". . . . . . 2 . .",
". . . . . . . . .",
". . . . . . . . .",
". . . . . . . . ."
]
=
miracleRules
sudokuRules<> withSeen (knight <> king) unique
<> withSeen adjacent noConsecutive
king :: KnownNat n => Sees (Finite n, Finite n)
= fromOffsets $ (,) <$> [-1 .. 1] <*> [-1 .. 1]
king
adjacent :: KnownNat n => Sees (Finite n, Finite n)
= fromOffsets [(0, -1), (0, 1), (1, 0), (-1, 0)]
adjacent
noConsecutive :: KnownNat n => Relation (Finite n)
= All . all ((/= 1) . difference n) noConsecutive n
```

As for actually solving it, I highly recommend trying it for yourself, especially since if you don’t compile GHCi will take a while.

That concludes the Sudokus, let’s try a few other puzzles.

Now that we’re more familiar with how to write and compose rules, let’s look back and have some fun with the *n* queens problem. We’re going to express it differently this time, instead of mapping every column to a row with a queen, we’ll express it as mapping every cell on the board to whether or not there is a queen there, similar to how we mapped each cell of a Sudoku to a digit. This allows us some more flexibility, like decomposing *n* queens into *n* bishops and *n* rooks:

```
data Square = Piece | Empty
deriving (Eq, Show, Bounded, Ix, Ord, Enum)
nonattacking :: Relation Square
Empty _ = All True
nonattacking Piece xs = All (notElem Piece xs)
nonattacking
diagonals :: KnownNat n => Sees (Finite n, Finite n)
= Set.fromList $ do
diagonals (x, y) <- universe
d <- [x - d, x + d]
dx let dy = y - d
$ difference x dx == difference y dy
guard pure (dx, dy)
nrooks :: KnownNat n => Rule (Finite n, Finite n) Square
= withSeen (row <> column) nonattacking
nrooks
nbishops :: KnownNat n => Rule (Finite n, Finite n) Square
= withSeen diagonals nonattacking
nbishops
nqueens :: KnownNat n => Rule (Finite n, Finite n) Square
= nrooks <> nbishops nqueens
```

```
λ> printSolution (showGrid showSquare) (solve (nrooks @8) [])
Ambiguous, first solution:
X . . . . . . .
. X . . . . . .
. . X . . . . .
. . . X . . . .
. . . . X . . .
. . . . . X . .
. . . . . . X .
. . . . . . . X
λ> printSolution (showGrid showSquare) (solve (nbishops @8) [])
Ambiguous, first solution:
X . . . . . . .
X . . . . . . .
X . . . . . . .
X . . . . X . X
X . . . . X . X
X . . . . . . .
X . . . . . . .
X . . . . . . .
```

If you look at the solution to `nbishops`

, you might spot an issue. The object of the original *n* queens game is to place exactly *n* queens, but our backtracker’s goal is to just assign `Empty`

or `Piece`

to every square. In the case of `nbishops`

you could place as many as 14 bishops, but we’re not guiding the solver towards that point. It becomes especially clear if we try `nqueens`

:

```
λ> printSolution (showGrid showSquare) (solve (nqueens @8) [])
Ambiguous, first solution:
X . . . . . . .
. . . X . . . .
. X . . . . . .
. . . . X . . .
. . X . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
```

That won’t do at all. We *could* filter every solution at the *end* based on whether or not it has a queen in every column, but that’s more brute forcing than backtracking. Instead we’ll define a new combinator, called `constraint`

. It will place a constraint on a region by, when every cell in a region has been assigned a value, checking whether some condition holds for those values.

```
constraint :: Eq i => Sees i -> ([a] -> All) -> Rule i a
= go
constraint sees rel where
=
go f i a let f' i' = if i' == i then Just a else f i'
in maybe (All True) rel . traverse f' . Set.toList . sees $ i
```

And with that, we can reformulate `nqeens`

:

```
contains :: (Eq i, Eq a) => Sees i -> a -> Rule i a
= constraint sees (All . elem a)
contains sees a
nqueens2 :: KnownNat n => Rule (Finite n, Finite n) Square
= nrooks <> nbishops <> (column `contains` Piece) nqueens2
```

```
λ> printSolution (showGrid showSquare) (solve (nqueens2 @8) [])
Ambiguous, first solution:
X . . . . . . .
. . . . . . X .
. . . . X . . .
. . . . . . . X
. X . . . . . .
. . . X . . . .
. . . . . X . .
. . X . . . . .
```

And as expected, we get a proper solution again.

Let’s take a lesson from the Sudoku variants, and consider a variant of *n* queens in which the queens also cannot be within a knight’s move from one another:

```
λ> printSolution (showGrid showSquare) (solve (withSeen knight nonattacking <> nqueens2 @8) [])
No Solutions
```

Turns out it doesn’t actually have any solutions for *n* = 8… Instead we need to go to *n* = 10 (or 1), but only if we don’t also force a piece at (5,5):

```
λ> printSolution (showGrid showSquare) (solve (withSeen knight nonattacking <> nqueens2 @10) [])
Ambiguous, first solution:
. . . X . . . . . .
. . . . . . . X . .
X . . . . . . . . .
. . . . X . . . . .
. . . . . . . . X .
. X . . . . . . . .
. . . . . X . . . .
. . . . . . . . . X
. . X . . . . . . .
. . . . . . X . . .
λ> printSolution (showGrid showSquare) (solve (withSeen knight nonattacking <> nqueens2 @10) [((5, 5), Piece)])
No solutions
```

And finally, my new favorite kind of puzzle: Star Battle. In a Star Battle puzzle, the object is to place two stars in every row, column, and outlined region, such that no two stars touch, even diagonally.

It may initially seem tricky to express the outlined regions, but it’s simply another `Sees`

relation. Aside from that, we have all the tools we need to express the rules to star battle already.

```
starbattleRules :: KnownNat n => Sees (Finite n, Finite n) -> Rule (Finite n, Finite n) Square
=
starbattleRules regions
withSeen king nonattacking<> has2 regions
<> has2 column
<> has2 row
where
= constraint r (All . (== 2) . length . filter (== Piece))
has2 r
parseStarbattle :: (KnownNat n) => [String] -> Sees (Finite n, Finite n)
starbattle :: Sees (F10, F10)
=
starbattle
parseStarbattle"AAAAAABBBB",
[ "ACADABBEEE",
"ACCDDBEEEE",
"ACCDDBEEEF",
"ACGDDBEEEF",
"ACGDHHEEFF",
"AGGGHIIEEF",
"JGGGHIIEFF",
"JGGHHJIIFF",
"JJJJJJIIFF"
]
```

```
λ> printSolution (showGrid showSquare) (solve (starbattleRules starbattle) [])
. . . X . . . . X .
. X . . . . X . . .
. . . . X . . . X .
X . X . . . . . . .
. . . . . . . X . X
. . . X . X . . . .
. X . . . . . . . X
. . . . X . X . . .
X . X . . . . . . .
. . . . . X . X . .
```

And that’s how you solve a Star Battle.

If there is a point to this post, it would be that simple higher-order functions can get you *really* far. We were able to write a solver for a large family of puzzles, almost entirely without ever writing a data type or type class. I’m leaving the story of why that might be a good thing for another time.

Thanks for reading, criticism is welcome.

Thanks to [@cdepillabout](https://github.com/cdepillabout/), [@kayhide](https://github.com/kayhide/), and [@considerate](https://github.com/considerate) for proof-reading.

```
printSolution :: (Solution i a -> String) -> [Solution i a] -> IO ()
= putStrLn $ case sols of
printSolution pp sols -> "No solutions"
[] -> pp x
[x] : _) -> "Ambiguous, first solution:\n" <> pp x
(x
showGrid :: (Universe x, Universe y) => (a -> Char) -> Solution (x, y) a -> String
= ($ "") . unlines' $ showRow <$> universe
showGrid showA sol where
= showString . intersperse ' ' $ showA . sol . (,y) <$> universe
showRow y = foldr (.) id . intersperse (showChar '\n')
unlines'
showF9 :: F9 -> Char
= chr . (+ ord '1') . fromIntegral
showF9
parseSudoku :: [String] -> Givens (F9, F9) F9
= do
parseSudoku strs <- zip [0 ..] strs
(y, xs) Just d) <- zip [0 ..] (fromChar <$> filter (/= ' ') xs)
(x, pure ((x, y), d)
where
fromChar :: Char -> Maybe F9
fromChar c| c >= '1' && c <= '9' = Just . fromIntegral $ ord c - ord '1'
| otherwise = Nothing
parseStarbattle :: KnownNat n => [String] -> Sees (Finite n, Finite n)
= (groupPos M.!) . (posGroup M.!)
parseStarbattle strs where
= M.fromList assocs
posGroup = foldr (\(p, group) m -> M.insertWith (<>) group (Set.singleton p) m) mempty assocs
groupPos = do
assocs <- zip [0 ..] strs
(y, line) group) <- zip [0 ..] (filter (/= ' ') line)
(x, pure ((x, y), group)
```

If you’re thinking why we don’t just use

`Enum`

instead of`Ix`

, it’s because tuples don’t have`Enum`

instances, and we’re going to be using a lot of tuples.↩︎`Finite`

doesn’t actually have an`Ix`

instance yet, so for now you’ll have to import the`Data.Finite.Internal`

module and add a standalone`deriving instance (Ix (Finite n))`

.↩︎Once you get up to

*n*= 12 GHCi definitely starts to sputter. Compiling will make things orders of magnitude faster, but not so fast we can solve for large*n*.↩︎