Acht Damen in core.logic

Hier ist meine core.logic-Lösung für das klassische Damenproblem: acht Damen so auf ein Schachbrett stellen, dass keine zwei sich gegenseitig schlagen können.

Das Schöne daran: Ich sage dem Computer nie, wie er suchen soll. Ich beschreibe, wie eine Lösung aussieht, und die Logik-Engine findet alle.


(ns eight-queens
  (:refer-clojure :exclude [==])
  (:require
   [clojure.string :as str]
   [clojure.core.logic :refer :all :as l]
   [clojure.core.logic.fd :as fd]))

;; Classic AI problem:
;;
;;
;; Find a chess board configuration, where (n=8) queens are on the board;
;; And no pairs attack each other.
;;

;;
;; representation:
;;
;; permutation <0...7>,
;; 1 number per row,
;; so that [0,1,2,3,4,5,6,7] is placing all queens on a diagonal (everybody attacks each other).
;;
;; - constrains the configuration:
;; - all queens are on different rows.
;; - all queens are on different columns.
;;
;; This is fine, because those configurations are not in the set of solutions.
;;
;;

  (defn queens-logic
    [n]
    ;; make (n=8) logic variables, for each row
    (let [colvars (map (fn [i] (l/lvar (str "col-" i))) (range n))]
      (l/run* [q]
        ;; 1. each queen is in a column 0..n-1
        (everyg (fn [lv] (fd/in lv (fd/interval (dec n)))) colvars)
        ;; 2. columns must be different; rows already are (one variable per row): a permutation
        (fd/distinct colvars)
        ;; 3. diagonal constraint
        ;; for each queen, say that the other queens are not attacking diagonally
        (and* (for [i (range n)
                    j (range (inc i) n)
                    :let [row-diff (- j i)
                          ci (nth colvars i)
                          cj (nth colvars j)]]
                (fresh []
                  ;; handle south-east and north-east cases
                  (fd/eq (!= cj (+ ci row-diff)))
                  ;; fd domains are non-negative, so write both diagonals with + instead of -
                  (fd/eq (!= ci (+ cj row-diff))))))
        (l/== q colvars))))

  (take 1 (queens-logic 8))
  '((1 3 5 7 2 0 6 4))

♕

Beim relationalen Programmieren sind die Bausteine Logikvariablen und Ziele (goals). Wir schreiben ein Programm, das die Bedingungen an die Variablen aufstellt, und übergeben es mit run* an die Logik-Engine.

Nach der Wahl der cleveren Darstellung, eine Variable pro Zeile, deren Wert die Spalte der Dame in dieser Zeile ist, programmieren wir die nötigen Bedingungen:

Jede Dame ist eine Zahl zwischen 0 und n-1: die Spalte, auf der sie steht.
Jede Dame hat eine andere Zahl als die anderen: Sie steht in einer anderen Spalte. Die Zeilen sind durch die Konstruktion verschieden. (1 und 2 zusammen sind die Permutationsbedingung.)
Die Damen schlagen sich nicht diagonal: Für die Zeilen i und j dürfen sich die Spalten nicht um genau j - i unterscheiden.

Warum + auf beiden Seiten statt |ci - cj| ! j - i=? Die endlichen Domänen von core.logic enthalten nur nicht-negative ganze Zahlen, also kann ci - row-diff aus der Domäne fallen. Mit cj ! ci + d= und ci ! cj + d= sind beide Diagonalen abgedeckt, und alles bleibt nicht-negativ.

Prüfen, ob es stimmt:

(comment

  ;; reference is defined below
  (def reference-outcome (find-all-solutions 8))

  (def outcome (queens-logic 8))

  [(= (into #{} reference-outcome) (into #{} outcome))
   (every? zero? (map quality reference-outcome))
   (every? zero? (map quality outcome)) (count outcome)]

  ;; =>
  [true true true 92])

Warum relational?

Das relationale Programm und das Backtracking-Programm unten finden dieselben 92 Lösungen. Der Unterschied ist, was ich aufschreiben musste.

Beim Backtracker geht es um die Suche: welches Feld als Nächstes, wann aufgeben, wie zurücknehmen.
Beim relationalen Programm geht es um das Problem: drei Tatsachen über eine Lösung. Die Suche ist Sache der Engine.
Ändert sich das Problem, etwa "eine Dame muss auf a1 stehen", bekommt das relationale Programm eine Zeile mehr, (l/= (first colvars) 0)=, und 4 der 92 Lösungen bleiben übrig. Beim Backtracker muss man an die Suchlogik ran.

Das ist derselbe Hebel wie bei der Datenorientierung: sagen, was, und das Wie weglassen. Mehr dazu.

Offene Fragen:

Von den 92 Lösungen sind nur 12 bis auf Drehung und Spiegelung verschieden.¹ Lässt sich das Brechen der Symmetrie als einfach eine weitere Bedingung ausdrücken, und wie viel schneller wird es dadurch?
Wie skaliert das mit n? Wo hört core.logics fd auf, Spaß zu machen, und wo übernimmt ein SAT-Solver?

Backtracking- und Hill-Climbing-Lösungen, KI-generiert, zum Vergleich und als Referenz zum Prüfen:

;; ============================
;; Helpers and non-relational solutions

(defn quality
  "Count the number of queens attacking each other in the given board configuration.
   board-config is a vector of column positions, one per row.
   Returns the number of pairs of queens that attack each other."
  [board-config]
  (let [n (count board-config)]
    (loop [row1 0
           conflicts 0]
      (if (>= row1 n)
        conflicts
        (let [col1 (nth board-config row1)
              new-conflicts (loop [row2 (inc row1)
                                   acc 0]
                              (if (>= row2 n)
                                acc
                                (let [col2 (nth board-config row2)
                                      ;; Check diagonal attacks
                                      diag-attack? (= (Math/abs (- row1 row2))
                                                      (Math/abs (- col1 col2)))]
                                  (recur (inc row2)
                                         (if diag-attack? (inc acc) acc)))))]
          (recur (inc row1) (+ conflicts new-conflicts)))))))

(defn valid-solution?
  "Returns true if the board configuration has no conflicts."
  [board-config]
  (zero? (quality board-config)))

(defn print-board
  "Prints a visual representation of the board."
  [board-config]
  (let [n (count board-config)]
    (doseq [row (range n)]
      (let [col (nth board-config row)]
        (println (apply str (for [c (range n)]
                              (if (= c col) "Q " ". ")))))))
  (println))

(defn solve-backtrack
  "Solves the N-Queens problem using backtracking.
   Returns the first valid solution found, or nil if none exists."
  [n]
  (letfn [(safe? [board row col]
            (let [board-vec (vec board)]
              ;; Check if placing a queen at [row col] is safe
              (not (some (fn [r]
                           (let [c (nth board-vec r)]
                             (or (= c col)
                                 (= (Math/abs (- r row))
                                    (Math/abs (- c col))))))
                         (range row)))))

          (place-queens [board row]
            (if (= row n)
              board ;; Solution found
              (some (fn [col]
                      (when (safe? board row col)
                        (place-queens (conj board col) (inc row))))
                    (range n))))]

    (place-queens [] 0)))

(defn find-all-solutions
  "Finds all solutions to the N-Queens problem.
   Returns a sequence of all valid board configurations."
  [n]
  (letfn [(safe? [board row col]
            (let [board-vec (vec board)]
              (not (some (fn [r]
                           (let [c (nth board-vec r)]
                             (or (= c col)
                                 (= (Math/abs (- r row))
                                    (Math/abs (- c col))))))
                         (range row)))))

          (place-queens [board row]
            (if (= row n)
              [board] ;; Return solution in a vector
              (mapcat (fn [col]
                        (when (safe? board row col)
                          (place-queens (conj board col) (inc row))))
                      (range n))))]

    (place-queens [] 0)))

(defn random-config
  "Generates a random board configuration of size n."
  [n]
  (vec (shuffle (range n))))


(defn solve-hill-climbing
  "Solves the N-Queens problem using hill climbing with random restarts.
   max-restarts: maximum number of random restarts to attempt.
   max-steps: maximum steps per climb attempt."
  [n & {:keys [max-restarts max-steps]
        :or {max-restarts 100 max-steps 1000}}]
  (letfn [(swap-positions [config i j]
            (assoc config i (nth config j) j (nth config i)))

          (get-neighbors [config]
            (for [i (range n)
                  j (range (inc i) n)]
              (swap-positions config i j)))

          (climb [config steps]
            (if (or (zero? steps) (valid-solution? config))
              config
              (let [current-quality (quality config)
                    neighbors (get-neighbors config)
                    better-neighbors (filter #(< (quality %) current-quality) neighbors)]
                (if (empty? better-neighbors)
                  config ;; Local minimum reached
                  (recur (first (sort-by quality better-neighbors))
                         (dec steps))))))]

    (loop [restarts 0]
      (if (>= restarts max-restarts)
        nil ;; Failed to find solution
        (let [start-config (random-config n)
              result (climb start-config max-steps)]
          (if (valid-solution? result)
            result
            (recur (inc restarts))))))))


(comment
  ;; Example usage:

  ;; Test the quality function
  (quality [0 1 2 3 4 5 6 7]) ;; All on diagonal - many conflicts
  ;; => 28

  (quality [0 4 7 5 2 6 1 3]) ;; A valid solution
  ;; => 0

  ;; Solve for 8 queens using backtracking
  (def solution (solve-backtrack 8))
  solution
  ;; => [0 4 7 5 2 6 1 3]

  (print-board solution)
  ;; Q . . . . . . .
  ;; . . . . Q . . .
  ;; . . . . . . . Q
  ;; . . . . . Q . .
  ;; . . Q . . . . .
  ;; . . . . . . Q .
  ;; . Q . . . . . .
  ;; . . . Q . . . .

  ;; Find all solutions
  (def all-sols (find-all-solutions 8))
  (count all-sols)
  ;; => 92 (there are 92 distinct solutions for 8 queens)

  ;; Solve using hill climbing
  (def hc-solution (solve-hill-climbing 8))
  (print-board hc-solution)

  ;; Test quality on various board sizes
  (quality [0 1]) ;; => 0 (2 queens, no conflict)
  (quality [0 2 1]) ;; => 0 (3 queens, valid)
  (quality [1 3 0 2]) ;; => 0 (4 queens, valid)
  )

Ich könnte alle Lösungen ausgeben. Warum nicht als HTML, damit es auf diesem Blog gerendert wird (der Rendering-Code ist KI-generiert):

(require '[hiccup2.core :as html])

(defn board-to-hiccup
  "Converts a board configuration to hiccup format with checkerboard pattern."
  [board-config]
  (let [n (count board-config)]
    [:div {:style {:display "inline-block"
                   :border "2px solid #333"}}
     (for [row (range n)]
       (let [col (nth board-config row)]
         [:div {:style {:display "flex"}}
          (for [c (range n)]
            (let [is-dark? (odd? (+ row c))
                  has-queen? (= c col)]
              [:div {:style {:width "60px"
                             :height "60px"
                             :background-color (if is-dark? "#769656" "#eeeed2")
                             :display "flex"
                             :align-items "center"
                             :justify-content "center"
                             :font-size "40px"
                             :font-weight "bold"
                             :color "#000"}}
               (when has-queen? "♕")]))]))]))

(spit
 "board.html"
 (html/html
     [:div
      {:style
       {:display "flex"
        :padding "8px"
        :gap "8px"
        :flex-wrap "wrap"}}
      (doall (map board-to-hiccup (queens-logic 8)))]))

Alle Lösungen, einfach weil es geht

♕

Fußnoten:

Damenproblem, Wikipedia: 92 Lösungen, 12 grundlegend verschiedene.

Generiert von Claude im Auftrag von Benjamin Schwerdtner.

ftlm :faster-than-light /memes Joyful ideas are better ideas

Acht Damen in core.logic

Warum relational?

Fußnoten: