6 ms·

Having done academic research into N-Queens, I'll say that this is result is a remarkable step forward and, once vetted, is generations' worth of advancement in

by babel_ 5y ago

Having done academic research into N-Queens, I'll say that this is result is a remarkable step forward and, once vetted, is generations' worth of advancement in establishing the upper and lower bounds of the problem with remarkable precision. Here's to the next few generations taking this technique and not only applying it elsewhere, but also applying it to exactly solving for higher N than 27. It'll be fascinating to see if this supersedes symmetry breaking as done with the Q27 project in allowing us to dispatch far more efficiently the reasonable starting configurations to a highly parallelised #SAT solver, and allows us to come up with branching heuristics that are actually viable (as the research I was involved with showed most simply added overhead and little benefit for an overall negative effect). Edit: here's the arxiv so you can read the actual results, since Quanta makes it surprisingly awkward to look for. https://arxiv.org/abs/2107.13460 https://arxiv.org/abs/2107.13460

CJefferson 5y ago
I'm not convinced a SAT solver will ever be that useful in practice, as finding (huge!) numbers of solutions to N-queens tends to be easy -- so a simpler (specialised) technique will usually churn through solutions faster. While it is true that completing a solution to N-queens is NP-complete (I was an author on the paper that proved that), you need fairly big instances before the problem gets "hard" in practice (at least, as far as we showed).
- kevinwang 5y ago
  Is counting the number of solutions for a given n known to be NP-hard? And is finding any solution for a given n known to be in P? I saw a paper that found solutions up to 500,000 using a probabilistic method but wasn't sure if it was definitively proven to be in P or not.
  - CJefferson 5y ago
    Checking if a partially filled in n-queens problem has a solution at all is NP complete. It might be there is an easy way of counting solutions for an empty grid, but usually the way we count solutions is divide and conquer, by giving different computers partially filled in grids.
    - kevinwang 5y ago
      Interesting, so we don't know that it's np hard, but we basically assume it is? Do you know if anyone has tried to prove that it is?
      - CJefferson 5y ago
        NP-hardness is about yes/no questions, and we already know thwre is an answer to all n-queens instances except 2 and 3 :) It also can't really be #P (which is to do with hardness of counting), as that has to do with "input problem size", and N-queens with an empty grid doesn't have enough structure (as it's just a number) -- this is hard to explain in full in a short message :)
        bjourne 5y ago
        But you can easily phrase it as an NP-hard problem: Are there at least X unique solutions to a board of particular size?
  - CaptainNegative 5y ago
    Technically the answer to the second question is "no" when n is given in binary. As a valid output is Omega(n log n) bits in length, we can't hope to construct a solution in time polynomial in the input size, i.e. time poly(log n). However, when n is given in unary (meaning we have poly(n) time to find and output a solution), there is a 19th century German-language paper by Pauls that explicitly and efficiently constructs an n-queens solution for all n>3. So the unary version of the problem is in FP (the search version equivalent of P). tl;dr a solution to n-queens can be found in deterministic poly(n) time.
- babel_ 5y ago
  So indeed the simpler techniques are the fastest by walltime on the solvable problems; typically shown as N=16 through N=20, or up to N=22 or N=24 if you have sufficient parallelisation available. As you mention, it's not convincing that SAT will be faster in practice, and it's quite possible that it will not. However, if you wish to attack the upper bounds of what needs to be computed for an exact solution, then a SAT solver is no worse than these simple approaches, as in the worst case it could simply fall-back and use the simple logic as a branching heuristic, so it's all about where the gains from being smarter overtake the processing overheads. In reality, a trivial SAT solver based on DPLL actually bears remarkable similarity to the simpler methods, and simply switching to the more straight-forward representation and weakening the propagation and heuristics brings the SAT solver inline with the fastest method. In other words, the simpler methods are a weak SAT solver that is fairly well optimised for N-Queens (at least for low N, but this includes N=27 so it's very practical). As walltimes show, SAT has notable overhead, however if this can be shown to be close enough then this could be an avenue to solving higher N. At worst, using stronger SAT is simply a galactic algorithm that gets better "eventually" (or merely asymptotically). In practice, it may unlock more the ability to incoporate elements of the dynamic programming approach to strongly lower the time needed for larger N, bolstered by strong heuristics, finally going beyond churning through solutions as you described. Even if higher N are infeasible, it could be applicable to, say, verify the results of Q27. I have a lot of respect for work such as proving that N-Queens Completion satisfiability is NP-complete, thank you for your contributions. The research I was involved in ended up proving a few things with regards to what SAT can achieve here, however we have not yet had the chance to publish. Hopefully some time soon. To answer some of the people in sibling and child comments, determining Q(N), aka the number of solutions for N-Queens, is best considered from the perspective of counting the valid solutions to N-Queens Completion over an exhaustive set of starting points (in the simplest, starting with a Queen in a square on the top row), hence it is #P-complete, and full enumeration ends up NP-Hard (which refers to finding the next solution until Q(N) is determined). This is sidestepping the "empty board" concerns, and closer to the practical approach for distributed/parallel solvers. If you use the empty board then the satisfiability is linear in N and solving for Q(N) progresses upwards with exponential complexity (see Rivin and Zabih 1992 for the classic dynamic programming result, or Pratt 2016 for a similar complexity but in only polynomial space). Unfortunately, this is one situation in which the literature is rather confusing, and "N-Queens" is used to mean anything from finding a single non-attacking board (often a challenge for AI students) to the "full" count of how many non-attacking boards (the likes of the Q27 project). There is also confusion over unary vs binary N, which in my experience has just ended up messing with people. Can't fault anyone for that. It's best if you use unary N for this, hence N is the problem size rather than lg(N). This is most consistent with literature and wider research, as only a few consider binary N. It's also what I use above. For those wanting to learn more, see Bell and Stevens 2009, as their survey is pretty comprehensive. J. Bell and B. Stevens, “A survey of known results and research areas for n-queens”, Discrete Mathematics, vol. 309, no. 1, 2009. I. Rivin and R. Zabih, “A dynamic programming solution to the n-queens problem”, Information Processing Letters, vol. 41, no. 5, pp. 253–256, 1992. K. Pratt, “Closed-Form Expressions for the n-Queens Problem and Related Problems”, 2016.

