SAT solvers and scripts to find solutions to Martin Gardner's minimum no-3-in-a-line problem. Utilizes the sat13 SAT solver written by D. E. Knuth in the CWEB programming language by Knuth and Levy, the Stanford GraphBase (SGB) by Knuth, adaptations of scripts by Knuth to encode the no3 problem in Conjunctive Normal Form (CNF)--these scripts are contained in in the folder nothree. We also added scripts to convert this encoding to the DIMACS format & back in order to search exhaustively for solutions to the no3 problem using a blocking clause, all-solutions SAT solver.
Using this software we were able to find good placements of n+1 queens on only odd rows and columns for odd n up to n = 41. Previously there were only upper bounds established for up to n=18.
Additionally, we found exhaustive lists of good placements of up to n+1 queens for odd n up to 19. These findings are summarized in the following table:
Board Size (n) | 5 | 7 | 9 | 11 | 13 | 15 | 17 | 19 |
-----------------+---+---+---+----+----+----+----+-----
# of Placements | 1 | 2 | 2 | 6 | 15 | 23 | 44 | 65 |
The number of placements are up to listed symmetry; e.g. placements which differed only by a reflection or a rotation were not counted multiple times.
Based on these results, we suggest an upper bound of n+1 for odd n. With Cooper, Pikhurko, Schmitt, and Warrington's result, this would confine the problem solution to {n,n+1} except when n is congruent to 3 modulo 4, where one fewer queen may suffice.