Monoidal Puzzle Solving

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.

1 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¹ 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)

1.1 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 integers².

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 answers³:

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

2 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)]

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

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 ."
    ]

2.1 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:

2.2 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

miracleSudoku =
  parseSudoku
    [ ". . .  . . .  . . .",
      ". . .  . . .  . . .",
      ". . .  . . .  . . .",
      ". . .  . . .  . . .",
      ". . 1  . . .  . . .",
      ". . .  . . .  2 . .",
      ". . .  . . .  . . .",
      ". . .  . . .  . . .",
      ". . .  . . .  . . ."
    ]

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

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.

3 A Few Other Puzzles

3.1 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

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:

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

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)

3.2 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:

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):

3.3 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",
      "ACADABBEEE",
      "ACCDDBEEEE",
      "ACCDDBEEEF",
      "ACGDDBEEEF",
      "ACGDHHEEFF",
      "AGGGHIIEEF",
      "JGGGHIIEFF",
      "JGGHHJIIFF",
      "JJJJJJIIFF"
    ]

4 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 to [@cdepillabout](https://github.com/cdepillabout/), [@kayhide](https://github.com/kayhide/), and [@considerate](https://github.com/considerate) for proof-reading.

5 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)

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