Rudy's OBTF

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

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