# Monoidal Puzzle Solving

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.

# The 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]
universe = range (minBound, maxBound)``````

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]
solve rule given = go (filter (`Map.notMember` m0) universe) m0
where
m0 :: Map i a
m0 = Map.fromList given
go :: [i] -> Map i a -> [Solution i a]
go [] m = pure (m Map.!)
go (i : is) m = do
a <- universe
guard . getAll \$ rule (m Map.!?) i a
go is (M.insert i a m)``````

### n Queens

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 integers2.

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)
nqueens f x y = All . and \$ do
qx <- universe
qy <- toList (f qx)
[qy /= y, difference qx x /= difference qy y]

difference :: KnownNat n => Finite n -> Finite n -> Finite n
difference a b = max a b - min a b``````

If we now ask GHCi how many ways there are to place the n queens on the board, we get the expected answers3:

``````λ> 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.

# Sudoku

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)
row (_, y) = Set.fromList \$ (,y) <\$> universe

column :: (Universe y, Ord x) => Sees (x, y)
column (x, _) = Set.fromList \$ (x,) <\$> universe

type F9 = Finite 9

box :: Sees (F9, F9)
box = Set.fromList . bitraverse (group 3) (group 3)
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
unique = (All .) . notElem

withSeen :: forall i a. Sees i -> Relation a -> Rule i a
withSeen sees rel = go
where
go :: Solution i (Maybe a) -> i -> a -> All
go f i a = rel a \$ Set.toList (sees i) >>= toList . f``````

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

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

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``````

### Anti-Knight Sudoku

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)
fromOffsets offsets (x, y) = Set.fromList \$ do
(dx, dy) <- offsets
(,) <\$> asInt (+ dx) x <*> asInt (+ dy) y
where
asInt f = maybe [] pure . packFinite . f . getFinite

knight :: KnownNat n => Sees (Finite n, Finite n)
knight = fromOffsets \$ [(2, 1), (1, 2)] >>= bitraverse f f
where
f x = [x, -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 . .  . . ."
]

antiknightRules = sudokuRules <> withSeen knight unique``````

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``````

### Miracle Sudoku

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
• Antiking
• No two consecutive digits can be orthogonally adjacent
``````miracleSudoku =
parseSudoku
[ ". . .  . . .  . . .",
". . .  . . .  . . .",
". . .  . . .  . . .",
". . .  . . .  . . .",
". . 1  . . .  . . .",
". . .  . . .  2 . .",
". . .  . . .  . . .",
". . .  . . .  . . .",
". . .  . . .  . . ."
]

miracleRules =
sudokuRules
<> withSeen (knight <> king) unique

king :: KnownNat n => Sees (Finite n, Finite n)
king = fromOffsets \$ (,) <\$> [-1 .. 1] <*> [-1 .. 1]

adjacent :: KnownNat n => Sees (Finite n, Finite n)
adjacent = fromOffsets [(0, -1), (0, 1), (1, 0), (-1, 0)]

noConsecutive :: KnownNat n => Relation (Finite n)
noConsecutive n = All . all ((/= 1) . difference 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.

# A Few Other Puzzles

### n Queens, Bishops, and Rooks

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
nonattacking Empty _ = All True
nonattacking Piece xs = All (notElem Piece xs)

diagonals :: KnownNat n => Sees (Finite n, Finite n)
diagonals (x, y) = Set.fromList \$ do
d <- universe
dx <- [x - d, x + d]
let dy = y - d
guard \$ difference x dx == difference y dy
pure (dx, dy)

nrooks :: KnownNat n => Rule (Finite n, Finite n) Square
nrooks = withSeen (row <> column) nonattacking

nbishops :: KnownNat n => Rule (Finite n, Finite n) Square
nbishops = withSeen diagonals nonattacking

nqueens :: KnownNat n => Rule (Finite n, Finite n) Square
nqueens = nrooks <> nbishops``````
``````λ> 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
constraint sees rel = go
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
contains sees a = constraint sees (All . elem a)

nqueens2 :: KnownNat n => Rule (Finite n, Finite n) Square
nqueens2 = nrooks <> nbishops <> (column `contains` Piece)``````
``````λ> 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.

### nti-knight Queens

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``````

### Star Battle

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
has2 r = constraint r (All . (== 2) . length . filter (== Piece))

parseStarbattle :: (KnownNat n) => [String] -> Sees (Finite n, Finite n)

starbattle :: Sees (F10, F10)
starbattle =
parseStarbattle
[ "AAAAAABBBB",
"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.

# Conclusion

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.

# Appendix: Omitted Code

``````printSolution :: (Solution i a -> String) -> [Solution i a] -> IO ()
printSolution pp sols = putStrLn \$ case sols of
[] -> "No solutions"
[x] -> pp x
(x : _) -> "Ambiguous, first solution:\n" <> pp x

showGrid :: (Universe x, Universe y) => (a -> Char) -> Solution (x, y) a -> String
showGrid showA sol = (\$ "") . unlines' \$ showRow <\$> universe
where
showRow y = showString . intersperse ' ' \$ showA . sol . (,y) <\$> universe
unlines' = foldr (.) id . intersperse (showChar '\n')

showF9 :: F9 -> Char
showF9 = chr . (+ ord '1') . fromIntegral

parseSudoku :: [String] -> Givens (F9, F9) F9
parseSudoku strs = do
(y, xs) <- zip [0 ..] strs
(x, Just d) <- zip [0 ..] (fromChar <\$> filter (/= ' ') xs)
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)
parseStarbattle strs = (groupPos M.!) . (posGroup M.!)
where
posGroup = M.fromList assocs
groupPos = foldr (\(p, group) m -> M.insertWith (<>) group (Set.singleton p) m) mempty assocs
assocs = do
(y, line) <- zip [0 ..] strs
(x, group) <- zip [0 ..] (filter (/= ' ') line)
pure ((x, y), group)``````

1. 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.↩︎

2. `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))`.↩︎

3. 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.↩︎