-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Puzzles.Sudoku
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- The Sudoku solver, quintessential SMT solver example!
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Puzzles.Sudoku where

import Data.List  (transpose)
import Data.Maybe (fromJust)

import Data.SBV

-------------------------------------------------------------------
-- * Modeling Sudoku
-------------------------------------------------------------------
-- | A row is a sequence of 8-bit words, too large indeed for representing 1-9, but does not harm
type Row   = [SWord8]

-- | A Sudoku board is a sequence of 9 rows
type Board = [Row]

-- | Given a series of elements, make sure they are all different
-- and they all are numbers between 1 and 9
check :: [SWord8] -> SBool
check :: [SWord8] -> SBool
check [SWord8]
grp = [SBool] -> SBool
sAnd ([SBool] -> SBool) -> [SBool] -> SBool
forall a b. (a -> b) -> a -> b
$ [SWord8] -> SBool
forall a. EqSymbolic a => [a] -> SBool
distinct [SWord8]
grp SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: (SWord8 -> SBool) -> [SWord8] -> [SBool]
forall a b. (a -> b) -> [a] -> [b]
map SWord8 -> SBool
forall a. (OrdSymbolic a, Num a) => a -> SBool
rangeFine [SWord8]
grp
  where rangeFine :: a -> SBool
rangeFine a
x = a
x a -> a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> a
0 SBool -> SBool -> SBool
.&& a
x a -> a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= a
9

-- | Given a full Sudoku board, check that it is valid
valid :: Board -> SBool
valid :: Board -> SBool
valid Board
rows = [SBool] -> SBool
sAnd ([SBool] -> SBool) -> [SBool] -> SBool
forall a b. (a -> b) -> a -> b
$ Bool -> SBool
forall a. SymVal a => a -> SBV a
literal Bool
sizesOK SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: ([SWord8] -> SBool) -> Board -> [SBool]
forall a b. (a -> b) -> [a] -> [b]
map [SWord8] -> SBool
check (Board
rows Board -> Board -> Board
forall a. [a] -> [a] -> [a]
++ Board
columns Board -> Board -> Board
forall a. [a] -> [a] -> [a]
++ Board
squares)
  where sizesOK :: Bool
sizesOK = Board -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Board
rows Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
9 Bool -> Bool -> Bool
&& ([SWord8] -> Bool) -> Board -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\[SWord8]
r -> [SWord8] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord8]
r Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
9) Board
rows
        columns :: Board
columns = Board -> Board
forall a. [[a]] -> [[a]]
transpose Board
rows
        regions :: [Board]
regions = [Board] -> [Board]
forall a. [[a]] -> [[a]]
transpose [Int -> [SWord8] -> Board
forall a. Int -> [a] -> [[a]]
chunk Int
3 [SWord8]
row | [SWord8]
row <- Board
rows]
        squares :: Board
squares = [Board -> [SWord8]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat Board
sq | Board
sq <- Int -> Board -> [Board]
forall a. Int -> [a] -> [[a]]
chunk Int
3 ([Board] -> Board
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Board]
regions)]
        chunk :: Int -> [a] -> [[a]]
        chunk :: Int -> [a] -> [[a]]
chunk Int
_ [] = []
        chunk Int
