-----------------------------------------------------------------------------
-- |
-- 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 grp :: [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 x :: a
x = a
x a -> a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> 0 SBool -> SBool -> SBool
.&& a
x a -> a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= 9

-- | Given a full Sudoku board, check that it is valid
valid :: Board -> SBool
valid :: Board -> SBool
valid rows :: 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
== 9 Bool -> Bool -> Bool
&& ([SWord8] -> Bool) -> Board -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\r :: [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
== 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 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 3 ([Board] -> Board
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Board]
regions)]
        chunk :: Int -> [a] -> [[a]]
        chunk :: Int -> [a] -> [[a]]
chunk _ [] = []
        chunk i :: Int
i xs :: [a]
xs = let (f :: [a]
f, r :: [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@(i :: Int
i, f :: [SWord8] -> Board
f) = do String -> IO ()
putStrLn "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 sln :: (Bool, [Word8])
sln -> Puzzle -> (Bool, [Word8]) -> IO ()
dispSolution Puzzle
p (Bool, [Word8])
sln
                       Left m :: String
m    -> String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "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 (i :: Int
i, f :: [SWord8] -> Board
f) (_, fs :: [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
$ "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]
++ " 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 "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
$ "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 "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 r :: t (SBV a)
r = String -> IO ()
putStr "   " 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_ (\x :: 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]
++ " ")) t (SBV a)
r IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
putStrLn ""

-- | Find all solutions to a puzzle
solveAll :: Puzzle -> IO ()
solveAll :: Puzzle -> IO ()
solveAll p :: Puzzle
p@(i :: Int
i, f :: [SWord8] -> Board
f) = do String -> IO ()
putStrLn "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
$ "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]
++ " solution(s)."
   where disp :: a -> (Bool, [Word8]) -> IO ()
disp n :: a
n s :: (Bool, [Word8])
s = do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "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 = (81, [SWord8] -> Board
forall a. [a] -> [[a]]
f)
  where f :: [a] -> [[a]]
f   [ a1 :: a
a1, a2 :: a
a2, a3 :: a
a3, a4 :: a
a4, a5 :: a
a5, a6 :: a
a6, a7 :: a
a7, a8 :: a
a8, a9 :: a
a9,
              b1 :: a
b1, b2 :: a
b2, b3 :: a
b3, b4 :: a
b4, b5 :: a
b5, b6 :: a
b6, b7 :: a
b7, b8 :: a
b8, b9 :: a
b9,
              c1 :: a
c1, c2 :: a
c2, c3 :: a
c3, c4 :: a
c4, c5 :: a
c5, c6 :: a
c6, c7 :: a
c7, c8 :: a
c8, c9 :: a
c9,
              d1 :: a
d1, d2 :: a
d2, d3 :: a
d3, d4 :: a
d4, d5 :: a
d5, d6 :: a
d6, d7 :: a
d7, d8 :: a
d8, d9 :: a
d9,
              e1 :: a
e1, e2 :: a
e2, e3 :: a
e3, e4 :: a
e4, e5 :: a
e5, e6 :: a
e6, e7 :: a
e7, e8 :: a
e8, e9 :: a
e9,
              f1 :: a
f1, f2 :: a
f2, f3 :: a
f3, f4 :: a
f4, f5 :: a
f5, f6 :: a
f6, f7 :: a
f7, f8 :: a
f8, f9 :: a
f9,
              g1 :: a
g1, g2 :: a
g2, g3 :: a
g3, g4 :: a
g4, g5 :: a
g5, g6 :: a
g6, g7 :: a
g7, g8 :: a
g8, g9 :: a
g9,
              h1 :: a
h1, h2 :: a
h2, h3 :: a
h3, h4 :: a
h4, h5 :: a
h5, h6 :: a
h6, h7 :: a
h7, h8 :: a
h8, h9 :: a
h9,
              i1 :: a
i1, i2 :: a
i2, i3 :: a
i3, i4 :: a
i4, i5 :: a
i5, i6 :: a
i6, i7 :: a
i7, i8 :: a
i8, i9 :: 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 _ = String -> [[a]]
forall a. HasCallStack => String -> a
error "puzzle0 needs exactly 81 elements!"

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

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

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

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

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