stau.space
My omnium-gatherom of scripts and source code.
1#!/usr/bin/env python3
2
3from z3 import *
4import math
5
6N = int(sys.argv[1])
7INT_SIZE = math.ceil(math.log(4*N)) + 1
8
9S = Solver()
10
11Y = [BitVec(f"Y{i + 1}", INT_SIZE) for i in range(N)]
12
13S.add(And(*(And(1 <= y, y <= N) for y in Y)))
14
15S.add(Distinct(*Y))
16
17for k in range(1, N):
18 for i in range(0, N - k):
19 for j in range(0, N - k):
20 if i != j:
21 S.add(Y[i + k] - Y[i] != Y[j + k] - Y[j])
22
23def all_smt(s, initial_terms):
24 def block_term(s, m, t):
25 s.add(t != m.eval(t, model_completion=True))
26 def fix_term(s, m, t):
27 s.add(t == m.eval(t, model_completion=True))
28 def all_smt_rec(terms):
29 if sat == s.check():
30 m = s.model()
31 yield m
32 for i in range(len(terms)):
33 s.push()
34 block_term(s, m, terms[i])
35 for j in range(i):
36 fix_term(s, m, terms[j])
37 yield from all_smt_rec(terms[i:])
38 s.pop()
39 yield from all_smt_rec(list(initial_terms))
40
41count = 0
42for m in all_smt(S, Y):
43 count += 1
44
45print(f"count: {count}")