Eight queens

The following program solves the eight queens puzzle.

function main () {
  array8<array2<int5>> queens;

  queens.eachCombination(2, function (pair) {
    invariant !attacking?(pair.first, pair.last);
  });

  queens.each(function^ (queen, index) {
    invariant queen.row.between?(1, queens.length);
    invariant queen.column.between?(1, queens.length);

    # This rules out duplicate (permuted) solutions:
    invariant queen.row == index + 1;
  });

  expose queens;
};

function attacking? (queen1, queen2) {
  return queen1.row == queen2.row
      || queen1.column == queen2.column
      || queen1.leftDiagonal == queen2.leftDiagonal
      || queen1.rightDiagonal == queen2.rightDiagonal;
};

function row (queen) {
  return queen[0];
};

function column (queen) {
  return queen[1];
};

function leftDiagonal (queen) {
  return queen.row + queen.column;
};

function rightDiagonal (queen) {
  return queen.row - queen.column;
};

main();

You can touch the chessboard on the right to cycle through different solutions.

How does it work?

We declare an array of eight queens, which are represented as (x, y) coordinates. We iterate through all possible pairs of queen with eachCombination and specify that they must not be attacking. We then check that all queens are in-bounds.

To determine whether two queens are attacking, we check if they are on the same row, column or diagonal. To test the diagonals, we add and subtract the components of the coordinates and compare these values.

This program uses the method syntax to help with readibility. It also wraps the high-level code in a ‘main’ function so that it can be placed at the top of the file.

CLI example

Here is an example of running this program with the command-line interface:

sentient --run eight-queens.json --number 0

# standard output:
{"queens":[[1,3],[2,5],[3,7],[4,1],[5,4],[6,2],[7,8],[8,6]]}
{"queens":[[1,4],[2,8],[3,5],[4,3],[5,1],[6,7],[7,2],[8,6]]}
{"queens":[[1,8],[2,2],[3,5],[4,3],[5,1],[6,7],[7,4],[8,6]]}
# ...

Sentient finds 92 unique solutions in about 6 seconds.