by babel_ 5y ago

CJefferson 5y ago

I'm not convinced a SAT solver will ever be that useful in practice, as finding (huge!) numbers of solutions to N-queens tends to be easy -- so a simpler (specialised) technique will usually churn through solutions faster. While it is true that completing a solution to N-queens is NP-complete (I was an author on the paper that proved that), you need fairly big instances before the problem gets "hard" in practice (at least, as far as we showed).

kevinwang 5y ago
Is counting the number of solutions for a given n known to be NP-hard? And is finding any solution for a given n known to be in P? I saw a paper that found solutions up to 500,000 using a probabilistic method but wasn't sure if it was definitively proven to be in P or not.
- CJefferson 5y ago
  Checking if a partially filled in n-queens problem has a solution at all is NP complete. It might be there is an easy way of counting solutions for an empty grid, but usually the way we count solutions is divide and conquer, by giving different computers partially filled in grids.
  - kevinwang 5y ago
    Interesting, so we don't know that it's np hard, but we basically assume it is? Do you know if anyone has tried to prove that it is?
    - CJefferson 5y ago
      NP-hardness is about yes/no questions, and we already know thwre is an answer to all n-queens instances except 2 and 3 :) It also can't really be #P (which is to do with hardness of counting), as that has to do with "input problem size", and N-queens with an empty grid doesn't have enough structure (as it's just a number) -- this is hard to explain in full in a short message :)
      - bjourne 5y ago
        But you can easily phrase it as an NP-hard problem: Are there at least X unique solutions to a board of particular size?
- CaptainNegative 5y ago
  Technically the answer to the second question is "no" when n is given in binary. As a valid output is Omega(n log n) bits in length, we can't hope to construct a solution in time polynomial in the input size, i.e. time poly(log n). However, when n is given in unary (meaning we have poly(n) time to find and output a solution), there is a 19th century German-language paper by Pauls that explicitly and efficiently constructs an n-queens solution for all n>3. So the unary version of the problem is in FP (the search version equivalent of P). tl;dr a solution to n-queens can be found in deterministic poly(n) time.
babel_ 5y ago
So indeed the simpler techniques are the fastest by walltime on the solvable problems; typically shown as N=16 through N=20, or up to N=22 or N=24 if you have sufficient parallelisation available. As you mention, it's not convincing that SAT will be faster in practice, and it's quite possible that it will not. However, if you wish to attack the upper bounds of what needs to be computed for an exact solution, then a SAT solver is no worse than these simple approaches, as in the worst case it could simply fall-back and use the simple logic as a branching heuristic, so it's all about where the gains from being smarter overtake the processing overheads. In reality, a trivial SAT solver based on DPLL actually bears remarkable similarity to the simpler methods, and simply switching to the more straight-forward representation and weakening the propagation and heuristics brings the SAT solver inline with the fastest method. In other words, the simpler methods are a weak SAT solver that is fairly well optimised for N-Queens (at least for low N, but this includes N=27 so it's very practical). As walltimes show, SAT has notable overhead, however if this can be shown to be close enough then this could be an avenue to solving higher N. At worst, using stronger SAT is simply a galactic algorithm that gets better "eventually" (or merely asymptotically). In practice, it may unlock more the ability to incoporate elements of the dynamic programming approach to strongly lower the time needed for larger N, bolstered by strong heuristics, finally going beyond churning through solutions as you described. Even if higher N are infeasible, it could be applicable to, say, verify the results of Q27. I have a lot of respect for work such as proving that N-Queens Completion satisfiability is NP-complete, thank you for your contributions. The research I was involved in ended up proving a few things with regards to what SAT can achieve here, however we have not yet had the chance to publish. Hopefully some time soon. To answer some of the people in sibling and child comments, determining Q(N), aka the number of solutions for N-Queens, is best considered from the perspective of counting the valid solutions to N-Queens Completion over an exhaustive set of starting points (in the simplest, starting with a Queen in a square on the top row), hence it is #P-complete, and full enumeration ends up NP-Hard (which refers to finding the next solution until Q(N) is determined). This is sidestepping the "empty board" concerns, and closer to the practical approach for distributed/parallel solvers. If you use the empty board then the satisfiability is linear in N and solving for Q(N) progresses upwards with exponential complexity (see Rivin and Zabih 1992 for the classic dynamic programming result, or Pratt 2016 for a similar complexity but in only polynomial space). Unfortunately, this is one situation in which the literature is rather confusing, and "N-Queens" is used to mean anything from finding a single non-attacking board (often a challenge for AI students) to the "full" count of how many non-attacking boards (the likes of the Q27 project). There is also confusion over unary vs binary N, which in my experience has just ended up messing with people. Can't fault anyone for that. It's best if you use unary N for this, hence N is the problem size rather than lg(N). This is most consistent with literature and wider research, as only a few consider binary N. It's also what I use above. For those wanting to learn more, see Bell and Stevens 2009, as their survey is pretty comprehensive. J. Bell and B. Stevens, “A survey of known results and research areas for n-queens”, Discrete Mathematics, vol. 309, no. 1, 2009. I. Rivin and R. Zabih, “A dynamic programming solution to the n-queens problem”, Information Processing Letters, vol. 41, no. 5, pp. 253–256, 1992. K. Pratt, “Closed-Form Expressions for the n-Queens Problem and Related Problems”, 2016.