Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.n-queens

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/n_queens.clj1 definitions, 3 theorems

AHoF N-Queens (backtracking constraint satisfaction): place N queens on an NxN board so none attacks another -- the textbook example of backtracking search, which extends a partial placement column by column and abandons (backtracks) any branch that violates a constraint. Placing one queen per column, the remaining conflict is the DIAGONAL attack: two queens attack diagonally exactly when their row distance equals their column distance, attacks-diagonally? row-distance col-distance = (row-distance <= col-distance) AND (col-distance <= row-distance) (i.e. the distances are equal), over exact-rational (integer) distances. Proved native and axiom-free: the diagonal-attack test as the equality of the two distances (a boolean conjunction of two comparisons via logic/if-data); that equal distances are a diagonal attack (the branch is pruned); the certificates that an attack's distances coincide (each at most the other, native nnrat/at-most); and that unequal distances are safe. The row placement and the recursive search are executable; what is proved is the diagonal-conflict decision. Requires audit/decide-nnrat-at-most, logic/if-data, nnrat/at-most, nnrat/decide-at-most-true-sound (all in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.n-queens` prints this classification.

n-queens/attacks-diagonally? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

n-queens/equal-distance-attacks :
  → floyd-cycle/meet? 3 3 = data/true

n-queens/attack-distances-coincide :
  → 3 ≤ 3

n-queens/unequal-distance-safe :
  → floyd-cycle/meet? 3 5 = data/false