Adiar 2.1.0
An External Memory Decision Diagram Library
Loading...
Searching...
No Matches
Queens

Queens

The queens problem is a classic problem that is easy to state and understand but fascinatingly hard to solve efficiently.

‍Given \(N\), in how many ways can \(N\) queens be placed on an \(N \times N\) chess board without threatening each other?

All code shown here can be found in examples/queens.cpp. You can also compile and run this file to play around with it yourself.

Variable Ordering

Well stay with the simple row-by-row ordering of variables for now. That is, we represent whether a queen is placed at position \((i,j)\) on an \(N \times N\) chess board as the truth value of the BDD variable \(x_{i,j} := x_{N\cdot i+j}\).

In C++, we can derive the label of each chess board position as follows.

inline typename adiar::bdd::label_type label_of_position(uint64_t i, uint64_t j)
{
return (N * i) + j;
}
node_type::label_type label_type
Type of this node's variable label.
Definition dd.h:282

Constructing the Board

We construct the set of solutions for the Queens problem as described by Kunkle, Slavici, and Cooperman.

  • [Kunkle10] Daniel Kunkle, Vlad Slavici, Gene Cooperman. “*Parallel Disk-Based Computation for Large, Monolithic Binary Decision Diagrams*”. In: PASCO '10: Proceedings of the 4th International Workshop on Parallel and Symbolic Computation. 2010

S(i,j) : Single Position

Let us first restrict our attention to the base case of expressing the state of a single cell \((i,j)\). We need to express that a single queen is placed here and that it is in no conflict with any other queens on the board, i.e. there cannot be any queen on the same row, column or diagonal.

┌─────────────────┐
8 │╲ │ ╱ │
7 │ ╲ │ ╱ │
6 │ ╲│ ╱ │
5 │─────👑──────────│
4 │ ╱│ ╲ │
3 │ ╱ │ ╲ │
2 │╱ │ ╲ │
1 │ │ ╲ │
└─────────────────┘
a b c d e f g h

This essentially is the formula \(fx_{i,j} \wedge \neg \mathit{is\_threatened}(i,j)\) where \(\mathit{is\_threatened}(i,j)\) is \(\top\) if one or more queens are placed on conflicting positions. We could construct this BDD using adiar::bdd_ithvar, adiar::bdd_not, and adiar::bdd_and. Yet, the resulting (reduced) BDD is very well structured. So, we can construct it explicitly! All BDDs are stored on disk bottom-up, so we'll have to start at the bottom-right corner and work ourselves back up to the top-left corner. We can skip all labels for cells that don't lie on the same row, column or the two diagonals. For the remaining cells, we have to check that all but the one for cell \((i,j)\) they are \(\bot\) while \((i,j)\) is \(\top\).

For example, for \(N = 3\) and \((i,j) = (1,0)\), i.e. for a queen placed at position 2A on a \(3\times 3\) chess board, the variable is \(x_3\) and no queen is allowed to be placed on the same row, \(x_4\) and \(x_5\), nor its column, \(x_0\) and \(6\), nor either column, \(x_1\) and \(x_7\). The resulting BDD looks like this.

Since we construct it explicitly using the adiar::bdd_builder, then the work we do in the base case goes down to only \(O(\text{scan}(N))\) time I/Os rather than \(O(\text{sort}(Nˆ2))\). One pretty much cannot do this base case faster.

adiar::bdd queens_S(int i, int j)
{
int row = N - 1;
adiar::bdd_ptr next = builder.add_node(true);
do {
int row_diff = std::max(row,i) - std::min(row,i);
if (row_diff == 0) {
// On row of the queen in question
int column = N - 1;
do {
typename adiar::bdd::label_type label = label_of_position(row, column);
// If (row, column) == (i,j), then the chain goes through high because
// then we need to check the queen actually is placed here.
next = column == j
? builder.add_node(label, false, next)
: builder.add_node(label, next, false);
} while (column-- > 0);
} else {
// On another row
if (j + row_diff < N) {
// Diagonal to the right is within bounds
next = builder.add_node(label_of_position(row, j + row_diff), next, false);
}
// Column
next = builder.add_node(label_of_position(row, j), next, false);
if (row_diff <= j) {
// Diagonal to the left is within bounds
next = builder.add_node(label_of_position(row, j - row_diff), next, false);
}
}
} while (row-- > 0);
adiar::bdd res = builder.build();
largest_nodes = std::max(largest_nodes, bdd_nodecount(res));
return res;
}
A reduced Binary Decision Diagram.
Definition bdd.h:53
The pointer type that builders use to identify the nodes they have constructed in a decision diagram.
Definition builder.h:54
A builder for decision diagrams.
Definition builder.h:146
builder_ptr< Policy > add_node(typename Policy::label_type label, const builder_ptr< Policy > &low, const builder_ptr< Policy > &high)
Add an internal node with a given label and its two children.
Definition builder.h:241
Policy::dd_type build()
Builds the decision diagram with the added nodes. This also clears the builder.
Definition builder.h:420
size_t bdd_nodecount(const bdd &f)
The number of (internal) nodes used to represent the function.

R(i) : Row

Now that we have a formula each cell, we can accumulate them with an \(\vee\). This ensures that there is at least one queen on each row since each n_queens_S is only \(\top\) if the queen is placed. Furthermore, the placed queen(s) are not in conflicts. Implicitly, this also provides an at-most-one constraints.

We could do so in two ways:

  • Recursively split the row in half until we reach the base case of n_queens_S. This will minimise the number of Apply's that we will make.
  • Similar to a list.fold in functional programming languages, we iteratively combine them. This will minimise the number of BDDs that are "active" at any given time, since we only need to persist the input and output of each iteration.

