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

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV.Examples.Puzzles.NQueens

Description

Solves the NQueens puzzle: http://en.wikipedia.org/wiki/Eight_queens_puzzle

Synopsis

Documentation

type Solution = [SWord8] Source

A solution is a sequence of row-numbers where queens should be placed

isValid :: Int -> Solution -> SBool Source

Checks that a given solution of n-queens is valid, i.e., no queen captures any other.

nQueens :: Int -> IO () Source

Given n, it solves the n-queens puzzle, printing all possible solutions.