scheduling.py

from z3 import *

s = Optimize()

task_length = {
        1: 20,
        2: 50,
        3: 80,
        4: 50,
        5: 60,
        6: 45,
        7: 20,
        8: 25,
        9: 50,
        10: 30,
        11: 40,
        12: 50
}
tx = {k: Int("t{}".format(k)) for k in task_length.keys()}
s.add(And([t >= 0 for t in tx.values()]))

tend = Int("tend")

for i in [1, 2, 3]:
    s.add(tx[i] + task_length[i] <= tx[i+1])
s.add(tx[4] + task_length[4] <= tend)

for i in [5, 6, 7]:
    s.add(tx[i] + task_length[i] <= tx[i+1])
s.add(tx[8] + task_length[8] <= tend)

for i in [9, 10, 11]:
    s.add(tx[i] + task_length[i] <= tx[i+1])
s.add(tx[12] + task_length[12] <= tend)

def add_related_constraint(s, a, b):
    bo = Bool("b{},{}".format(a, b))
    s.add(
        If(bo, tx[a] + task_length[a] <= tx[b], tx[b] + task_length[b] <= tx[a]))

add_related_constraint(s, 1, 5)
add_related_constraint(s, 5, 11)
add_related_constraint(s, 1, 11)

add_related_constraint(s, 2, 7)
add_related_constraint(s, 7, 9)
add_related_constraint(s, 2, 9)

add_related_constraint(s, 3, 8)
add_related_constraint(s, 8, 10)
add_related_constraint(s, 3, 10)

add_related_constraint(s, 4, 6)
add_related_constraint(s, 6, 12)
add_related_constraint(s, 4, 12)

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

for i in sorted(task_length.keys()):
    print tx[i], m[tx[i]]

print tend, m[tend]