Solve the eight queens problem at compile-time

Question

Can you solve the eight queens puzzle at compile-time?

Pick any suitable output format.

I'm particularly interested in a C++ template metaprogramming solution, but you can use languages that have similar constructs, like, for example, Haskell's type system.

Ideally your metaprogram would output all solutions. No hardcoding.

Answer 1

My meta-program finds all 92 solutions. They are printed as error messages:

error: 'solution' is not a member of 'print<15863724>'

This means the first queen should be placed at y = 1, the second at y = 5, the third at y = 8 and so on.

First, some useful meta-functions:

template <typename T>
struct return_
{
    typedef T type;
};

template <bool Condition, typename Then, typename False>
struct if_then_else;

template <typename Then, typename Else>
struct if_then_else<true, Then, Else> : return_<Then> {};

template <typename Then, typename Else>
struct if_then_else<false, Then, Else> : return_<Else> {};

template <int N>
struct constant
{
    enum { value = N };
};

template <int N>
struct print
{
    // empty body -> member access yields a compiler error involving N
};

Then, two interesting meta-functions (note the singular and the plural):

template <int queens, int rows, int sums, int difs, int x, int y>
struct put_queen;

template <int queens, int rows, int sums, int difs, int x>
struct put_queens : constant
     < put_queen<queens, rows, sums, difs, x, 1>::value
     + put_queen<queens, rows, sums, difs, x, 2>::value
     + put_queen<queens, rows, sums, difs, x, 3>::value
     + put_queen<queens, rows, sums, difs, x, 4>::value
     + put_queen<queens, rows, sums, difs, x, 5>::value
     + put_queen<queens, rows, sums, difs, x, 6>::value
     + put_queen<queens, rows, sums, difs, x, 7>::value
     + put_queen<queens, rows, sums, difs, x, 8>::value > {};

template <int queens, int rows, int sums, int difs, int x, int y>
struct put_queen : if_then_else<
    rows & (1 << y) || sums & (1 << (x + y)) || difs & (1 << (8 + x - y)),
    constant<0>,
    put_queens<queens * 10 + y, rows | (1 << y), sums | (1 << (x + y)),
               difs | (1 << (8 + x - y)), x + 1>
>::type {};

The variable queens stores the y coordinates of the queens placed on the board so far. The following three variables store the rows and diagonals that are already occupied by queens. x and y should be self-explanatory.

The first argument to if_then_else checks whether the current position is blocked. If it is, the recursion stops by returning the (meaningless) result 0. Otherwise, the queen is placed on the board, and the process continues with the next column.

When x reaches 8, we have found a solution:

template <int queens, int rows, int sums, int difs>
struct put_queens<queens, rows, sums, difs, 8>
{
    enum { value = print<queens>::solution };
};

Since the print template has no member solution, the compiler generates an error.

And finally, to start the process, we inspect the value member of the empty board:

int go = put_queens<0, 0, 0, 0, 0>::value;

The complete program can be found at ideone.

Answer 2

I came up with a solution that uses the Haskell type system. I googled a bit for an existing solution to the problem at the value level, changed it a bit, and then lifted it to the type level. It took a lot of reinventing. I also had to enable a bunch of GHC extensions.

First, since integers are not allowed at the type level, I needed to reinvent the natural numbers once more, this time as types:

data Zero -- type that represents zero
data S n  -- type constructor that constructs the successor of another natural number
-- Some numbers shortcuts
type One = S Zero
type Two = S One
type Three = S Two
type Four = S Three
type Five = S Four
type Six = S Five
type Seven = S Six
type Eight = S Seven

The algorithm I adapted makes additions and subtractions on naturals, so I had to reinvent these as well. Functions at the type level are defined with resort to type classes. This requires the extensions for multiple parameter type classes and functional dependencies. Type classes cannot "return values", so we use an extra parameter for that, in a manner similar to PROLOG.

class Add a b r | a b -> r -- last param is the result
instance Add Zero b b                     -- 0 + b = b
instance (Add a b r) => Add (S a) b (S r) -- S(a) + b = S(a + b)

class Sub a b r | a b -> r
instance Sub a Zero a                     -- a - 0 = a
instance (Sub a b r) => Sub (S a) (S b) r -- S(a) - S(b) = a - b

Recursion is implemented with class assertions, so the syntax looks a bit backward.

Next up were booleans:

data True  -- type that represents truth
data False -- type that represents falsehood

And a function to do inequality comparisons:

class NotEq a b r | a b -> r
instance NotEq Zero Zero False                -- 0 /= 0 = False
instance NotEq (S a) Zero True                -- S(a) /= 0 = True
instance NotEq Zero (S a) True                -- 0 /= S(a) = True
instance (NotEq a b r) => NotEq (S a) (S b) r -- S(a) /= S(b) = a /= b

And lists...

data Nil
data h ::: t
infixr 0 :::

class Append xs ys r | xs ys -> r
instance Append Nil ys ys                                       -- [] ++ _ = []
instance (Append xs ys rec) => Append (x ::: xs) ys (x ::: rec) -- (x:xs) ++ ys = x:(xs ++ ys)

class Concat xs r | xs -> r
instance Concat Nil Nil                                         -- concat [] = []
instance (Concat xs rec, Append x rec r) => Concat (x ::: xs) r -- concat (x:xs) = x ++ concat xs

