----------------------------------------------------------------------------- -- | -- 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! ----------------------------------------------------------------------------- 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 grp = sAnd \$ distinct grp : map rangeFine grp where rangeFine x = x .> 0 .&& x .<= 9 -- | Given a full Sudoku board, check that it is valid valid :: Board -> SBool valid rows = sAnd \$ literal sizesOK : map check (rows ++ columns ++ squares) where sizesOK = length rows == 9 && all (\r -> length r == 9) rows columns = transpose rows regions = transpose [chunk 3 row | row <- rows] squares = [concat sq | sq <- chunk 3 (concat regions)] chunk :: Int -> [a] -> [[a]] chunk _ [] = [] chunk i xs = let (f, r) = splitAt i xs in f : chunk i 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 p@(i, f) = do putStrLn "Solving the puzzle.." model <- getModelAssignment `fmap` sat ((valid . f) `fmap` mkExistVars i) case model of Right sln -> dispSolution p sln Left m -> putStrLn \$ "Unsolvable puzzle: " ++ m -- | Helper function to display results nicely, not really needed, but helps presentation dispSolution :: Puzzle -> (Bool, [Word8]) -> IO () dispSolution (i, f) (_, fs) | lmod /= i = error \$ "Impossible! Backend solver returned " ++ show lmod ++ " values, was expecting: " ++ show i | True = do putStrLn "Final board:" mapM_ printRow final putStrLn \$ "Valid Check: " ++ show (valid final) putStrLn "Done." where lmod = length fs final = f (map literal fs) printRow r = putStr " " >> mapM_ (\x -> putStr (show (fromJust (unliteral x)) ++ " ")) r >> putStrLn "" -- | Find all solutions to a puzzle solveAll :: Puzzle -> IO () solveAll p@(i, f) = do putStrLn "Finding all solutions.." res <- allSat \$ (valid . f) `fmap` mkExistVars i cnt <- displayModels disp res putStrLn \$ "Found: " ++ show cnt ++ " solution(s)." where disp n s = do putStrLn \$ "Solution #" ++ show n dispSolution p s ------------------------------------------------------------------- -- * Example boards ------------------------------------------------------------------- -- | Find an arbitrary good board puzzle0 :: Puzzle puzzle0 = (81, f) where f [ a1, a2, a3, a4, a5, a6, a7, a8, a9, b1, b2, b3, b4, b5, b6, b7, b8, b9, c1, c2, c3, c4, c5, c6, c7, c8, c9, d1, d2, d3, d4, d5, d6, d7, d8, d9, e1, e2, e3, e4, e5, e6, e7, e8, e9, f1, f2, f3, f4, f5, f6, f7, f8, f9, g1, g2, g3, g4, g5, g6, g7, g8, g9, h1, h2, h3, h4, h5, h6, h7, h8, h9, i1, i2, i3, i4, i5, i6, i7, i8, i9 ] = [ [a1, a2, a3, a4, a5, a6, a7, a8, a9], [b1, b2, b3, b4, b5, b6, b7, b8, b9], [c1, c2, c3, c4, c5, c6, c7, c8, c9], [d1, d2, d3, d4, d5, d6, d7, d8, d9], [e1, e2, e3, e4, e5, e6, e7, e8, e9], [f1, f2, f3, f4, f5, f6, f7, f8, f9], [g1, g2, g3, g4, g5, g6, g7, g8, g9], [h1, h2, h3, h4, h5, h6, h7, h8, h9], [i1, i2, i3, i4, i5, i6, i7, i8, i9] ] f _ = error "puzzle0 needs exactly 81 elements!" -- | A random puzzle, found on the internet.. puzzle1 :: Puzzle puzzle1 = (49, f) where f [ a1, a3, a4, a5, a6, a7, a9, b1, b2, b3, b7, b8, b9, c2, c4, c5, c6, c8, d3, d5, d7, e1, e2, e4, e5, e6, e8, e9, f3, f5, f7, g2, g4, g5, g6, g8, h1, h2, h3, h7, h8, h9, i1, i3, i4, i5, i6, i7, i9 ] = [ [a1, 6, a3, a4, a5, a6, a7, 1, a9], [b1, b2, b3, 6, 5, 1, b7, b8, b9], [ 1, c2, 7, c4, c5, c6, 6, c8, 2], [ 6, 2, d3, 3, d5, 5, d7, 9, 4], [e1, e2, 3, e4, e5, e6, 2, e8, e9], [ 4, 8, f3, 9, f5, 7, f7, 3, 6], [ 9, g2, 6, g4, g5, g6, 4, g8, 8], [h1, h2, h3, 7, 9, 4, h7, h8, h9], [i1, 5, i3, i4, i5, i6, i7, 7, i9] ] f _ = error "puzzle1 needs exactly 49 elements!" -- | Another random puzzle, found on the internet.. puzzle2 :: Puzzle puzzle2 = (55, f) where f [ a2, a4, a5, a6, a7, a9, b1, b2, b4, b7, b8, b9, c1, c3, c4, c5, c6, c7, c8, c9, d2, d3, d4, d8, d9, e1, e3, e5, e7, e9, f1, f2, f6, f7, f8, g1, g2, g3, g4, g5, g6, g7, g9, h1, h2, h3, h6, h8, h9, i1, i3, i4, i5, i6, i8 ] = [ [ 1, a2, 3, a4, a5, a6, a7, 8, a9], [b1, b2, 6, b4, 4, 8, b7, b8, b9], [c1, 4, c3, c4, c5, c6, c7, c8, c9], [ 2, d2, d3, d4, 9, 6, 1, d8, d9], [e1, 9, e3, 8, e5, 1, e7, 4, e9], [f1, f2, 4, 3, 2, f6, f7, f8, 8], [g1, g2, g3, g4, g5, g6, g7, 7, g9], [h1, h2, h3, 1, 5, h6, 4, h8, h9], [i1, 6, i3, i4, i5, i6, 2, i8, 3] ] f _ = error "puzzle2 needs exactly 55 elements!" -- | Another random puzzle, found on the internet.. puzzle3 :: Puzzle puzzle3 = (56, f) where f [ a2, a3, a4, a6, a8, a9, b2, b4, b5, b6, b7, b8, b9, c1, c2, c3, c4, c6, c7, c9, d1, d3, d5, d7, d9, e2, e3, e4, e6, e7, e8, f1, f3, f5, f7, f9, g1, g3, g4, g6, g7, g8, g9, h1, h2, h3, h4, h5, h6, h8, i1, i2, i4, i6, i7, i8 ] = [ [ 6, a2, a3, a4, 1, a6, 5, a8, a9], [ 8, b2, 3, b4, b5, b6, b7, b8, b9], [c1, c2, c3, c4, 6, c6, c7, 2, c9], [d1, 3, d3, 1, d5, 8, d7, 9, d9], [ 1, e2, e3, e4, 9, e6, e7, e8, 4], [f1, 5, f3, 2, f5, 3, f7, 1, f9], [g1, 7, g3, g4, 3, g6, g7, g8, g9], [h1, h2, h3, h4, h5, h6, 3, h8, 6], [i1, i2, 4, i4, 5, i6, i7, i8, 9] ] f _ = error "puzzle3 needs exactly 56 elements!" -- | According to the web, this is the toughest -- sudoku puzzle ever.. It even has a name: Al Escargot: -- puzzle4 :: Puzzle puzzle4 = (58, f) where f [ a2, a3, a4, a5, a7, a9, b1, b3, b4, b6, b7, b8, c1, c2, c5, c6, c8, c9, d1, d2, d5, d6, d8, d9, e1, e3, e4, e6, e7, e8, f2, f3, f4, f5, f7, f8, f9, g2, g3, g4, g5, g6, g7, g9, h1, h3, h4, h5, h6, h7, h8, i1, i2, i4, i5, i6, i8, i9 ] = [ [ 1, a2, a3, a4, a5, 7, a7, 9, a9], [b1, 3, b3, b4, 2, b6, b7, b8, 8], [c1, c2, 9, 6, c5, c6, 5, c8, c9], [d1, d2, 5, 3, d5, d6, 9, d8, d9], [e1, 1, e3, e4, 8, e6, e7, e8, 2], [ 6, f2, f3, f4, f5, 4, f7, f8, f9], [ 3, g2, g3, g4, g5, g6, g7, 1, g9], [h1, 4, h3, h4, h5, h6, h7, h8, 7], [i1, i2, 7, i4, i5, i6, 3, i8, i9] ] f _ = error "puzzle4 needs exactly 58 elements!" -- | This one has been called diabolical, apparently puzzle5 :: Puzzle puzzle5 = (53, f) where f [ a1, a3, a5, a6, a9, b1, b4, b5, b7, b9, c2, c4, c5, c6, c7, c8, c9, d1, d2, d4, d6, d7, d8, e1, e2, e3, e5, e7, e8, e9, f2, f3, f4, f6, f8, f9, g1, g2, g3, g4, g5, g6, g8, h1, h3, h5, h6, h9, i1, i4, i5, i7, i9 ] = [ [a1, 9, a3, 7, a5, a6, 8, 6, a9], [b1, 3, 1, b4, b5, 5, b7, 2, b9], [ 8, c2, 6, c4, c5, c6, c7, c8, c9], [d1, d2, 7, d4, 5, d6, d7, d8, 6], [e1, e2, e3, 3, e5, 7, e7, e8, e9], [ 5, f2, f3, f4, 1, f6, 7, f8, f9], [g1, g2, g3, g4, g5, g6, 1, g8, 9], [h1, 2, h3, 6, h5, h6, 3, 5, h9], [i1, 5, 4, i4, i5, 8, i7, 7, i9] ] f _ = error "puzzle5 needs exactly 53 elements!" -- | The following is nefarious according to -- puzzle6 :: Puzzle puzzle6 = (64, f) where f [ a1, a2, a3, a4, a6, a7, a9, b1, b3, b4, b5, b6, b7, b8, b9, c1, c2, c4, c5, c6, c7, c8, c9, d1, d3, d4, d5, d6, d8, e2, e3, e4, e6, e7, e8, e9, f1, f2, f3, f4, f5, f6, f8, f9, g1, g2, g5, g7, g8, g9, h2, h3, h5, h6, h8, h9, i1, i2, i3, i4, i5, i6, i7, i9 ] = [ [a1, a2, a3, a4, 6, a6, a7, 8, a9], [b1, 2, b3, b4, b5, b6, b7, b8, b9], [c1, c2, 1, c4, c5, c6, c7, c8, c9], [d1, 7, d3, d4, d5, d6, 1, d8, 2], [ 5, e2, e3, e4, 3, e6, e7, e8, e9], [f1, f2, f3, f4, f5, f6, 4, f8, f9], [g1, g2, 4, 2, g5, 1, g7, g8, g9], [ 3, h2, h3, 7, h5, h6, 6, h8, h9], [i1, i2, i3, i4, i5, i6, i7, 5, i9] ] f _ = error "puzzle6 needs exactly 64 elements!" -- | Solve them all, this takes a fraction of a second to run for each case allPuzzles :: IO () allPuzzles = mapM_ sudoku [puzzle0, puzzle1, puzzle2, puzzle3, puzzle4, puzzle5, puzzle6]