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.

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
], m
], m
]))
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
], m
]))
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.

Refer to alias answer for the best solution!

I solved the problem in an inefficient way using a hamiltonian circuit. I generated all the nodes and the link between nodes possible with the constraint:

all_pairs = [(i,j) for i in range(4) for j in range(4)]
adj_list = {
    all_pairs.index((i,j)): [all_pairs.index((x, y)) for x in range(4) for y in range(4) if (x!=i and y!=j)]
    for i in range(4) for j in range(4)
}
print(adj_list)

Then I used the already existing example of a z3 Hamiltonian path to solve it:

def gencon(gr):
    """
    Input a graph as an adjacency list, e.g. {0:[1,2], 1:[2], 2:[1,0]}.
    Produces solver to check if the given graph has
    a Hamiltonian cycle. Query the solver using s.check() and if sat,
    then s.model() spells out the cycle. Two example graphs from
    http://en.wikipedia.org/wiki/Hamiltonian_path are tested.

    =======================================================

    Explanation:

    Generate a list of Int vars. Constrain the first Int var ("Node 0") to be 0.
    Pick a node i, and attempt to number all nodes reachable from i to have a
    number one higher (mod L) than assigned to node i (use an Or constraint).

    =======================================================
    """
    L = len(gr)
    cv = [Int('cv%s'%i) for i in range(L)]
    s = Solver()
    s.add(cv[0]==0)
    for i in range(L):
        s.add(Or([cv[j]==(cv[i]+1)%L for j in gr[i]]))
    return s

grdodec = {0: [5, 6, 7, 9, 10, 11, 13, 14, 15], # (o0,s0)
 1: [4, 6, 7, 8, 10, 11, 12, 14, 15],# (o0,s1)
 2: [4, 5, 7, 8, 9, 11, 12, 13, 15],# (o0,s2)
 3: [4, 5, 6, 8, 9, 10, 12, 13, 14],# (o0,s3)
 4: [1, 2, 3, 9, 10, 11, 13, 14, 15],# (o1,s0)
 5: [0, 2, 3, 8, 10, 11, 12, 14, 15],# (o1,s1)
 6: [0, 1, 3, 8, 9, 11, 12, 13, 15],# (o1,s2)
 7: [0, 1, 2, 8, 9, 10, 12, 13, 14],# (o1,s3)
 8: [1, 2, 3, 5, 6, 7, 13, 14, 15],# (o2,s0)
 9: [0, 2, 3, 4, 6, 7, 12, 14, 15],# (o2,s1)
 10: [0, 1, 3, 4, 5, 7, 12, 13, 15],# (o2,s2)
 11: [0, 1, 2, 4, 5, 6, 12, 13, 14],# (o2,s3)
 12: [1, 2, 3, 5, 6, 7, 9, 10, 11],# (o3,s0)
 13: [0, 2, 3, 4, 6, 7, 8, 10, 11],# (o3,s1)
 14: [0, 1, 3, 4, 5, 7, 8, 9, 11],# (o3,s2)
 15: [0, 1, 2, 4, 5, 6, 8, 9, 10]# (o3,s3)
 }

import pprint
pp = pprint.PrettyPrinter(indent=4)
pp.pprint(grdodec)

sdodec=gencon(grdodec)
print(sdodec.check())

The thing is that it is incredibly slow, and it outputs only one solution. It is inefficient since multiple runs will explore the same paths and possibly give the same solution.

I was in a rush to have the result, so I ran different processes and waited for the number of permutations I needed.