class And l r | l -> r
instance And Nil True                    -- and [] = True
instance And (False ::: t) False         -- and (False:_) = False
instance (And t r) => And (True ::: t) r -- and (True:t) = and t

ifs are also missing at the type level...

class Cond c t e r | c t e -> r
instance Cond True t e t  -- cond True t _ = t
instance Cond False t e e -- cond False _ e = e

And with that, all the supporting machinery I used was in place. Time to tackle the problem itself!

Starting with a function to test if adding a queen to an existing board is ok:

-- Testing if it's safe to add a queen
class Safe x b n r | x b n -> r
instance Safe x Nil n True    -- safe x [] n = True
instance (Safe x y (S n) rec,
          Add c n cpn, Sub c n cmn,
          NotEq x c c1, NotEq x cpn c2, NotEq x cmn c3,
          And (c1 ::: c2 ::: c3 ::: rec ::: Nil) r) => Safe x (c ::: y) n r
    -- safe x (c:y) n = and [ x /= c , x /= c + n , x /= c - n , safe x y (n+1)]

Notice the use of class assertions to obtain intermediate results. Because the return values are actually an extra parameter, we can't just call the assertions directly from each other. Again, if you've used PROLOG before you may find this style a bit familiar.

After I made a few changes to remove the need for lambdas (which I could have implemented, but I decided to leave for another day), this is what the original solution looked like:

queens 0 = [[]]
-- The original used the list monad. I "unrolled" bind into concat & map.
queens n = concat $ map f $ queens (n-1)
g y x = if safe x y 1 then [x:y] else []
f y = concat $ map (g y) [1..8]

map is a higher order function. I thought implementing higher order meta-functions would be too much hassle (again the lambdas) so I just went with a simpler solution: since I know what functions will be mapped, I can implement specialized versions of map for each, so that those are not higher-order functions.

-- Auxiliary meta-functions
class G y x r | y x -> r
instance (Safe x y One s, Cond s ((x ::: y) ::: Nil) Nil r) => G y x r

class MapG y l r | y l -> r
instance MapG y Nil Nil
instance (MapG y xs rec, G y x g) => MapG y (x ::: xs) (g ::: rec)

-- Shortcut for [1..8]
type OneToEight = One ::: Two ::: Three ::: Four ::: Five ::: Six ::: Seven ::: Eight ::: Nil

class F y r | y -> r
instance (MapG y OneToEight m, Concat m r) => F y r -- f y = concat $ map (g y) [1..8]

class MapF l r | l -> r
instance MapF Nil Nil
instance (MapF xs rec, F x f) => MapF (x ::: xs) (f ::: rec)

And the last meta-function can be written now:

class Queens n r | n -> r
instance Queens Zero (Nil ::: Nil)
instance (Queens n rec, MapF rec m, Concat m r) => Queens (S n) r

All that's left is some kind of driver to coax the type-checking machinery to work out the solutions.

-- dummy value of type Eight
eight = undefined :: Eight
-- dummy function that asserts the Queens class
queens :: Queens n r => n -> r
queens = const undefined

This meta-program is supposed to run on the type checker, so one can fire up ghci and ask for the type of queens eight:

> :t queens eight

This will exceed the default recursion limit rather fast (it's a measly 20). To increase this limit, we need to invoke ghci with the -fcontext-stack=N option, where N is the desired stack depth (N=1000 and fifteen minutes is not enough). I haven't seen this run to completion yet, as it takes a very long time, but I've managed to run up to queens four.

There's a full program on ideone with some machinery for pretty printing the result types, but there only queens two can run without exceeding the limits :(

Answer 3

Here's a C++11 solution without any templates:

constexpr int trypos(
    int work, int col, int row, int rows, int diags1, int diags2,
    int rowbit, int diag1bit, int diag2bit);

constexpr int place(
    int result, int work, int col, int row, int rows, int diags1, int diags2)
{
    return result != 0 ? result
        : col == 8 ? work
        : row == 8 ? 0
        : trypos(work, col, row, rows, diags1, diags2,
                 1 << row, 1 << (7 + col - row), 1 << (14 - col - row));
}

constexpr int trypos(
    int work, int col, int row, int rows, int diags1, int diags2,
    int rowbit, int diag1bit, int diag2bit)
{
    return !(rows & rowbit) && !(diags1 & diag1bit) && !(diags2 & diag2bit)
        ? place(
            place(0, work*10 + 8-row, col + 1, 0,
                  rows | rowbit, diags1 | diag1bit, diags2 | diag2bit),
            work, col, row + 1, rows, diags1, diags2)
        : place(0, work, col, row + 1, rows, diags1, diags2);
}

int places = place(0, 0, 0, 0, 0, 0, 0);

The solution is encoded as decimal digits, as in FredOverflow's answers. GCC 4.7.1 compiles the above file into the following assembly source with g++ -S -std=c++11 8q.cpp:

    .file   "8q.cpp"
    .globl  places
    .data
    .align 4
    .type   places, @object
    .size   places, 4
places:
    .long   84136275
    .ident  "GCC: (GNU) 4.7.1"
    .section    .note.GNU-stack,"",@progbits

The value of the symbol places is 84136275, i.e. the first queen is at a8, the second at b4 etc.