Rudy's OBTF

Home / Computer science / N-queens / 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)))))