Plans on the n queens problem.
More...
Go to the source code of this file.
Detailed Description
Plans on the n queens problem.
 Todo:
 Update namespace.
 Todo:
 Create milestones.
 Todo:
 Literature review

What is the complexity of finding one solution and of counting all solutions (in n) ?

A first introduction one finds in http://en.wikipedia.org/wiki/Eight_queens_puzzle.

There is also an algorithm given for quickly finding one solution, so that's not a problem (but see below).

The true challenge is counting all solutions.

http://www.research.att.com/~njas/sequences/A000170 shows the current stateoftheart: With a lot of computing power n = 25 was solved recently.

http://www.research.att.com/~njas/sequences/A002562 is about counting symmetric solutions only once. Here only n = 23 is known.
If we could count for n=26, this would yield some nice publicity.

http://www.liacs.nl/home/kosters/nqueens.html is a collection of literature.

One can also consider the enumeration of all solutions, for example in lexicographical order, with polynomial delay (or finding the first and the next solution).

For what n can solvers find one solutions, and for what n can one find all solutions (or count them) ?

In [P.A.Geelen. Dual viewpoint heuristics for binary constraint satisfaction problems. 10th European Conference on Artificial Intelligence, 3135, 1992] apparently the nQueens problem is considered with a heuristics similar (in "spirit") to the tauheuristics.

Compare "Heuristics" in ComputerAlgebra/Satisfiability/Lisp/Backtracking/plans/general.hpp.
 Todo:
 Organisation
 Todo:
 Different perspectives:

A natural formulation considers the hypergraph with n^2 vertices and with hyperedges corresponding to the rows, columns and diagonals, and searches for a strong independent set (see Hypergraphs/IndependentSets/plans/general.hpp) of size n.

Another formulation is as a crisp CSPproblem (see Transformers/CrispCSP/plans/general.hpp and ComputerAlgebra/Satisfiability/Lisp/ConstraintProblems/Generators.mac).

The following assumes the columnsrepresentation (see below).

The conditions on the moves of the queens can be formulated directly by one constraint.

More powerfull is to use two constraints, one is the bijectivity constraint, and the other captures the 2 * (2 n  1) diagonales: The power comes from the bijectivity constraint.

The bijectivity constraint allows for intelligent algorithms; it comprises the vertical and horizontal moves. Could one also have such matching techniques for the diagonal moves? (Or for all moves together??)

The quest is to use more active *clauses* (like the bijectivity condition).

And, of course, various (generalised) clausesets formulations.

And, of course, active clausesets.
 Todo:
 Different formulations

The most "natural" perspective is the queensperspective, that is, n variables for the n queens (where the value set is the set of squares). The set of total assignments has size n^(n^2) here.

The queensperspective has the disadvantage of added symmetries, which are avoided by the column perspective (n variables for the columns, each with values {1,...,n}), or, equivalently, the row perspective. We get the smaller statespace n^n. It seems that this perspective is inherently better than the "extreme" queensperspective from above (but perhaps this "extreme" perspective has other representations in it(!)).

One could also consider the fieldperspective, that is, n^2 boolean variables (with a queen or not). This yields the statespace size 2^(n^2).

And one can combine these perspectives.

See [Barbara M. Smith, Modelling, 2006] for an entry into the literature; [Nadel 2006; Representation Selection for Constraint Satisfaction: A Case Study Using nQueens] seems to be the major study.
 Todo:
 Active clausesets for the movescondition

In the following we are using the columnsperspective (see above).

The domain association perhaps best is realised here as a square matrix of order n with boolean entries.

Propagation happens as follows:

There is the deque of unitclauses to be processed. Once we reach a column (again) which is in this deque we remove it (this should always be the leftmost entry of the deque).

We run through all columns from left to right, at each step always performing all eliminations for all elements of the deque (respectively removing it from the deque if we reach it (again)).

When processing a column and we find it become a unit, it is (immediately) added to the end of the deque (and thus is processed directly with the new column).

We stop processing once a round didn't create a new unitclause.

Since we need only to run through all current unitclauses and to add to the right, remove from the left, perhaps a list is better than a deque.

We also stop once a column becomes empty. We have counters for the domain sizes (the occupied elements in a column).

An interesting question is, whether the lookahead for this condition (that is, the condition strengthened by (complete) lookahead) could be implement more efficient, using the properties of this special case? In general, when implementing the lookahead as an operator (creating a new active clauseset from a given one), it would need from the given active clauseset the set of implied units (and the given active clauseset should be operatable in "lookahead mode").

As noted above, for for each n the problem is solvable and and also to find one solution is easy, however the real question is about the complexity of the *partially instantiated* board!

The most intuitive situation is, that some queens are already placed on the board, and the problem is to decide whether this position can be extended to one using n queens.

More generally, the question is about the abbove different problem formulation, and whether the nqueens activeclauseset can actually be turned into an active clause.
 Todo:
 The challenge of counting

The big problem for counting all solutions is the large number of solutions, which are all total, and thus a SAT solver, which must create a node for each such (total) solution, has to create a large number of nodes even if he can completely avoid to explore unsatisfiable nodes.

One possibility would be to invent some new form of ("intelligent") literals which would allow for partial solutions.

Another possibility is to use symmetry; though it seems that counting solutions modulo symmetry makes the problem actually harder. Of course, the question here is what kinds of symmetries to consider.

The program apparently currently the fastest (jmsnqueens.zip; see Buildsystem/ExternalSources/SpecialBuilds/plans/SAT.hpp), is actually a very simple backtracker! It's all about brute force.

The current best processing speed seems to be around 1.7 * 10^6 solutions per second for n=17, and 10^6 solutions per second for n=23 (Pentium4 Xeon 2.8 GHz; http://www.arch.cs.titech.ac.jp/~kise/doc/paper/uecis200406.pdf, [Solving the 24queens Problem using MPI on a PC Cluster]. Likely the numbers need to be divided by 2 due to the simple symmetrytrick.

So actually, despite its simplicity, the program doesn't seem to spend much time on unsatisfiable branches? One should obtain a node count.

The general question is, how easy it is to avoid unsatisfiable branches (see above). Perhaps it is quite easy?

Parallelisation:

This should work very well with a lookahead architecture.

Basically we have two levels: Say we want to split into 64 problems. Then we look at depth d = 6:

Up to depth d we use strong inference, strong heuristics, etc.

Once the problem is split, then we use weaker methods.

One would assume that not much load balancing is needed, but that automatically the 2^d processes are very similar.

The distributed processes should have many variables already eliminated, and they should be able to exploit this (so "eager
preprocessing" here is needed).

The DNF structure is very "simple": only full clauses. But perhaps the prime implicates have some interesting structure ?!? (Using nonboolean clausesets.)
Definition in file general.hpp.