Rudy's OBTF

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

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-at-most-one-per-row-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)))))