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

Documentation.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