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

Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.Puzzles.NQueens

Description

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

Synopsis

type Solution = [SWord8]
isValid :: Int -> Solution -> SBool
nQueens :: Int -> IO ()

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.