Solve with home-grown SAT solver

• Decision variables
  

  Denote the \(n\)-queens on an \(n \times n\) chess board by

  \begin{equation*} X \in \mathbb{B}^{n \times n}, \end{equation*}

  where \(x_{ij} = 1\) iff a queen is at row \(i\) in column \(j\).

  (defun my-queens-variables (size &optional transpose)
    "Return a list of decision variables for SIZE-queen problem.
  
  The result is a list of 3-element lists containing a variable, row, and
  column, all positive integers.  The lists are returned in row-major
  order for reproducibility and testability.  With TRANSPOSE, the board is
  transposed and the lists are returned in column-major mode."
    (mapcan (lambda (row)
              (mapcar (lambda (column)
                        (let ((variable (+ (* (1- row) size) column)))
                          (append (list variable)
                                  (or (and transpose (list column row))
                                      (list row column)))))
                      (number-sequence 1 size)))
            (number-sequence 1 size)))
  

  (ert-deftest my-queens-variables/2-queens/row-major ()
    (should (equal (my-queens-variables 2)
                   '((1 1 1) (2 1 2)
                     (3 2 1) (4 2 2)))))
  
  (ert-deftest my-queens-variables/2-queens/column-major ()
    (should (equal (my-queens-variables 2 t)
                   '((1 1 1) (2 2 1)
                     (3 1 2) (4 2 2)))))
  
  (ert-deftest my-queens-variables/3-queens/row-major ()
    (should (equal (my-queens-variables 3)
                   '((1 1 1) (2 1 2) (3 1 3)
                     (4 2 1) (5 2 2) (6 2 3)
                     (7 3 1) (8 3 2) (9 3 3)))))
  
  (ert-deftest my-queens-variables/3-queens/column-major ()
    (should (equal (my-queens-variables 3 t)
                   '((1 1 1) (2 2 1) (3 3 1)
                     (4 1 2) (5 2 2) (6 3 2)
                     (7 1 3) (8 2 3) (9 3 3)))))
  

