Constrain a consecutive True array in z3

Question

Preemptively: I've been trying to find different solutions to this for a few days to no avail, looking for anything useful.

Problem:

I am currently trying to find a solution for the Minimum Shift Design problem whereby we try to optimize the number of shits and employees needed to satisfy staffing requirements over a period of time.

Approach

We have:

• shift_needs = s_i which represents the staffing needs for each hour i=0..11 as well as the
• max_employees the maximum number of employees
• e_i_j, where i is the employee number and j the hour. True means employee i is working at hour j

So it's essentially a simple ILP and solving it is trivial BUT the issue I am having is to constrain the shifts. I.e., we need to have consecutive True without False in-between.

This is OK: [True, True, True, True, False, False, False, False, False, False, False, False]

This is no OKt: [True, True, False, True, False, False, True, True, False, False, False, False]

I tried to add a constraint whereby:

• if e_i_j == True then we can't have And(e_i_j+1 == False, e_i_j-1 == False)
• if e_i_j == Falsethen we can't have And(e_i_j+1 == True, e_i_j-1 == True)

But then I still get clusters.

What would be the best approach to achieve the goal? Thanks in advance.

Answer 1

There could be many different ways to solve this problem, but the following idea the easiest: Count the number of switches from false to true or true to false. If the first element is True, then we allow at most one switch. If the first element is False, then we allow at most two switches. You can tweak the counting based on your needs.

I'm coding the below in z3py, but this can be coded more or less similarly in any high-level binding. Coding this sort of thing directly in SMTLib is harder, but can be done for any finite sequence.

from z3 import *

# Count the number of times the value changes in a list
def countSwitches(xs):
    return Sum([If(a != b, 1, 0) for (a, b) in zip(xs, xs[1:])])

# If we start at True, we want switches to be at most 1. Otherwise at most 2.
def contiguousShift(xs):
    if not xs:
        return Bool(True)
    return countSwitches(xs) < If(xs[0], 1, 2)

# Test
bs = [Bool('b' + str(i)) for i in range(10)]
s = Solver()
s.add(contiguousShift(bs))
r = s.check()
if r == sat:
    m = s.model()
    print([m.eval(b) for b in bs])

When I run this, I get:

[False, False, False, True, True, True, True, True, True, True]

Which gives us a contiguous shift. Hope this gets you started!

Answer 2

I typically model this in MIP models as follows.

Let x[t] a binary variable (i.e. 0 or 1). Introduce another variable start[t] that indicates when x flips from 0 to 1. I.e.:

 x     = [ 0 0 1 1 1 0 0 1 1 ]
 start = [ 0 0 1 0 0 0 0 1 0 ]

To achieve what you want, you want to limit the number of starts to 1. Or in terms of inequalities:

 start[t] ≥ x[t] - x[t-1]     ∀t 
 sum(t, start[t]) ≤ 1
 x[t], start[t] ∈ {0,1}

x[0] can be seen as the initial state.

I am sure that this can be easily translated into Z3.