sbv-5.9: 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

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