i [a]
xs = let ([a]
f, [a]
r) = Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
i [a]
xs in [a]
f [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: Int -> [a] -> [[a]]
forall a. Int -> [a] -> [[a]]
chunk Int
i [a]
r

-- | A puzzle is a pair: First is the number of missing elements, second
-- is a function that given that many elements returns the final board.
type Puzzle = (Int, [SWord8] -> Board)

-------------------------------------------------------------------
-- * Solving Sudoku puzzles
-------------------------------------------------------------------

-- | Solve a given puzzle and print the results
sudoku :: Puzzle -> IO ()
sudoku :: Puzzle -> IO ()
sudoku p :: Puzzle
p@(Int
i, [SWord8] -> Board
f) = do String -> IO ()
putStrLn String
"Solving the puzzle.."
                     Either String (Bool, [Word8])
model <- SatResult -> Either String (Bool, [Word8])
forall a b.
(Modelable a, SatModel b) =>
a -> Either String (Bool, b)
getModelAssignment (SatResult -> Either String (Bool, [Word8]))
-> IO SatResult -> IO (Either String (Bool, [Word8]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` SymbolicT IO SBool -> IO SatResult
forall a. Provable a => a -> IO SatResult
sat ((Board -> SBool
valid (Board -> SBool) -> ([SWord8] -> Board) -> [SWord8] -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SWord8] -> Board
f) ([SWord8] -> SBool) -> SymbolicT IO [SWord8] -> SymbolicT IO SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Int -> SymbolicT IO [SWord8]
forall a. SymVal a => Int -> Symbolic [SBV a]
mkExistVars Int
i)
                     case Either String (Bool, [Word8])
model of
                       Right (Bool, [Word8])
sln -> Puzzle -> (Bool, [Word8]) -> IO ()
dispSolution Puzzle
p (Bool, [Word8])
sln
                       Left String
m    -> String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Unsolvable puzzle: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m

-- | Helper function to display results nicely, not really needed, but helps presentation
dispSolution :: Puzzle -> (Bool, [Word8]) -> IO ()
dispSolution :: Puzzle -> (Bool, [Word8]) -> IO ()
dispSolution (Int
i, [SWord8] -> Board
f) (Bool
_, [Word8]
fs)
  | Int
lmod Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
i = String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Impossible! Backend solver returned " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
lmod String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" values, was expecting: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  | Bool
True      = do String -> IO ()
putStrLn String
"Final board:"
                   ([SWord8] -> IO ()) -> Board -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [SWord8] -> IO ()
forall (t :: * -> *) a.
(Foldable t, Show a, SymVal a) =>
t (SBV a) -> IO ()
printRow Board
final
                   String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Valid Check: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBool -> String
forall a. Show a => a -> String
show (Board -> SBool
valid Board
final)
                   String -> IO ()
putStrLn String
"Done."
  where lmod :: Int
lmod = [Word8] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Word8]
fs
        final :: Board
final = [SWord8] -> Board
f ((Word8 -> SWord8) -> [Word8] -> [SWord8]
forall a b. (a -> b) -> [a] -> [b]
map Word8 -> SWord8
forall a. SymVal a => a -> SBV a
literal [Word8]
fs)
        printRow :: t (SBV a) -> IO ()
printRow t (SBV a)
r = String -> IO ()
putStr String
"   " IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (SBV a -> IO ()) -> t (SBV a) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\SBV a
x -> String -> IO ()
putStr (a -> String
forall a. Show a => a -> String
show (Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJust (SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
x)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ")) t (SBV a)
r IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
putStrLn String
""

-- | Find all solutions to a puzzle
solveAll :: Puzzle -> IO ()
solveAll :: Puzzle -> IO ()
solveAll p :: Puzzle
p@(Int
i, [SWord8] -> Board
f) = do String -> IO ()
putStrLn String
"Finding all solutions.."
                       AllSatResult
res <- SymbolicT IO SBool -> IO AllSatResult
forall a. Provable a => a -> IO AllSatResult
allSat (SymbolicT IO SBool -> IO AllSatResult)
-> SymbolicT IO SBool -> IO AllSatResult
forall a b. (a -> b) -> a -> b
$ (Board -> SBool
valid (Board -> SBool) -> ([SWord8] -> Board) -> [SWord8] -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SWord8] -> Board
f) ([SWord8] -> SBool) -> SymbolicT IO [SWord8] -> SymbolicT IO SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Int -> SymbolicT IO [SWord8]
forall a. SymVal a => Int -> Symbolic [SBV a]
mkExistVars Int
i
                       Int
cnt <- ([(Bool, [Word8])] -> [(Bool, [Word8])])
-> (Int -> (Bool, [Word8]) -> IO ()) -> AllSatResult -> IO Int
forall a.
SatModel a =>
([(Bool, a)] -> [(Bool, a)])
-> (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
displayModels [(Bool, [Word8])] -> [(Bool, [Word8])]
forall a. a -> a
id Int -> (Bool, [Word8]) -> IO ()
forall a. Show a => a -> (Bool, [Word8]) -> IO ()
disp AllSatResult
res
                       String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Found: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
cnt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" solution(s)."
   where disp :: a -> (Bool, [Word8]) -> IO ()
disp a
n (Bool, [Word8])
s = do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Solution #" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n
                       Puzzle -> (Bool, [Word8]) -> IO ()
dispSolution Puzzle
p (Bool, [Word8])
s

-------------------------------------------------------------------
-- * Example boards
-------------------------------------------------------------------

-- | Find an arbitrary good board
puzzle0 :: Puzzle
puzzle0 :: Puzzle
puzzle0 = (Int
81, [SWord8] -> Board
forall a. [a] -> [[a]]
f)
  where f :: [a] -> [[a]]
f   [ a
a1, a
a2, a
a3, a
a4, a
a5, a
a6, a
a7, a
a8, a
a9,
              a
b1, a
b2, a
b3, a
b4, a
b5, a
b6, a
b7, a
b8, a
b9,
              a
c1, a
c2, a
c3, a
c4, a
c5, a
c6, a
c7, a
c8, a
c9,
              a
d1, a
d2, a
d3, a
d4, a
d5, a
d6, a
d7, a
d8, a
d9,
              a
e1, a
e2, a
e3, a
e4, a
e5, a
e6, a
e7, a
e8, a
e9,
              a
f1, a
f2, a
f3, a
f4, a
f5, a
f6, a
f7, a
f8, a
f9,
              a
g1, a
g2, a
g3, a
g4, a
g5, a
g6, a
g7, a
g8, a
g9,
              a
h1, a
h2, a
h3, a
h4, a
h5, a
h6, a
h7, a
h8, a
h9,
              a
i1, a
i2, a
i3, a
i4, a
i5, a
i6, a
i7, a
i8, a
i9 ]
         = [ [a
a1, a
a2, a
a3, a
a4, a
a5, a
a6, a
a7, a
a8, a
a9],
             [a
b1, a
b2, a
b3, a
b4, a
b5, a
b6, a
b7, a
b8, a
b9],
             [a
c1, a
c2, a
c3, a
c4, a
c5, a
c6, a
c7, a
c8, a
c9],
             [a
d1, a
d2, a
d3, a
d4, a
d5, a
d6, a
d7, a
d8, a
d9],
             [a
e1, a
e2, a
e3, a
e4, a
e5, a
e6, a
e7, a
e8, a
e9],
             [a
f1, a
f2, a
f3, a
f4, a
f5, a
f6, a
f7, a
f8, a
f9],
             [a
g1, a
g2, a
g3, a
g4, a
g5, a
g6, a
g7, a
g8, a
g9],
             [a
h1, a
h2, a
h3, a
h4, a
h5, a
h6, a
h7, a
h8, a
h9],
             [a
i1, a
i2, a
i3, a
i4, a
i5, a
i6, a
i7, a
i8, a
i9] ]
        f [a]
_ = String -> [[a]]
forall a. HasCallStack => String -> a
error String
"puzzle0 needs exactly 81 elements!"

-- | A random puzzle, found on the internet..
puzzle1 :: Puzzle
puzzle1 :: Puzzle
puzzle1 = (Int
49, [SWord8] -> Board
forall a. Num a => [a] -> [[a]]
f)
  where f :: [a] -> [[a]]
f   [ a
a1,     a
a3, a
a4, a
a5, a
a6, a
a7,     a
a9,
              a
b1, a
b2, a
b3,             a
b7, a
b8, a
b9,
                  a
c2,     a
c4, a
c5, a
c6,     a
c8,
                      a
d3,     a
d5,     a
d7,
              a
e1, a
e2,     a
e4, a
e5, a
e6,     a
e8, a
e9,
                      a
f3,     a
f5,     a
f7,
                  a
g2,     a
g4, a
g5, a
g6,     a
g8,
              a
h1, a
h2, a
h3,             a
h7, a
h8, a
h9,
              a
i1,     a
i3, a
i4, a
i5, a
i6, a
i7,     a
i9 ]
         = [ [a
a1,  a
6, a
a3, a
a4, a
a5, a
a6, a
a7,  a
1, a
a9],
             [a
b1, a
b2, a
b3,  a
6,  a
5,  a
1, a
b7, a
b8, a
b9],
             [ a
1, a
c2,  a
7, a
c4, a
c5, a
c6,  a
6, a
c8,  a
2],
             [ a
6,  a
2, a
d3,  a
3, a
d5,  a
5, a
d7,  a
9,  a
4],
             [a
e1, a
e2,  a
3, a
e4, a
e5, a
e6,  a
2, a
e8, a
e9],
             [ a
4,  a
8, a
f3,  a
9, a
f5,  a
7, a
f7,  a
3,  a
6],
             [ a
9, a
g2,  a
6, a
g4, a
g5, a
g6,  a
4, a
g8,  a
8],
             [a
h1, a
h2, a
h3,  a
7,  a
9,  a
4, a
h7, a
h8, a
h9],
             [a
i1,  a
5, a
i3, a
i4, a
i5, a
i6, a
i7,  a
7, a
i9] ]
        f [a]
_ = String -> [[a]]
forall a. HasCallStack => String -> a
error String
"puzzle1 needs exactly 49 elements!"

-- | Another random puzzle, found on the internet..
puzzle2 :: Puzzle
puzzle2 :: Puzzle
puzzle2 = (Int
55, [SWord8] -> Board
forall a. Num a => [a] -> [[a]]
f)
  where f :: [a] -> [[a]]
f   [     a
a2,     a
a4, a
a5, a
a6, a
a7,     a
a9,
              a
b1, a
b2,     a
b4,         a
b7, a
b8, a
b9,
              a
c1,     a
c3, a
c4, a
c5, a
c6, a
c7, a
c8, a
c9,
                  a
d2, a
d3, a
d4,             a
d8, a
d9,
              a
e1,     a
e3,     a
e5,     a
e7,     a
e9,
              a
f1, a
f2,             a
f6, a
f7, a
f8,
              a
g1, a
g2, a
g3, a
g4, a
g5, a
g6, a
g7,     a
g9,
              a
h1, a
h2, a
h3,         a
h6,     a
h8, a
h9,
              a
i1,     a
i3, a
i4, a
i5, a
i6,     a
i8     ]
         = [ [ a
1, a
a2,  a
3, a
a4, a
a5, a
a6, a
a7,  a
8, a
a9],
             [a
b1, a
b2,  a
6, a
b4,  a
4,  a
8, a
b7, a
b8, a
b9],
             [a
c1,  a
4, a
c3, a
c4, a
c5, a
c6, a
c7, a
c8, a
c9],
             [ a
2, a
d2, a
d3, a
d4,  a
9,  a
6,  a
1, a
d8, a
d9],
             [a
e1,  a
9, a
e3,  a
8, a
e5,  a
1, a
e7,  a
4, a
e9],
             [a
f1, a
f2,  a
4,  a
3,  a
2, a
f6, a
f7, a
f8,  a
8],
             [a
g1, a
g2, a
g3, a
g4, a
g5, a
g6, a
g7,  a
7, a
g9],
             [a
h1, a
h2, a
h3,  a
1,  a
5, a
h6,  a
4, a
h8, a
h9],
             [a
i1,  a
6, a
i3, a
i4, a
i5, a
i6,  a
2, a
i8,  a
3] ]
        f [a]
_ = String -> [[a]]
forall a. HasCallStack => String -> a
error String
"puzzle2 needs exactly 55 elements!"

-- | Another random puzzle, found on the internet..
puzzle3 :: Puzzle
puzzle3 :: Puzzle
puzzle3 = (Int
56, [SWord8] -> Board
forall a. Num a => [a] -> [[a]]
f)
  where f :: [a] -> [[a]]
f   [     a
a2, a
a3, a
a4,     a
a6,     a
a8, a
a9,
                  a
b2,     a
b4, a
b5, a
b6, a
b7, a
b8, a
b9,
              a
c1, a
c2, a
c3, a
c4,     a
c6, a
c7,     a
c9,
              a
d1,     a
d3,     a
d5,     a
d7,     a
d9,
                  a
e2, a
e3, a
e4,     a
e6, a
e7, a
e8,
              a
f1,     a
f3,     a
f5,     a
f7,     a
f9,
              a
g1,     a
g3, a
g4,     a
g6, a
g7, a
g8, a
g9,
              a
h1, a
h2, a
h3, a
h4, a
h5, a
h6,     a
h8,
              a
i1, a
i2,     a
i4,     a
i6, a
i7, a
i8     ]
         = [ [ a
6, a
a2, a
a3, a
a4,  a
1, a
a6,  a
5, a
a8, a
a9],
             [ a
8, a
b2,  a
3, a
b4, a
b5, a
b6, a
b7, a
b8, a
b9],
             [a
c1, a
c2, a
c3, a
c4,  a
6, a
c6, a
c7,  a
2, a
c9],
             [a
d1,  a
3, a
d3,  a
1, a
d5,  a
8, a
d7,  a
9, a
d9],
             [ a
1, a
e2, a
e3, a
e4,  a
9, a
e6, a
e7, a
e8,  a
4],
             [a
f1,  a
5, a
f3,  a
2, a
f5,  a
3, a
f7,  a
1, a
f9],
             [a
g1,  a
7, a
g3, a
g4,  a
3, a
g6, a
g7, a
g8, a
g9],
             [a
h1, a
h2, a
h3, a
h4, a
h5, a
h6,  a
3, a
h8,  a
6],
             [a
i1, a
i2,  a
4, a
i4,  a
5, a
i6, a
i7, a
i8,  a
9] ]
        f [a]
_ = String -> [[a]]
forall a. HasCallStack => String -> a
error String
"puzzle3 needs exactly 56 elements!"

-- | According to the web, this is the toughest 
-- sudoku puzzle ever.. It even has a name: Al Escargot:
-- <http://zonkedyak.blogspot.com/2006/11/worlds-hardest-sudoku-puzzle-al.html>
puzzle4 :: Puzzle
puzzle4 :: Puzzle
puzzle4 = (Int
58, [SWord8] -> Board
forall a. Num a => [a] -> [[a]]
f)
  where f :: [a] -> [[a]]
f   [     a
a2, a
a3, a
a4, a
a5,     a
a7,     a
a9,
              a
b1,     a
b3, a
b4,     a
b6, a
b7, a
b8,
              a
c1, a
c2,         a
c5, a
c6,     a
c8, a
c9,
              a
d1, a
d2,         a
d5, a
d6,     a
d8, a
d9,
              a
e1,     a
e3, a
e4,     a
e6, a
e7, a
e8,
                  a
f2, a
f3, a
f4, a
f5,     a
f7, a
f8, a
f9,
                  a
g2, a
g3, a
g4, a
g5, a
g6, a
g7,     a
g9,
              a
h1,     a
h3, a
h4, a
h5, a
h6, a
h7, a
h8,
              a
i1, a
i2,     a
i4, a
i5, a
i6,     a
i8, a
i9 ]
         = [ [ a
1, a
a2, a
a3, a
a4, a
a5,  a
7, a
a7,  a
9, a
a9],
             [a
b1,  a
3, a
b3, a
b4,  a
2, a
b6, a
b7, a
b8,  a
8],
             [a
c1, a
c2,  a
9,  a
6, a
c5, a
c6,  a
5, a
c8, a
c9],
             [a
d1, a
d2,  a
5,  a
3, a
d5, a
d6,  a
9, a
d8, a
d9],
             [a
e1,  a
1, a
e3, a
e4,  a
8, a
e6, a
e7, a
e8,  a
2],
             [ a
6, a
f2, a
f3, a
f4, a
f5,  a
4, a
f7, a
f8, a
f9],
             [ a
3, a
g2, a
g3, a
g4, a
g5, a
g6, a
g7,  a
1, a
g9],
             [a
h1,  a
4, a
h3, a
h4, a
h5, a
h6, a
h7, a
h8,  a
7],
             [a
i1, a
i2,  a
7, a
i4, a
i5, a
i6,  a
3, a
i8, a
i9] ]
        f [a]
_ = String -> [[a]]
forall a. HasCallStack => String -> a
error String
"puzzle4 needs exactly 58 elements!"

-- | This one has been called diabolical, apparently
puzzle5 :: Puzzle
puzzle5 :: Puzzle
puzzle5 = (Int
53, [SWord8] -> Board
forall a. Num a => [a] -> [[a]]
f)
  where f :: [a] -> [[a]]
f   [ a
a1,     a
a3,     a
a5, a
a6,         a
a9,
              a
b1,         a
b4, a
b5,     a
b7,     a
b9,
                  a
c2,     a
c4, a
c5, a
c6, a
c7, a
c8, a
c9,
              a
d1, a
d2,     a
d4,     a
d6, a
d7, a
d8,
              a
e1, a
e2, a
e3,     a
e5,     a
e7, a
e8, a
e9,
                  a
f2, a
f3, a
f4,     a
f6,     a
f8, a
f9,
              a
g1, a
g2, a
g3, a
g4, a
g5, a
g6,     a
g8,
              a
h1,     a
h3,     a
h5, a
h6,         a
h9,
              a
i1,         a
i4, a
i5,     a
i7,     a
i9 ]
         = [ [a
a1,  a
9, a
a3,  a
7, a
a5, a
a6,  a
8,  a
6, a
a9],
             [a
b1,  a
3,  a
1, a
b4, a
b5,  a
5, a
b7,  a
2, a
b9],
             [ a
8, a
c2,  a
6, a
c4, a
c5, a
c6, a
c7, a
c8, a
c9],
             [a
d1, a
d2,  a
7, a
d4,  a
5, a
d6, a
d7, a
d8,  a
6],
             [a
e1, a
e2, a
e3,  a
3, a
e5,  a
7, a
e7, a
e8, a
e9],
             [ a
5, a
f2, a
f3, a
f4,  a
1, a
f6,  a
7, a
f8, a
f9],
             [a
g1, a
g2, a
g3, a
g4, a
g5, a
g6,  a
1, a
g8,  a
9],
             [a
h1,  a
2, a
h3,  a
6, a
h5, a
h6,  a
3,  a
5, a
h9],
             [a
i1,  a
5,  a
4, a
i4, a
i5,  a
8, a
i7,  a
7, a
i9] ]
        f [a]
_ = String -> [[a]]
forall a. HasCallStack => String -> a
error String
"puzzle5 needs exactly 53 elements!"

-- | The following is nefarious according to
-- <http://haskell.org/haskellwiki/Sudoku>
puzzle6 :: Puzzle
puzzle6 :: Puzzle
puzzle6 = (Int
64, [SWord8] -> Board
forall a. Num a => [a] -> [[a]]
f)
  where f :: [a] -> [[a]]
f   [ a
a1, a
a2, a
a3, a
a4,     a
a6, a
a7,     a
a9,
              a
b1,     a
b3, a
b4, a
b5, a
b6, a
b7, a
b8, a
b9,
              a
c1, a
c2,     a
c4, a
c5, a
c6, a
c7, a
c8, a
c9,
              a
d1,     a
d3, a
d4, a
d5, a
d6,     a
d8,
                  a
e2, a
e3, a
e4,     a
e6, a
e7, a
e8, a
e9,
              a
f1, a
f2, a
f3, a
f4, a
f5, a
f6,     a
f8, a
f9,
              a
g1, a
g2,         a
g5,     a
g7, a
g8, a
g9,
                  a
h2, a
h3,     a
h5, a
h6,     a
h8, a
h9,
              a
i1, a
i2, a
i3, a
i4, a
i5, a
i6, a
i7,     a
i9  ]
         = [ [a
a1, a
a2, a
a3, a
a4,  a
6, a
a6, a
a7,  a
8, a
a9],
             [a
b1,  a
2, a
b3, a
b4, a
b5, a
b6, a
b7, a
b8, a
b9],
             [a
c1, a
c2,  a
1, a
c4, a
c5, a
c6, a
c7, a
c8, a
c9],
             [a
d1,  a
7, a
d3, a
d4, a
d5, a
d6,  a
1, a
d8,  a
2],
             [ a
5, a
e2, a
e3, a
e4,  a
3, a
e6, a
e7, a
e8, a
e9],
             [a
f1, a
f2, a
f3, a
f4, a
f5, a
f6,  a
4, a
f8, a
f9],
             [a
g1, a
g2,  a
4,  a
2, a
g5,  a
1, a
g7, a
g8, a
g9],
             [ a
3, a
h2, a
h3,  a
7, a
h5, a
h6,  a
6, a
h8, a
h9],
             [a
i1, a
i2, a
i3, a
i4, a
i5, a
i6, a
i7,  a
5, a
i9] ]
        f [a]
_ = String -> [[a]]
forall a. HasCallStack => String -> a
error String
"puzzle6 needs exactly 64 elements!"

-- | Solve them all, this takes a fraction of a second to run for each case
allPuzzles :: IO ()
allPuzzles :: IO ()
allPuzzles = (Puzzle -> IO ()) -> [Puzzle] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Puzzle -> IO ()
sudoku [Puzzle
puzzle0, Puzzle
puzzle1, Puzzle
puzzle2, Puzzle
puzzle3, Puzzle
puzzle4, Puzzle
puzzle5, Puzzle
puzzle6]