sbv-0.9.7: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.

Portability portable experimental erkokl@gmail.com

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] -> SBoolSource

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

Solve a given puzzle and print the results

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

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

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