Rudy's OBTF

Home / Computer science / N-queens / Solve with home-grown SAT solver

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)))))