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 s

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.