Magic/Latin square of Knut Vik design: getting it using Z3

Magic/Latin square is a square filled with numbers/letters, which are all distinct in each row and column. Sudoku is 9*9 magic square with additional constraints (for each 3*3 subsquare).

"Knut Vik design" is a square, where all (broken) diagonals has distinct numbers.

This is diagonal of 5*5 square:

. . . . *
. . . * .
. . * . .
. * . . .
* . . . .


These are broken diagonals:

. . * . .
. . . * .
. . . . *
* . . . .
. * . . .

* . . . .
. . . . *
. . . * .
. . * . .
. * . . .


I could only find 5*5 and 7*7 squares using Z3, couldn't find 11*11 square, however, it's possible to prove there are no 6*6 and 4*4 squares (such squares doesn't exist if size is divisible by 2 or 3).

from z3 import *

#SIZE=4 # unsat
#SIZE=5 # OK
#SIZE=6 # unsat
SIZE=7 # OK

a=[[Int('%d_%d' % (r,c)) for c in range(SIZE)] for r in range(SIZE)]

s=Solver()

# all numbers must be in 1..SIZE limits
for r in range(SIZE):
for c in range(SIZE):

# all numbers in all rows must be distinct:
for r in range(SIZE):
# expression like s.add(Distinct(a[r][0], a[r][1], ..., a[r][last])) is formed here:

# ... in all columns as well:
for c in range(SIZE):

# all (broken) diagonals must also be distinct:
for r in range(SIZE):
s.add(Distinct(*[a[(r+r2) % SIZE][r2 % SIZE] for r2 in range(SIZE)]))
# this line of code is the same as previous, but the column is "flipped" horizontally (SIZE-1-column):
s.add(Distinct(*[a[(r+r2) % SIZE][SIZE-1-(r2 % SIZE)] for r2 in range(SIZE)]))

print s.check()
m=s.model()

for r in range(SIZE):
for c in range(SIZE):
print m[a[r][c]].as_long(),
print ""



5*5 Knut Vik square:

3 4 5 1 2
5 1 2 3 4
2 3 4 5 1
4 5 1 2 3
1 2 3 4 5


7*7:

4 7 6 5 1 2 3
6 5 1 2 3 4 7
1 2 3 4 7 6 5
3 4 7 6 5 1 2
7 6 5 1 2 3 4
5 1 2 3 4 7 6
2 3 4 7 6 5 1


This is NP-problem: you can check this result visually, but it takes several seconds for computer to find it.

We can also use different encoding: each number can be represented by one bit. 0b0001 for 1, 0b0010 for 2, 0b1000 for 4, etc. Then a "Distinct" operator can be replaced by OR operation and comparison against mask with all bits present.

import math, operator
from z3 import *

#SIZE=4 # unsat
SIZE=5 # OK
#SIZE=6 # unsat
#SIZE=7 # OK

a=[[BitVec('%d_%d' % (r,c), SIZE) for c in range(SIZE)] for r in range(SIZE)]

# 0b11111 for SIZE=5:

s=Solver()

# all numbers must have form 2^n, like 1, 2, 4, 8, 16, etc.
# we add contraint like Or(a[r][c]==2, a[r][c]==4, ..., a[r][c]==32, ...)
for r in range(SIZE):
for c in range(SIZE):

# all numbers in all rows must be distinct:
for r in range(SIZE):
# expression like s,add(a[r][0] | a[r][1] | ... | a[r][last] == mask) is formed here:

# ... in all columns as well:
for c in range(SIZE):
# expression like s,add(a[0][c] | a[1][c] | ... | a[last][c] == mask) is formed here:

# for all (broken) diagonals:
for r in range(SIZE):
# this line of code is the same as previous, but the column is "flipped" horizontally (SIZE-1-column):

print s.check()
m=s.model()

for r in range(SIZE):
for c in range(SIZE):
print int(math.log(m[a[r][c]].as_long(),2)),
print ""



That works twice as faster (however, numbers are in 0..SIZE-1 range instead of 1..SIZE, but you've got the idea).

Besides recreational mathematics, squares like these are very important in design of experiments.