Adiar 2.1.0
An External Memory Decision Diagram Library
|
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.
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.
We construct the set of solutions for the Queens problem as described by Kunkle, Slavici, and Cooperman.
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.
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.
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:
n_queens_S
. This will minimise the number of Apply's that we will make.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.
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.
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.
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:
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.
The recursion can then be started with an empty assignment.
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.