general.hpp File Reference

Plans on the n queens problem. More...

Go to the source code of this file.

Detailed Description

Plans on the n queens problem.

Update namespace.
Create milestones.
Literature review
  • What is the complexity of finding one solution and of counting all solutions (in n) ?
    1. A first introduction one finds in http://en.wikipedia.org/wiki/Eight_queens_puzzle.
    2. There is also an algorithm given for quickly finding one solution, so that's not a problem (but see below).
    3. The true challenge is counting all solutions.
    4. http://www.research.att.com/~njas/sequences/A000170 shows the current state-of-the-art: With a lot of computing power n = 25 was solved recently.
    5. 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, 31-35, 1992] apparently the n-Queens problem is considered with a heuristics similar (in "spirit") to the tau-heuristics.
  • Compare "Heuristics" in ComputerAlgebra/Satisfiability/Lisp/Backtracking/plans/general.hpp.
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 CSP-problem (see Transformers/CrispCSP/plans/general.hpp and ComputerAlgebra/Satisfiability/Lisp/ConstraintProblems/Generators.mac).
    1. The following assumes the columns-representation (see below).
    2. The conditions on the moves of the queens can be formulated directly by one constraint.
    3. 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.
    4. 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??)
    5. The quest is to use more active *clauses* (like the bijectivity condition).
  • And, of course, various (generalised) clause-sets- formulations.
  • And, of course, active clause-sets.
Different formulations
  • The most "natural" perspective is the queens-perspective, 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 queens-perspective 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 state-space n^n. It seems that this perspective is inherently better than the "extreme" queens-perspective from above (but perhaps this "extreme" perspective has other representations in it(!)).
  • One could also consider the field-perspective, that is, n^2 boolean variables (with a queen or not). This yields the state-space 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 n-Queens] seems to be the major study.
Active clause-sets for the moves-condition
  • In the following we are using the columns-perspective (see above).
  • The domain association perhaps best is realised here as a square matrix of order n with boolean entries.
  • Propagation happens as follows:
    1. There is the deque of unit-clauses 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).
    2. 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)).
    3. 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).
    4. We stop processing once a round didn't create a new unit-clause.
    5. Since we need only to run through all current unit-clauses and to add to the right, remove from the left, perhaps a list is better than a deque.
    6. 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 look-ahead for this condition (that is, the condition strengthened by (complete) look-ahead) could be implement more efficient, using the properties of this special case? In general, when implementing the look-ahead as an operator (creating a new active clause-set from a given one), it would need from the given active clause-set the set of implied units (and the given active clause-set should be operatable in "look-ahead 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!
    1. 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.
    2. More generally, the question is about the abbove different problem formulation, and whether the n-queens active-clause-set can actually be turned into an active clause.
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/uec-is-2004-06.pdf, [Solving the 24-queens Problem using MPI on a PC Cluster]. Likely the numbers need to be divided by 2 due to the simple symmetry-trick.
  • 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:
    1. This should work very well with a look-ahead architecture.
    2. 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.
    3. One would assume that not much load balancing is needed, but that automatically the 2^d processes are very similar.
    4. 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 non-boolean clause-sets.)

Definition in file general.hpp.