For Adiar to be able to achieve optimality on disk, it sacrifices the possibility of a hash-table to instantiate the entire forest of all currently active BDDs. In other words, each BDD is completely separate and no memory is saved if there is a major overlap. So, we will choose to do it iteratively.

adiar::bdd queens_R(int i)
{
adiar::bdd out = queens_S(i, 0);
for (int j = 1; j < N; j++) {
out |= queens_S(i, j);
largest_nodes = std::max(largest_nodes, bdd_nodecount(out));
}
return out;
}

B() : Board

Now that we have each entire row done, we only need to combine them. Here we again iterate over all rows to combine them one-by-one. One can probably remove the code duplication that we now introduce.

adiar::bdd queens_B()
{
if (N == 1) {
return queens_S(0, 0);
}
adiar::bdd out = queens_R(0);
for (int i = 1; i < N; i++) {
out &= queens_R(i);
largest_nodes = std::max(largest_nodes, bdd_nodecount(out));
}
return out;
}

Counting Solutions

Above, we constructed a single BDD that os \(\top\) if and only if we have placed \(N\) queen on each row and without putting them in conflict with each other. That is, we have constructed the set of all valid solutions to the Queens problem. So, now we can merely count the number of satisfying assignments.

uint64_t queens_count(const adiar::bdd &board)
{
return adiar::bdd_satcount(board);
}
uint64_t bdd_satcount(const bdd &f, bdd::label_type varcount)
Count the number of assignments x that make f(x) true.

Enumerating all Solutions

Based on this project report by Thorbjørn Nielsen and Martin Faartoft, we can use the BDD constructed above to guide a recursive procedure to enumerate all satisfying solutions. The BDD prunes the search tree when recursing.

Starting from the BDD created with queens_B above, we use adiar::bdd_restrict to place queens one row at a time: starting from the left-most column in a row, we place the queen and then recurse. Recursion can stop early in two cases:

  • If the given BDD already is trivially false. We have placed a queen, such that it conflicts with another.
  • If the number of unique paths in the restricted BDD is exactly one. Then we are forced to place the remaining queens.

Since we want to back track in our choices, we may keep BDDs for each column. This is easily achieved by writing it as a recursive procedure. One should notice though, that this will result in multiple BDDs concurrently being instantiated in memory or on disk at the same time.

uint64_t queens_list_rec(uint64_t N, uint64_t row,
std::vector<uint64_t>& partial_assignment,
const adiar::bdd& constraints)
{
if (adiar::bdd_isfalse(constraints)) {
return 0;
}
deepest_row = std::max(deepest_row, row);
uint64_t solutions = 0;
for (uint64_t col_q = 0; col_q < N; col_q++) {
partial_assignment.push_back(col_q);
// Construct the assignment for this entire row
std::vector<adiar::pair<adiar::bdd::label_type, bool>> column_assignment;
for (uint64_t col = 0; col < N; col++) {
column_assignment.push_back({label_of_position(row, col), col == col_q});
}
adiar::bdd restricted_constraints = adiar::bdd_restrict(constraints,
column_assignment.begin(),
column_assignment.end());
if (adiar::bdd_pathcount(restricted_constraints) == 1) {
solutions += 1;
// Obtain the lexicographically minimal true assignment. Well, only one
// exists, so we get the only one left.
adiar::bdd_satmin(restricted_constraints,
[&partial_assignment](adiar::pair<adiar::bdd::label_type, bool> xv) {
// Skip all empty cells, i.e. assignments to `false`.
if (!xv.second) { return; }
// Push non-empty cells, i.e. assignments to `true`. Since `bdd_satmin`
// provides the assignment (ascendingly) according to the variable
// ordering, then we can merely push to `partial_assignment`
partial_assignment.push_back(xv.first);
});
print_assignment(partial_assignment);
// Forget the forced assignment again
for (uint64_t r = N-1; r > row; r--) {
partial_assignment.pop_back();
}
} else if (adiar::bdd_istrue(restricted_constraints)) {
print_assignment(partial_assignment);
solutions += 1;
} else {
solutions += queens_list_rec(N, row+1, partial_assignment, restricted_constraints);
}
partial_assignment.pop_back();
}
return solutions;
}
bool bdd_istrue(const bdd &f)
Whether a BDD is the constant true.
bdd bdd_satmin(const bdd &f)
The lexicographically smallest cube x such that f(x) is true.
bool bdd_isfalse(const bdd &f)
Whether a BDD is the constant false.
uint64_t bdd_pathcount(const bdd &f)
Count all unique (but not necessarily disjoint) paths to the true terminal.
__bdd bdd_restrict(const bdd &f, bdd::label_type var, bool val)
Restrict a single variable to a constant value.
std::pair< T1, T2 > pair
A pair of values.
Definition types.h:53

The recursion can then be started with an empty assignment.

uint64_t queens_list(uint64_t N, const adiar::bdd& board)
{
std::cout << "| | solutions:" << std::endl;
if (N == 1) {
// To make the recursive function work for N = 1 we would have to have the
// adiar::count_paths check above at the beginning. That would in all other
// cases merely result in an unecessary counting of paths at the very start.
std::vector<uint64_t> assignment { 0 };
print_assignment(assignment);
return 1;
}
std::vector<uint64_t> partial_assignment { };
partial_assignment.reserve(N);
return queens_list_rec(N, 0, partial_assignment, board);
}

This uses a helper function, print_assignment which converts the variable labels \(0, 1, \dots, N^2-1\) back to their coordinate and prints them in chess notation.

void print_assignment(std::vector<uint64_t>& assignment)
{
std::cout << "| | | ";
for (char i = 0; i < N; ++i) {
const char col = 'A' + i;
const char row = '1' + (assignment.at(i) % N);
std::cout << row << col << " ";
}
std::cout << "\n";
}