# Solving 8 Queens Puzzle with Alloy

### david karapetyan γ»3 min read

Continuing the series on Alloy this time we'll solve the 8 queens puzzle because it is another example of a problem easily expressed using constraint programming. The gist is that we want to place 8 queens on an 8x8 chess board such that no two queens attack each other.

We start off by describing the components of the puzzle

```
// Queens are placed on boards.
some sig Queen { }
// The coordinates on the board.
let positions = { i: Int, j: Int | 0 <= i && i <= 7 && 0 <= j && j <= 7 }
// Each position can have at most one queen occupying it and each queen
// has exactly one position assigned.
one sig Board { queens: positions one -> lone Queen }
```

We want non-trivial solutions so we make sure there is at least 1 queen (`some ...`

). The positions of the board hopefully are obvious and are just the row and column numbers of an 8x8 chess board. The board is a little trickier to explain because of the `... one -> lone ...`

syntax but I'll try to explain anyway.

In Alloy we work with relations and the signature of the board says that it consists of a mapping from positions to queens (`... queens: positions one -> lone Queen ...`

). We have some tuples like `(i, j, q)`

where `i`

and `j`

are the row and column of the position of the queen `q`

. The way to understand the `one`

and `lone`

part is to break it up into two parts, first `positions -> lone Queen`

, and second `Queen -> one positions`

. The first part means that for every position there is at most one queen assigned to it, that's the `lone`

part. The second part says that every queen is assigned exactly one position, that's the `one`

part. Hopefully that's a good enough explanation but if not you can just ignore it for now because the intuition is really just that each queen is assigned a unique position and no two queens can occupy the same space.

With the basic components done we now have to describe the attack constraint. The attack constraint is that no two queens can be placed on the board in a way that allows one to attack the other so we have to express that in terms of the positions. In order to do that I'm going to define a helper function that gives the absolute value difference of two numbers

```
// Absolute value difference for comparing diagonal attack positions.
fun absDifference(m: Int, n: Int): Int {
let difference = minus[m, n] {
difference > 0 => difference else minus[0, difference]
}
}
```

Now we can specify the attack constraint as a predicate

```
// Attack relationship in terms of coordinates.
pred attacks(q1: (Int -> Int), q2: (Int -> Int)) {
let q1row = q1.univ, q1col = univ.q1,
q2row = q2.univ, q2col = univ.q2,
rowDifference = absDifference[q1row, q2row],
colDifference = absDifference[q1col, q2col] {
// Same row attacks
rowDifference = 0 ||
// Same column attacks
colDifference = 0 ||
// Diagonal attacks
rowDifference = colDifference
}
}
```

In plain english the above says that two queens `q1`

and `q2`

attack each other if they're on the same row, the same column, or one of them is on a diagonal attack path of the other. Convince yourself that this is only true when the absolute value of the row differences is the same as the absolute value of the column differences. Think about the formula for lines in the plane in terms of rise over run and what diagonal means on a chess board from the viewpoint of one of the attacking queens.

Now with the attack constraint we can specify the fact that all models, i.e. solutions, must satisfy

```
// Make sure no two queens attack each other.
fact notAttacking {
all q1, q2: Queen | q1 != q2 => !attacks[Board.queens.q1, Board.queens.q2]
}
```

The above says that for any two queens `q1`

and `q2`

if they are unequal then they must not be in attacking positions.

Now we can "run" the model and get the solutions

```
run { } for 1 Board, exactly 8 Queen
```

I've specified that I want 1 board and exactly 8 queens in each instance. See what happens if you don't specify `exactly`

.