fix: queens

This commit is contained in:
Renge 2024-02-22 13:58:13 -05:00
parent ebb4f02981
commit e7f0e54480
4 changed files with 400011 additions and 50008 deletions

View File

@ -1,4 +1,5 @@
#const n = 8.
#const n = 20.
#const k = 5.
% n-Queens encoding
@ -6,3 +7,4 @@
{ q(1..n,J) } == 1 :- J = 1..n.
:- { q(D-J,J) } >= 2, D = 2..2*n.
:- { q(D+J,J) } >= 2, D = 1-n..n-1.
:- q(X1, Y1), q(X2, Y2), X1 != X2, |X1-X2| + |Y1-Y2| < k.

View File

@ -10,10 +10,10 @@ vocabulary V {
}
structure S : V {
index = {1..4}
diag = {1..7}
n = 4
k = 2
index = {1..20}
diag = {1..39}
n = 20
k = 5
}
theory T : V {
@ -23,8 +23,8 @@ theory T : V {
!y : ?=1x : queen(x, y). //(2)
!d : #{x y : queen(x, y) & diag1(x, y) = d} < 2. //(3)
!d : #{x y : queen(x, y) & diag2(x, y) = d} < 2. //(4)
~? x1 y1 x2 y2: queen(x1, y1) & queen(x2, y2) & ~x1 = x2 & abs(x1-x2) + abs(y1-y2) =< k.
//~? x1 y1 x2 y2: queen(x1, y1) & queen(x2, y2) & abs(x1-y1) = 3.
!x1 y1 x2 y2: queen(x1, y1) & queen(x2, y2) & x1 ~= x2 => abs(x1-x2) + abs(y1-y2) >= k.
//~? x1 y1 x2 y2: queen(x1, y1) & queen(x2, y2) & ~x1 = x2 & abs(x1-x2) + abs(y1-y2) =< k.
}
procedure main() {

View File

@ -1,5 +1,6 @@
import random
for i in range(100000):
j = random.randint(1,10000)
k = random.randint(1,10000)
x = int(input())
for i in range(10 * x):
j = random.randint(1,x)
k = random.randint(1,x)
print("edge(", j, ",", k, ").")

449996
reachin1000

File diff suppressed because it is too large Load Diff