The n-Queens Problem

This is a tutorial introduction demonstrating the use of the cflp package by solving the n-queens problem with a lazy functional-logic program: place n queens on an n × n chessboard such that no queen can hit another in one move.

Installation instructions can be found on the cflp website. Once you have installed the package you can execute this tutorial which is Literate Haskell. If you are reading the HTML version, you find the plain .lhs file on the mentioned website (and vice versa).

{-# LANGUAGE
NoMonomorphismRestriction,
MultiParamTypeClasses,
FlexibleInstances,
NoMonoPatBinds,
TypeFamilies
#-}

import CFLP
import CFLP.Strategies

import CFLP.Types.Bool
import CFLP.Types.List hiding ( map )
import Prelude hiding ( not )

After importing the CFLP library, we can access combinators to define non-deterministic datatypes and operations.

Non-Deterministic Data

In order to demonstrate how to define lazy non-deterministic datatypes, we use natural numbers in Peano notation to denote rows and columns of a chessboard:

data Nat = Zero | Suc Nat
deriving Show

For convenience, we define functions that convert between Peano numbers and integers.

nat2int :: Nat -> Int
nat2int Zero = 0
nat2int (Suc n) = nat2int n + 1

int2nat :: Int -> Nat
int2nat 0 = Zero
int2nat (n+1) = Suc (int2nat n)

A functional-logic program will use numbers of type Data s Nat where Nondet is an abstract type constructor for non-deterministic data, cs is a constraint store and m is a constraint solver monad. We don't care about what exactly a constraint solver or a constraint solver monad is but simply notice, that we might use different ones in order to use different search strategies.

We can define constructor functions for values of type Data s Nat using combinators from the CFLP library. To do so, we need to define type-class instances that describe the structure of our datatype. The definitions are completely mechanic and could probably be automated.

First, we define an instance of the class ApplyCons:

instance ApplyCons Nat where type Result Nat = Nat; applyCons = const

All user-defined instances of ApplyCons look like this.

The structure of our datatype is captured by the class Generic:

instance Generic Nat
where constr = cons "Zero" Zero dZero ! cons "Suc" Suc dSuc

We only need to list the constructors and destructors of our datatype. Destructors are also defined mechanically:

dZero, dSuc :: Decons Nat
dZero zero Zero = Just (zero [])
dZero _ _ = Nothing
dSuc suc (Suc n) = Just (suc [generic n])
dSuc _ _ = Nothing

The Generic instance allows to convert between non-deterministic and primitive Haskell values and to define constructors and destructors for non-deterministic data.

zero :: Monad s => Nondet c s Nat
suc :: Monad s => Nondet c s Nat -> Nondet c s Nat
zero :! suc :! () = constructors

Here, it is important to list the constructors in the same order as in the instance declaration for the class Generic. We get constructor functions of arbitrary aritiy where all types are lifted to the Nondet type.

In order to define operations on non-deterministic numbers, we also need helpers for pattern matching that are defined similarly.

pZero :: (Context c -> Nondet c s a) -> Match Nat c s a
pSuc :: (Context c -> Nondet c s Nat -> Nondet c s a) -> Match Nat c s a
pZero :! pSuc :! () = patterns

A matcher takes a function that takes an evaluation context and non-deterministic values that correspond to the arguments of the matched constructor and yields an arbitrary non-deterministic value.

Operations on Non-Deterministic Data

No we can define operations on non-deterministic numbers. As an example consider addition:

add :: CFLP s
=> Data s Nat -> Data s Nat -> Context (Ctx s) -> Data s Nat
add n m = caseOf n
[ pZero (\_ -> m)
, pSuc (\cs n' -> suc (add n' m cs)) ]

The function add takes two non-deterministic numbers and - as additional argument - a constraint store that is passed to the combinator caseOf for pattern matching. The case alternatives are given as a list of matchers that can access an updated constraint store and pass it down in the computation1. The context CFLP s states that cs is a constraint store and m is a constraint solver monad suitable for functional-logic programming.

Once we have defined addition, we can use logic programming to define subtraction! In the functional-logic programming language Curry, we could define the function sub as follows:

sub :: Nat -> Nat -> Nat
sub n m | n =:= add m x = x
where x free

This definition uses the constraint-equality operation (=:=) :: a -> a -> Success to state that the sum of the second argument of sub and its result should equal its first argument. The result of sub is introduced as free (logic) variable.