• Constraints: Population
  

  Enforce at least one queen in every row and column,

  \begin{equation*} \forall (1 \leq i \leq n) \quad \sum_{j = 1}^{n} x_{ij} \geq 1, \end{equation*}

  transformed to the conjunctive normal form as

  \begin{equation*} \forall i \bigvee_{j = 1}^{n} x_{ij} \qand \forall j \bigvee_{i = 1}^{n} x_{ij}. \end{equation*}

  (defun my-queens-at-least-one-per-row-clauses (size &optional transpose)
    "Return CNF clauses enforcing at least one queen per row.
  
  Implements constraints for SIZE-queens puzzle.  With non-nil TRANSPOSE,
  enforce at least one queen per column, instead of row.
  
  The result is a list of lists containing literals, non-zero integers
  representing variables, possibly negated.  All returned clauses and
  literals are sorted for testability and reproducibility."
    (sort (mapcar (lambda (row)
                    (mapcan (pcase-lambda (`(,variable ,row* _column))
                              (if (= row* row) (list variable)))
                            (my-queens-variables size transpose)))
                  (number-sequence 1 size))))
  

  (ert-deftest my-queens-at-least-one-per-row-clauses/size-2 ()
    (should (equal (my-queens-at-least-one-per-row-clauses 2)
                   '((1 2)
                     (3 4)))))
  
  (ert-deftest my-queens-at-least-one-per-row-clauses/size-2/transpose ()
    (should (equal (my-queens-at-least-one-per-row-clauses 2 t)
                   '((1 3)
                     (2 4)))))
  
  (ert-deftest my-queens-at-least-one-per-row-clauses/size-3 ()
    (should (equal (my-queens-at-least-one-per-row-clauses 3)
                   '((1 2 3)
                     (4 5 6)
                     (7 8 9)))))
  
  (ert-deftest my-queens-at-least-one-per-row-clauses/size-3/transpose ()
    (should (equal (my-queens-at-least-one-per-row-clauses 3 t)
                   '((1 4 7)
                     (2 5 8)
                     (3 6 9)))))
  

• Constraints: Orthogonal threats
  

  Enforce at most one queen in every row and column,

  \begin{equation*} \forall (1 \leq i \leq n) \quad \sum_{j = 1}^{n} x_{ij} \leq 1, \end{equation*}

  transformed to the conjunctive normal form as

  \begin{align*} \forall (i, j) \> \forall (j' > j) \quad & (\lnot x_{ij} \lor \lnot x_{ij'}) \\ \forall (i, j) \> \forall (i' > i) \quad & (\lnot x_{ij} \lor \lnot x_{i'j}). \end{align*}

  (defun my-queens-orthogonal-threat-clauses (size &optional transpose)
    "Return CNF clauses enforcing at most one queen per row.
  
  Implements constraints for SIZE-queens puzzle.  With non-nil TRANSPOSE,
  enforce at most one queen per column, instead of row.
  
  The result is a list of lists containing literals, non-zero integers
  representing variables, possibly negated.  All returned clauses and
  literals are sorted for testability and reproducibility."
    (let ((variables (my-queens-variables size transpose)))
      (sort (mapcan (pcase-lambda (`(,variable ,row ,column))
                      (mapcan (pcase-lambda (`(,variable* ,row* ,column*))
                                (if (and (= row* row)
                                         (> column* column))
                                    (list (list (- variable*)
                                                (- variable)))))
                              variables))
                    variables))))
  

  (ert-deftest my-queens-at-most-one-per-row-clauses/size-2 ()
    (should (equal (my-queens-at-most-one-per-row-clauses 2)
                   '((-4 -3) (-2 -1)))))
  
  (ert-deftest my-queens-at-most-one-per-row-clauses/size-2/transpose ()
    (should (equal (my-queens-at-most-one-per-row-clauses 2 t)
                   '((-4 -2) (-3 -1)))))
  
  (ert-deftest my-queens-at-most-one-per-row-clauses/size-3 ()
    (should (equal (my-queens-at-most-one-per-row-clauses 3)
                   '((-9 -8)
                     (-9 -7)
                     (-8 -7)
                     (-6 -5)
                     (-6 -4)
                     (-5 -4)
                     (-3 -2)
                     (-3 -1)
                     (-2 -1)))))
  
  (ert-deftest my-queens-at-most-one-per-row-clauses/size-3/transpose ()
    (should (equal (my-queens-at-most-one-per-row-clauses 3 t)
                   '((-9 -6)
                     (-9 -3)
                     (-8 -5)
                     (-8 -2)
                     (-7 -4)
                     (-7 -1)
                     (-6 -3)
                     (-5 -2)
                     (-4 -1)))))
  
  (ert-deftest my-queens-at-most-one-per-row-clauses/size-4 ()
    (should (equal (my-queens-at-most-one-per-row-clauses 4)
                   '((-16 -15)
                     (-16 -14)
                     (-16 -13)
                     (-15 -14)
                     (-15 -13)
                     (-14 -13)
                     (-12 -11)
                     (-12 -10)
                     (-12 -9)
                     (-11 -10)
                     (-11 -9)
                     (-10 -9)
                     (-8 -7)
                     (-8 -6)
                     (-8 -5)
                     (-7 -6)
                     (-7 -5)
                     (-6 -5)
                     (-4 -3)
                     (-4 -2)
                     (-4 -1)
                     (-3 -2)
                     (-3 -1)
                     (-2 -1)))))
  

• Constraints: Diagonal threats
  

  Ensure at most one queen on every increasing and decreasing diagonal,

  \begin{align*} \forall (i, j) \> \forall(i' > i, j' > j) \quad & (i - j = i' - j') \implies (\lnot x_{ij} \lor \lnot x_{i'j'}) \\ \forall (i, j) \> \forall(i' > i, j' > j) \quad & (i + j = j' + j') \implies (\lnot x_{ij} \lor \lnot x_{i'j'}), \end{align*}

  derived from the constant difference between rows and columns on diagonals

  \begin{equation*} \begin{aligned} i' - i & = j' - j \\ i' + i & = j' + j \end{aligned} \iff \begin{aligned} i - i' & = +j - j' \\ i - i' & = -j + j' \end{aligned} \iff \begin{aligned} \Delta i & = + \Delta j \\ \Delta i & = - \Delta j \end{aligned} \iff \Delta i = \pm \Delta j \, . \end{equation*}

  (defun my-queens-not-sharing-diagonal-clauses (size &optional transpose)
    "Return CNF clauses enforcing at most one queen on decreasing diagonals.
  
  Implements constraints for SIZE-queens puzzle.  With non-nil TRANSPOSE,
  enforce at most most queen on increasing diagonals instead of decreasing
  diagonals.
  
  The result is a list of lists containing literals, non-zero integers
  representing variables, possibly negated.  All returned clauses and
  literals are sorted for testability and reproducibility."
    (sort (mapcan (pcase-lambda (`(,variable ,row ,column))
                    (mapcan (pcase-lambda (`(,variable* ,row* ,column*))
                              (when (or (and transpose
                                             (> row* row)
                                             (< column* column)
                                             (= (+ row column)
                                                (+ row* column*)))
                                        (and (not transpose)
                                             (> row* row)
                                             (> column* column)
                                             (= (- row column)
                                                (- row* column*))))
                                (list (sort (list (- variable)
                                                  (- variable*))))))
                            (my-queens-variables size)))
                  (my-queens-variables size))))
  
  

  (ert-deftest my-queens-not-sharing-diagonal-clauses/size-2 ()
    (should (equal (my-queens-not-sharing-diagonal-clauses 2)
                   '((-4 -1)))))
  
  (ert-deftest my-queens-not-sharing-diagonal-clauses/size-2/anti-diagonal ()
    (should (equal (my-queens-not-sharing-diagonal-clauses 2 t)
                   '((-3 -2)))))
  
  (ert-deftest my-queens-not-sharing-diagonal-clauses/size-3 ()
    (should (equal (my-queens-not-sharing-diagonal-clauses 3)
                   '((-9 -5)
                     (-9 -1)
                     (-8 -4)
                     (-6 -2)
                     (-5 -1)))))
  
  (ert-deftest my-queens-not-sharing-diagonal-clauses/size-3/anti-diagonal ()
    (should (equal (my-queens-not-sharing-diagonal-clauses 3 t)
                   '((-8 -6)
                     (-7 -5)
                     (-7 -3)
                     (-5 -3)
                     (-4 -2)))))
  
  (ert-deftest my-queens-not-sharing-diagonal-clauses/size-4 ()
    (should (equal (my-queens-not-sharing-diagonal-clauses 4)
                   '((-16 -11)
                     (-16 -6)
                     (-16 -1)
                     (-15 -10)
                     (-15 -5)
                     (-14 -9)
                     (-12 -7)
                     (-12 -2)
                     (-11 -6)
                     (-11 -1)
                     (-10 -5)
                     (-8 -3)
                     (-7 -2)
                     (-6 -1)))))
  

• Solver
  

  Define \(N\)-queens solver

  (defun my-queens (&optional size all-solutions-p)
    (let ((size (or size 8)))
      (my-sat-solve (append (my-queens-at-least-one-per-row-clauses size)
                            (my-queens-at-least-one-per-row-clauses size t)
                            (my-queens-at-most-one-per-row-clauses size)
                            (my-queens-at-most-one-per-row-clauses size t)
                            (my-queens-not-sharing-diagonal-clauses size)
                            (my-queens-not-sharing-diagonal-clauses size t))
                    all-solutions-p)))
  

• Solution formatter
  

  (defun my-queens-chess-position (variable size)
    "Return a file-rank string for SOLUTION."
    (let ((file (+ ?a (mod (1- variable) size)))
          (rank (- size (/ (1- variable) size))))
      (format "%c%d" file rank)))
  
  (defun my-queens-chess-pieces (solution)
    "Return a list of piece-file-rank strings for SOLUTION."
    (let ((size (truncate (sqrt (length solution)))))
      (mapcan (pcase-lambda (`(,variable . ,value))
                (when (= value 1)
                  (list (concat "q" (my-queens-chess-position variable size)))))
              solution)))
  
  (defun my-queens-render-solution (solution)
    "Return LaTeX source code that renders SOLUTION."
    (let ((size (truncate (sqrt (length solution)))))
      (format "\\chessboard[smallboard, maxfield=%s, setpieces={%s}]"
              (my-queens-chess-position size size)
              (string-join (sort (my-queens-chess-pieces solution)) ", "))))
  
  (defun my-queens-render-solutions (solutions)
    "Return LaTeX source code that renders SOLUTIONS."
    (string-join
     (append '("\\begin{flushleft}")
             (mapcar (lambda (solution)
                       (concat "  " (my-queens-render-solution solution)))
                     solutions)
             '("\\end{flushleft}"))
     "\n"))
  

  (ert-deftest my-queens-render-solutions/size-2 ()
    (should (equal (my-queens-render-solutions '(((1 . 1) (2 . 0)
                                                  (3 . 0) (4 . 1))))
                   "\\begin{flushleft}
    \\chessboard[smallboard, maxfield=b2, setpieces={qa2, qb1}]
  \\end{flushleft}")))
  
  (ert-deftest my-queens-render-solutions/size-2/different ()
    (should (equal (my-queens-render-solutions '(((1 . 0) (2 . 1)
                                                  (3 . 1) (4 . 0))))
                   "\\begin{flushleft}
    \\chessboard[smallboard, maxfield=b2, setpieces={qa1, qb2}]
  \\end{flushleft}")))
  
  (ert-deftest my-queens-render-solutions/size-2/multiple ()
    (should (equal (my-queens-render-solutions '(((1 . 1) (2 . 0)
                                                  (3 . 0) (4 . 1))
                                                 ((1 . 0) (2 . 1)
                                                  (3 . 1) (4 . 0))))
                   "\\begin{flushleft}
    \\chessboard[smallboard, maxfield=b2, setpieces={qa2, qb1}]
    \\chessboard[smallboard, maxfield=b2, setpieces={qa1, qb2}]
  \\end{flushleft}")))
  
  (ert-deftest my-queens-render-solutions/size-3 ()
    (should (equal (my-queens-render-solutions '(((1 . 0) (2 . 0) (3 . 0)
                                                  (4 . 0) (5 . 0) (6 . 0)
                                                  (7 . 0) (8 . 0) (9 . 1))))
                   "\\begin{flushleft}
    \\chessboard[smallboard, maxfield=c3, setpieces={qc1}]
  \\end{flushleft}")))
  

• Solutions
  

  \(n = 1\)-queens trivial,

  (my-queens-render-solutions (my-queens 1 t))
  

  

  \(n = 2\) and \(n = 3\)-queens have no solutions

  (list (length (my-queens 2 t))
        (length (my-queens 3 t)))
  

  (0 0)
  

  \(n = 4\)-queens has two solutions,

  (my-queens-render-solutions (my-queens 4 t))
  

  

  and the traditional \(n = 8\)-queens has

  (length (my-queens 8 t))
  

  92
  

  solutions, one of them being

  (my-queens-render-solutions (my-queens 8))