queens_20.tla

---- MODULE queens_20 ----

EXTENDS Naturals, FiniteSets

VARIABLE queens, n, solved
----

Init == /\ queens=[i \in 1..2 |-> 0]
        /\ n=20
        /\ solved = 0

Solve == /\ solved=0
         /\ queens' \in [1..n -> 1..n]
         /\ \A i \in 1..n : (\A j \in 2..n : i<j => queens'[i] # queens'[j] /\ queens'[i]+i-j # queens'[j] /\ queens'[i]-i+j # queens'[j])
         /\ solved'=1
         /\ n'=n
Spec == Init /\ [] [Solve]_<<n,queens>>

VISB_JSON_FILE == "queens_20_tla.json"

=======
\* Generated at Tue Jun 22 21:06:17 CEST 2010
\* TLC takes 2 seconds for n-6, 12 seconds to solve for n=7 
\* and 4 minutes 9 seconds for n=8, 1h45min47sec for n=9
\* ProB takes 0.01 seconds for n=8, both on MacBook Pro 3.06 GHz

\* with TLA Toolbox 1.7.1 on macOS MacBookAir M2 to find first solution 2024-09-05 
\* n=6 Finished in 2245ms 
\* n=7 Finished in 5797ms at (2024-09-05 15:03:50)
\* n=8 Finished in 77235ms with Deadlock checking  (93 distinct states found, 88 states left on queue)