Solve the eight queens problem at compile-time

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

error: ‘solution’ is not a member of ‘std::integral_constant<int, 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.

The meta-program consists of two mutually recursive meta-functions put_queen and put_queens:

#include <type_traits>

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 : std::integral_constant<int,
    // try all 8 possible values for y
       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 : std::conditional<
    // if blocked
    rows & (1 << y)
 || sums & (1 << (x + y))
 || difs & (1 << (x - y + 8)),
    // then backtrack
    std::integral_constant<int, 0>,
    // else recurse
    put_queens<queens * 10 + y,
               rows | (1 << y),
               sums | (1 << (x + y)),
               difs | (1 << (x - y + 8)),
               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 conditional checks whether the current position is blocked. If it is, we backtrack by returning the (meaningless) result 0. Otherwise, the queen is placed on the board, and the recursion 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> {
    // print solution as error message by accessing non-existent member
    enum { value = std::integral_constant<int, queens>::solution };
};

Since integral_constant has no member solution, the compiler prints queens as an error message.

To start the recursion, 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.

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 :(

C, via the preprocessor

I think the ANSI committee made a conscious choice not to extend the C preprocessor to the point of being Turing-complete. In any case, it's not really powerful enough to solve the eight queens problem. Not in any sort of general fashion.

But it can be done, if you're willing to hard-code the loop counters. There's no real way to loop, of course, but you can use self-inclusion (via #include __FILE__) to get a limited sort of recursion.

#ifdef i
# if (r_(i) & 1 << j_(i)) == 0 && (p_(i) & 1 << i + j_(i)) == 0 \
                               && (n_(i) & 1 << 7 + i - j_(i)) == 0
#  if i == 0
#   undef i
#   define i 1
#   undef r1
#   undef p1
#   undef n1
#   define r1 (r0 | (1 << j0))
#   define p1 (p0 | (1 << j0))
#   define n1 (n0 | (1 << 7 - j0))
#   undef j1
#   define j1 0
#   include __FILE__
#   undef j1
#   define j1 1
#   include __FILE__
#   undef j1
#   define j1 2
#   include __FILE__
#   undef j1
#   define j1 3
#   include __FILE__
#   undef j1
#   define j1 4
#   include __FILE__
#   undef j1
#   define j1 5
#   include __FILE__
#   undef j1
#   define j1 6
#   include __FILE__
#   undef j1
#   define j1 7
#   include __FILE__
#   undef i
#   define i 0
#  elif i == 1
#   undef i
#   define i 2
#   undef r2
#   undef p2
#   undef n2
#   define r2 (r1 | (1 << j1))
#   define p2 (p1 | (1 << 1 + j1))
#   define n2 (n1 | (1 << 8 - j1))
#   undef j2
#   define j2 0
#   include __FILE__
#   undef j2
#   define j2 1
#   include __FILE__
#   undef j2
#   define j2 2
#   include __FILE__
#   undef j2
#   define j2 3
#   include __FILE__
#   undef j2
#   define j2 4
#   include __FILE__
#   undef j2
#   define j2 5
#   include __FILE__
#   undef j2
#   define j2 6
#   include __FILE__
#   undef j2
#   define j2 7
#   include __FILE__
#   undef i
#   define i 1
#  elif i == 2
#   undef i
#   define i 3
#   undef r3
#   undef p3
#   undef n3
#   define r3 (r2 | (1 << j2))
#   define p3 (p2 | (1 << 2 + j2))
#   define n3 (n2 | (1 << 9 - j2))
#   undef j3
#   define j3 0
#   include __FILE__
#   undef j3
#   define j3 1
#   include __FILE__
#   undef j3
#   define j3 2
#   include __FILE__
#   undef j3
#   define j3 3
#   include __FILE__
#   undef j3
#   define j3 4
#   include __FILE__
#   undef j3
#   define j3 5
#   include __FILE__
#   undef j3
#   define j3 6
#   include __FILE__
#   undef j3
#   define j3 7
#   include __FILE__
#   undef i
#   define i 2
#  elif i == 3
#   undef i
#   define i 4
#   undef r4
#   undef p4
#   undef n4
#   define r4 (r3 | (1 << j3))
#   define p4 (p3 | (1 << 3 + j3))
#   define n4 (n3 | (1 << 10 - j3))
#   undef j4
#   define j4 0
#   include __FILE__
#   undef j4
#   define j4 1
#   include __FILE__
#   undef j4
#   define j4 2
#   include __FILE__
#   undef j4
#   define j4 3
#   include __FILE__
#   undef j4
#   define j4 4
#   include __FILE__
#   undef j4
#   define j4 5
#   include __FILE__
#   undef j4
#   define j4 6
#   include __FILE__
#   undef j4
#   define j4 7
#   include __FILE__
#   undef i
#   define i 3
#  elif i == 4
#   undef i
#   define i 5
#   undef r5
#   undef p5
#   undef n5
#   define r5 (r4 | (1 << j4))
#   define p5 (p4 | (1 << 4 + j4))
#   define n5 (n4 | (1 << 11 - j4))
#   undef j5
#   define j5 0
#   include __FILE__
#   undef j5
#   define j5 1
#   include __FILE__
#   undef j5
#   define j5 2
#   include __FILE__
#   undef j5
#   define j5 3
#   include __FILE__
#   undef j5
#   define j5 4
#   include __FILE__
#   undef j5
#   define j5 5
#   include __FILE__
#   undef j5
#   define j5 6
#   include __FILE__
#   undef j5
#   define j5 7
#   include __FILE__
#   undef i
#   define i 4
#  elif i == 5
#   undef i
#   define i 6
#   undef r6
#   undef p6
#   undef n6
#   define r6 (r5 | (1 << j5))
#   define p6 (p5 | (1 << 5 + j5))
#   define n6 (n5 | (1 << 12 - j5))
#   undef j6
#   define j6 0
#   include __FILE__
#   undef j6
#   define j6 1
#   include __FILE__
#   undef j6
#   define j6 2
#   include __FILE__
#   undef j6
#   define j6 3
#   include __FILE__
#   undef j6
#   define j6 4
#   include __FILE__
#   undef j6
#   define j6 5
#   include __FILE__
#   undef j6
#   define j6 6
#   include __FILE__
#   undef j6
#   define j6 7
#   include __FILE__
#   undef i
#   define i 5
#  elif i == 6
#   undef i
#   define i 7
#   undef r7
#   undef p7
#   undef n7
#   define r7 (r6 | (1 << j6))
#   define p7 (p6 | (1 << 6 + j6))
#   define n7 (n6 | (1 << 13 - j6))
#   undef j7
#   define j7 0
#   include __FILE__
#   undef j7
#   define j7 1
#   include __FILE__
#   undef j7
#   define j7 2
#   include __FILE__
#   undef j7
#   define j7 3
#   include __FILE__
#   undef j7
#   define j7 4
#   include __FILE__
#   undef j7
#   define j7 5
#   include __FILE__
#   undef j7
#   define j7 6
#   include __FILE__
#   undef j7
#   define j7 7
#   include __FILE__
#   undef i
#   define i 6
#  elif i == 7
    printf("(1 %d) (2 %d) (3 %d) (4 %d) (5 %d) (6 %d) (7 %d) (8 %d)\n",
           j0 + 1, j1 + 1, j2 + 1, j3 + 1, j4 + 1, j5 + 1, j6 + 1, j7 + 1);
#  endif
# endif
#else
#include <stdio.h>
#define _cat(a, b) a ## b
#define j_(i) _cat(j, i)
#define n_(i) _cat(n, i)
#define p_(i) _cat(p, i)
#define r_(i) _cat(r, i)
int main(void)
{
# define i 0
# define j0 0
# include __FILE__
# undef j0
# define j0 1
# include __FILE__
# undef j0
# define j0 2
# include __FILE__
# undef j0
# define j0 3
# include __FILE__
# undef j0
# define j0 4
# include __FILE__
# undef j0
# define j0 5
# include __FILE__
# undef j0
# define j0 6
# include __FILE__
# undef j0
# define j0 7
# include __FILE__
# undef j0
    return 0;
}
#endif

Despite the horrific amount of repetitive content, let me assure you that it truly is solving the eight queens problem algorithmically. Unfortunately the one thing that I couldn't do with the preprocessor is implement a general push-down stack data structure. The upshot is that I had to hard-code the value of i wherever it was used to select another value to set. (As opposed to retrieving values, which could be done completely generally. That's why the #if at the top of the file, which is what decides if a queen can be added at the current position, didn't need to be repeated eight times.)

Within the preprocessor code, i and j indicate the current position being considered, while r, p, and n keep track of which ranks and diagonals are currently unavailable for placement. However, i also doubles as the counter marking the current depth of recursion, so really all the other values actually use i as a sort of subscript, so that their values are preserved when resuming from a recursion. (And also because of the serious difficulty of modifying the value of a preprocessor symbol without completely replacing it.)

The compiled program prints all 92 solutions. The solutions are embedded directly into the executable; the preprocessor output looks like this:

/* ... #included content from <stdio.h> ... */
int main(void)
{
    printf("(1 %d) (2 %d) (3 %d) (4 %d) (5 %d) (6 %d) (7 %d) (8 %d)\n",
           0 + 1, 4 + 1, 7 + 1, 5 + 1, 2 + 1, 6 + 1, 1 + 1, 3 + 1);
    printf("(1 %d) (2 %d) (3 %d) (4 %d) (5 %d) (6 %d) (7 %d) (8 %d)\n",
           0 + 1, 5 + 1, 7 + 1, 2 + 1, 6 + 1, 3 + 1, 1 + 1, 4 + 1);
    printf("(1 %d) (2 %d) (3 %d) (4 %d) (5 %d) (6 %d) (7 %d) (8 %d)\n",
           0 + 1, 6 + 1, 3 + 1, 5 + 1, 7 + 1, 1 + 1, 4 + 1, 2 + 1);
    /* ... 88 more solutions ... */
    printf("(1 %d) (2 %d) (3 %d) (4 %d) (5 %d) (6 %d) (7 %d) (8 %d)\n",
           7 + 1, 3 + 1, 0 + 1, 2 + 1, 5 + 1, 1 + 1, 6 + 1, 4 + 1);
    return 0;
}

It can be done, even though it clearly shouldn't.