sbv-0.9.14: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.
Data.SBV.Examples.Puzzles.NQueens
Description
Solves the NQueens puzzle: http://en.wikipedia.org/wiki/Eight_queens_puzzle
Synopsis
type Solution = [SWord8]Source
A solution is a sequence of row-numbers where queens should be placed
isValid :: Int -> Solution -> SBoolSource
Checks that a given solution of n-queens is valid, i.e., no queen captures any other.
n
nQueens :: Int -> IO ()Source
Given n, it solves the n-queens puzzle, printing all possible solutions.
n-queens