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

Copyright (c) Levent Erkok BSD3 erkokl@gmail.com experimental None Haskell2010

Data.SBV.Examples.Puzzles.Sudoku

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] -> SBool Source

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

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

Find an arbitrary good board

A random puzzle, found on the internet..

Another random puzzle, found on the internet..

Another random puzzle, found on the internet..

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

This one has been called diabolical, apparently

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

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