We can define how to generate logic variables of type Data s Nat by instantiating the type class Narrow.

instance Narrow Nat
where
narrow cs u = withUnique (\u' -> oneOf [zero, suc (unknown u')] cs u) u

A free variable is a non-deterministic generator of each possible value. The combinator unknown is defined in terms of narrow and can be used to obtain a free logic variable. We can narrow non-deterministic natural numbers in every constraint store that supports non-deterministic choices which is expressed using a corresponding class constraint in the instance definition.

Operations that cause non-deterministic branching - like narrow does - need an additional argument of type ID that is passed to the oneOf combinator for non-deterministic choice. In order to simplify the distribution of unique identifiers, the CFLP library provides an overloaded operation withUnique that has all of the following types at the same time:

withUnique :: Data s a -> ID -> Data s a
withUnique :: (ID -> Data s a) -> ID -> Data s a
withUnique :: (ID -> ID -> Data s a) -> ID -> Data s a
withUnique :: (ID -> ID -> ID -> Data s a) -> ID -> Data s a
...

When using withUnique we can access an arbitrary number of unique identifiers (even zero) without bothering about how they are generated.

The CFLP library provides an operation (===) (similar to (=:=) in Curry but with a boolean result) that can be used to define the Haskell version of the function sub.

sub :: CFLP s
=> Data s Nat -> Data s Nat
-> Context (Ctx s) -> ID -> Data s Nat
sub n m cs = withUnique $ \u ->
let x = unknown u in
caseOf ((n === add m x cs) cs)
[pTrue (\_ -> x)] cs

As sub calls the combinator unknown to generate a free variable, we need to pass a unique identifier in addition to the constraint store. The guard of the Curry program is expressed by a partial pattern matching on True.

Now we can execute the call

 > eval dfs (sub(suc(suc zero)) (suc zero) :: Computation Nat)
[Suc Zero]

to enumerate the results of subtracting one from two in depth first order. Note, that results are returned as primitive Haskell terms of type Nat. We can also enumerate them interactively:

 > evalPrint dfs (sub(suc(suc zero)) (suc zero) :: Computation Nat)
Suc Zero
more? [Y(es)|n(o)|a(ll)]: y
No more solutions.

This is useful if the number of results is infinite or we are not interested in all of them for some other reason.

The first argument dfs () is a strategy that should be used for the computation. Here, we use the list monad which implements depth first search. If you have your own implementation m of MonadPlus and an enumeration function of type m a -> [a] then you can use this as a strategy as well!

Safely Placing Queens

We represent a placement of n queens on an n × n chessboard with a permutation of [1..n]. A number c at position r of the permutation means that in row r of the chessboard, a queen is placed at column c. This representation ensures that every row and every colum contains exactly one queen, so we only need to check whether they can hit each other diagonally.

In Curry, we could compute safe placements of queens as follows:

placement :: Int -> [Int]
placement n = allSafe (permute [1..n])

The non-deterministic operation permute computes permutations of its input by successively inserting its elements at arbitrary positions.

permute :: [a] -> [a]
permute [] = []
permute (x:xs) = insert x (permute xs)

insert :: a -> [a] -> [a]
insert x xs = x : xs
insert x (y:ys) = y : insert x ys

The operation insert either inserts the given element as new head or somewhere in the tail of the given list, if it is non-empty.

Now, we only need to define when a placement of queens is safe.

allSafe :: [Int] -> [Int]
allSafe [] = []
allSafe (q:qs) = safe q qs 1 : allSafe qs

The operation allSafe is a so called constrained identity function, i.e., it either returns its argument or fails. The operation safe is another constrained identity (on the first argument) that checks whether one queen can hit another by comparing the remaining positions to the diagonally reachable positions of the given queen.

safe :: Int -> [Int] -> Int -> Int
safe p [] _ = p
safe p (q:qs) offset | noAttac p q offset = safe p qs (offset+1)

noAttac :: Int -> Int -> Int -> Bool
noAttac p q offset | p + offset /= q = p /= q + offset

A key feature of this program is laziness: the constrained identities may fail without consuming the complete placement of queens, i.e., without computing the whole permutation. For example, if the placement is of the form 1:2:qs then qs (representing (n-2)! permutations) does not need to be computed.

Placing Queens with the CFLP library

We can implement an equivalent program (featuring laziness!) in pure Haskell using the CFLP library. The library provides constructors and matchers for non-deterministic lists with the following types:

nil   :: Monad s => Data s [a]
(^:) :: Monad s => Data s a -> Data s [a] -> Data s [a]

pNil :: (c -> Data s b) -> Match [a] c s b
pCons :: (c -> Data s a -> Data s [a] -> Data s b)
-> Match [a] c s b

The function that computes a safe placement of n queens is defined as follows:

placement :: CFLP s => Int -> Context (Ctx s) -> ID -> Data s [Nat]
placement n cs u = allSafe (permute queens cs u) cs
where queens = nondet (map int2nat [1..n])

It takes a constraint store and a unique identifier. The constraint store is passed to both allSafe and permute, but only permute needs a unique identifier - allSafe does not introduce non-deterministic branching.

The CFLP library provides a generic function

nondet :: (Monad m, Data a) => a -> Data s a

that generates non-deterministic data from primitive Haskell datatypes.

The operation permute resembles the Curry definition given above. It uses withUnique to access a sufficient number of fresh identifiers, the combinator caseOf to match the given non-deterministic list, and passes updated constraint stores to the function insert and the recursive call.

permute :: CFLP s
=> Data s [Nat] -> Context (Ctx s) -> ID -> Data s [Nat]
permute l cs = withUnique $ \u1 u2 -> caseOf l
[ pNil (\_ -> nil)
, pCons (\cs x xs -> insert x (permute xs cs u1) cs u2) ] cs

The insert operation uses oneOf to generate a non-deterministic choice between inserting the element as head or in the tail of the given list. Insertion in the tail is performed with a (partial) pattern matching on non-empty lists and a recursive call of insert to ys.

insert :: CFLP s
=> Data s Nat -> Data s [Nat]
-> Context (Ctx s) -> ID -> Data s [Nat]
insert x xs cs = withUnique $ \u ->
(x ^: xs) ?
(caseOf xs
[pCons (\cs y ys -> y ^: insert x ys cs u)] cs)

The operator (?) is similar to oneOf in that it declares a non-deterministic choice, but it takes exactly two arguments. More importantly, unlike oneOf, the operator (?) does not take a constraint store2.

Now, we need to define the constrained identity allSafe. All functions resemble the Curry definitions given above.

allSafe :: CFLP s => Data s [Nat] -> Context (Ctx s) -> Data s [Nat]
allSafe l = caseOf l
[ pNil (\_ -> nil)
, pCons (\cs q qs -> safe q qs (suc zero) cs ^: allSafe qs cs) ]

safe :: CFLP s
=> Data s Nat -> Data s [Nat] -> Data s Nat
-> Context (Ctx s) -> Data s Nat
safe p l offset = caseOf l
[ pNil (\_ -> p)
, pCons (\cs q qs -> caseOf (noAttac p q offset cs)
[ pTrue (safe p qs (suc offset)) ] cs) ]

noAttac :: CFLP s
=> Data s Nat -> Data s Nat -> Data s Nat
-> Context (Ctx s) -> Data s Bool
noAttac p q offset cs = caseOf ((add p offset cs === q) cs)
[ pFalse (\cs -> not ((p === add q offset cs) cs) cs) ] cs

Finally, we can define an operation main that prints all possible placements of 8 queens on an 8 × 8 chessboard:

main :: IO ()
main = do
qs <- eval dfs (placement 8 :: Computation [Nat])
mapM_ print . map (map nat2int) $ qs

Notes on Efficiency

Although I have not investigated any effort yet in the efficiency of the CFLP library, I have compared the runtime of this program with the run times of an equivalent Curry program in the Curry systems MCC, PAKCS, and KiCS. The results are depicted in the following table.

Systemrun time
MCC1.1s
PAKCS5.4s
KiCS8.4s
CFLP5.8s

I have also compared this implementation with a simple implementation using MonadPlus without preserving laziness. Such an implementation is much faster, probably because laziness is not important when computing permutations of such short lists.


  1. You may wonder, why we have to pass constraint stores explicitly and why they are not hidden in a state component of the monad. A significant feature of the CFLP library is, that monadic values are shared and not recomputed if the same monadic action occurs more than once in a computation because of sharing. Monadic values of a state-threading monad are functions and would need to be recomputed for each occurrence.

  2. Choices that are build with (?) are recomputed according to the current constraint store whenever they are matched (like free variables). So you should use (?) when you declare a non-deterministic choice (especially when you intend to share it). The combinator oneOf is usually only used in the definitions of narrow where reexecution is already handled before by unknown.