sbv-10.9: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.Puzzles.Sudoku

Description

The Sudoku solver, quintessential SMT solver example!

Synopsis

Modeling Sudoku

type Row = [SInteger] Source #

A row is a sequence of digits that we represent symbolic integers

type Board = [Row] Source #

A Sudoku board is a sequence of 9 rows

check :: [SInteger] -> SBool Source #

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

valid :: Board -> SBool Source #

Given a full Sudoku board, check that it is valid

type Puzzle = [[Integer]] Source #

A puzzle is simply a list of rows. Put 0 to indicate blanks.

Solving Sudoku puzzles

fillBoard :: Puzzle -> IO Puzzle Source #

Fill a given board, replacing 0's with appropriate elements to solve the puzzle

sudoku :: Puzzle -> IO () Source #

Solve a given puzzle and print the results

Example boards

puzzle1 :: Puzzle Source #

A random puzzle, found on the internet..

puzzle2 :: Puzzle Source #

Another random puzzle, found on the internet..

puzzle3 :: Puzzle Source #

Another random puzzle, found on the internet..

puzzle4 :: Puzzle Source #

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 :: Puzzle Source #

This one has been called diabolical, apparently

puzzle6 :: Puzzle Source #

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