Use Z3 constraint solver to create list of objects

I want to use z3 to create all the possible permutations of elements composed by 3 objects. I have the following objects categories:

# Objects o
o1, o2, o3, o4 = Ints('o1 o2 o3 o4')
# Objects w
w1, w2, w3, w4, w5 = Ints('w1 w2 w3 w4 w5')
# Objects s
s1, s2, s3, s4 = Ints('s1 s2 s3 s4')

I want to create all the possible list of permutations, like [(o1,w1,s1),(o2,w3,s4)...] with this constraints:

An element with the same object o cannot be repeated twice in a row. I don't want [...(o1,w1,s1),(o1,w3,s2)...]
An element with the same object s cannot be repeated twice in a row. I don't want [...(o2,w1,s1),(o1,w3,s1)...]
No element shopuld be repeated. There should be only one (o1,w1,s1) in the list.

I cannot find a way to create constraint based on the position of element in a list.

Sorry, it may seem a simple problem, but I am really a novice at z3 and I cannot find a similar example online.

Solution

The easiest way to address this problem would be to generate all permutations symbolically, and then assert your no-consecutive-repeats constraints on subsequent elements. Below, I'll use enumerations instead of integers, which is more suitable for this problem:

from z3 import *

# declare domains as enums
O, (o1, o2, o3, o4)     = EnumSort('O', ('o1', 'o2', 'o3', 'o4'))
W, (w1, w2, w3, w4, w5) = EnumSort('W', ('w1', 'w2', 'w3', 'w4', 'w5'))
S, (s1, s2, s3, s4)     = EnumSort('S', ('s1', 's2', 's3', 's4'))

# universe for each type
os = [o1, o2, o3, o4]
ws = [w1, w2, w3, w4, w5]
ss = [s1, s2, s3, s4]

solver = Solver()

# Create all permutations symbolically
perms = []
for i in range(len(os)*len(ws)*len(ss)):
    vo = Const('o' + str(i), O)
    vw = Const('w' + str(i), W)
    vs = Const('s' + str(i), S)
    perms = perms + [(vo, vw, vs)]

# assert the constraint that consecutive elements don't replicate o and s
for p, pn in zip(perms, perms[1:]):
    solver.add(p[0] != pn[0])
    solver.add(p[2] != pn[2])

# assert the constraint that each permutation is unique
for i in range(len(perms)):
    for j in range(len(perms)):
        if i < j:
            pi = perms[i]
            pj = perms[j]
            solver.add(Not(And(pi[0] == pj[0], pi[1] == pj[1], pi[2] == pj[2])))

if solver.check() == sat:
    m = solver.model()
    for p in perms:
        print((m[p[0]], m[p[1]], m[p[2]]))
else:
    print("Not satisfiable")

When run, this produces:

(o4, w2, s4)
(o1, w1, s2)
(o2, w4, s3)
(o4, w1, s4)
(o2, w5, s1)
(o1, w2, s4)
(o4, w5, s2)
(o1, w1, s1)
(o3, w3, s4)
(o2, w3, s3)
(o1, w5, s4)
(o4, w4, s1)
(o3, w5, s4)
(o2, w3, s1)
(o1, w4, s2)
(o2, w1, s4)
(o1, w4, s3)
(o3, w3, s1)
(o4, w3, s2)
(o2, w4, s1)
(o3, w3, s2)
(o4, w3, s3)
(o1, w3, s1)
(o3, w5, s3)
(o4, w2, s1)
(o3, w1, s3)
(o1, w2, s1)
(o3, w4, s4)
(o2, w3, s2)
(o3, w1, s1)
(o4, w1, s3)
(o2, w5, s2)
(o1, w3, s4)
(o3, w5, s1)
(o1, w2, s2)
(o2, w1, s3)
(o4, w1, s2)
(o2, w2, s4)
(o1, w5, s3)
(o4, w4, s2)
(o3, w4, s1)
(o4, w3, s4)
(o2, w5, s3)
(o1, w5, s1)
(o3, w2, s2)
(o4, w5, s1)
(o2, w3, s4)
(o3, w1, s2)
(o2, w5, s4)
(o4, w5, s3)
(o3, w1, s4)
(o1, w1, s3)
(o2, w1, s2)
(o3, w2, s1)
(o1, w3, s3)
(o4, w3, s1)
(o3, w4, s3)
(o1, w3, s2)
(o3, w2, s3)
(o1, w4, s1)
(o4, w5, s4)
(o1, w2, s3)
(o4, w2, s2)
(o2, w2, s1)
(o4, w4, s3)
(o3, w4, s2)
(o4, w2, s3)
(o3, w2, s4)
(o2, w1, s1)
(o1, w4, s4)
(o2, w2, s3)
(o1, w1, s4)
(o3, w5, s2)
(o2, w4, s4)
(o1, w5, s2)
(o3, w3, s3)
(o4, w4, s4)
(o2, w2, s2)
(o4, w1, s1)
(o2, w4, s2)

which satisfies your constraints. Unfortunately, it's relatively slow to run. (On my relatively decent machine, it takes about 4 minutes to complete.) But we can take advantage of the fact that there are no constraints on w values, and make it go faster.

Speeding up

Since there are no constraints on w, we can simply generate the permutations on o and s values, and then sprinkle w's in. The only thing we have to make sure is that the starting (o, s) pair and the ending (o, s) pair is different: Then we can simply repeat the same sequence for as many w's as there are. This leads to:

from z3 import *

# declare domains as enums
O, (o1, o2, o3, o4) = EnumSort('O', ('o1', 'o2', 'o3', 'o4'))
S, (s1, s2, s3, s4) = EnumSort('S', ('s1', 's2', 's3', 's4'))

# universe for each type
os = [o1, o2, o3, o4]
ss = [s1, s2, s3, s4]

solver = Solver()

lperms = len(os) * len(ss)

# Create all permutations symbolically
perms = []
for i in range(lperms):
    vo = Const('o' + str(i), O)
    vs = Const('s' + str(i), S)
    perms = perms + [(vo, vs)]

# assert the constraint that consecutive elements don't replicate o and s
for p, pn in zip(perms, perms[1:]):
    solver.add(p[0] != pn[0])
    solver.add(p[1] != pn[1])

# assert the constraint that each permutation is unique
for i in range(lperms):
    for j in range(lperms):
        if i < j:
            pi = perms[i]
            pj = perms[j]
            solver.add(Not(And(pi[0] == pj[0], pi[1] == pj[1])))

# require the first and last to be completely different:
solver.add(And(perms[0][0] != perms[-1][0], perms[0][1] != perms[-1][1]))

if solver.check() == sat:
    m = solver.model()
    for p in perms:
        print((m[p[0]], m[p[1]]))
else:
    print("Not satisfiable")

Printing:

(o4, s3)
(o3, s4)
(o2, s1)
(o1, s2)
(o2, s3)
(o4, s2)
(o1, s1)
(o4, s4)
(o3, s1)
(o2, s4)
(o3, s3)
(o2, s2)
(o1, s3)
(o4, s1)
(o3, s2)
(o1, s4)

The above takes less than a second to run on my machine. This isn't surprising, as there are much fewer degrees of freedom and much fewer variables to worry about. There are 16 elements in the above sequence, starting with (o4, s3), and ending with (o1, s4): Simply repeat the sequence 5 times, one for each of w1, w2, .., w5, and concatenate. That'll be the solution to your original problem, solved in less than half a second by z3 and a bit of extra programming.