sbv-2.3: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Stabilityexperimental
Maintainererkokl@gmail.com
Safe HaskellSafe-Infered

Data.SBV.Examples.Puzzles.Sudoku

Contents

Description

The Sudoku solver, quintessential SMT solver example!

Synopsis

Modeling Sudoku

type Row = [SWord8]Source

A row is a sequence of 8-bit words, too large indeed for representing 1-9, but does not harm

type Board = [Row]Source

A Sudoku board is a sequence of 9 rows

check :: [SWord8] -> SBoolSource

Given a series of elements, make sure they are all different and they all are numbers between 1 and 9

valid :: Board -> SBoolSource

Given a full Sudoku board, check that it is valid

type Puzzle = (Int, [SWord8] -> Board)Source

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.

Solving Sudoku puzzles

sudoku :: Puzzle -> IO ()Source

Solve a given puzzle and print the results

dispSolution :: Puzzle -> (Bool, [Word8]) -> IO ()Source

Helper function to display results nicely, not really needed, but helps presentation

solveAll :: Puzzle -> IO ()Source

Find all solutions to a puzzle

Example boards

puzzle0 :: PuzzleSource

Find an arbitrary good board

puzzle1 :: PuzzleSource

A random puzzle, found on the internet..

puzzle2 :: PuzzleSource

Another random puzzle, found on the internet..

puzzle3 :: PuzzleSource

Another random puzzle, found on the internet..

puzzle4 :: PuzzleSource

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

puzzle5 :: PuzzleSource

This one has been called diabolical, apparently

puzzle6 :: PuzzleSource

The following is nefarious according to http://haskell.org/haskellwiki/Sudoku

allPuzzles :: IO ()Source

Solve them all, this takes a fraction of a second to run for each case