This string has no description
Something went wrong. Try again.
nqueens.bcdc
· Created 1mo ago ·990 B · 36 lines
12345678910111213141516171819202122232425262728293031323334353637#lang bcdc(define n 8)(define q (ι 'q)); there is exact one queen in every row(define rows (for/list ([y (in-range n)]) (∃! (for/list ([x (in-range n)]) (q y x))))); there is exact one queen in every column(define columns (for/list ([x (in-range n)]) ; NOTE: we can omit the at most one condition, but this ; doesn't necessarily incur optimization on the sat solver side. ; ; (∃≥1 (∃! (for/list ([y (in-range n)]) (q y x))))); there is at most one queen on every diagonal(define diagonals (for*/list ([r1 (in-range n)] [c1 (in-range n)] [r2 (in-range (add1 r1) n)] [c2 (in-range n)] #:when (= (abs (- r1 r2)) (abs (- c1 c2)))) (∃≤1 (list (q r1 c1) (q r2 c2)))))(define model (all (append rows columns diagonals)))(write-dimacs "nqueens-8.cnf" model)