在 z3 中约束一个连续的 True 数组答案

【问题标题】：Constrain a consecutive True array in z3在 z3 中约束一个连续的 True 数组
【发布时间】：2020-07-07 15:07:35
【问题描述】：

先发制人：几天来我一直在尝试寻找不同的解决方案，但无济于事，寻找任何有用的东西。

问题：

我目前正在尝试为Minimum Shift Design 问题寻找解决方案，通过该解决方案我们尝试优化在一段时间内满足人员配备要求所需的工作人员和员工数量。

接近

我们有：

shift_needs = s_i 代表每小时的人员需求i=0..11 以及
max_employees 最大员工人数
e_i_j，其中i 是员工编号，j 是小时。 True 表示员工 i 正在工作时间 j

所以它本质上是一个简单的 ILP，解决它是微不足道的，但我遇到的问题是限制轮班。即，我们需要有连续的True，中间没有False。

没关系： [True, True, True, True, False, False, False, False, False, False, False, False]

这不行： [True, True, False, True, False, False, True, True, False, False, False, False]

我尝试添加一个约束：

如果e_i_j == True 那么我们不能有And(e_i_j+1 == False, e_i_j-1 == False)
如果e_i_j == False那么我们不能有And(e_i_j+1 == True, e_i_j-1 == True)

但我仍然得到集群。

实现目标的最佳方法是什么？提前致谢。

【问题讨论】：

如果您实际发布了一个您尝试过但效果不佳的代码示例，则 Stack-overflow 效果最好。见stackoverflow.com/help/minimal-reproducible-example

标签： z3 linear-programming

【解决方案1】：

可能有许多不同的方法来解决这个问题，但以下想法最简单：计算从假到真或真到假的切换次数。如果第一个元素是 True，那么我们最多允许一次切换。如果第一个元素是 False，那么我们最多允许两个开关。您可以根据需要调整计数。

我在 z3py 中编写以下代码，但在任何高级绑定中都可以或多或少地类似地编写代码。直接在 SMTLib 中编码这类事情比较困难，但可以对任何有限序列进行。

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])

当我运行它时，我得到：

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

这给了我们一个连续的转变。希望这能让你开始！

【讨论】：

这看起来非常有前途！我现在正在尝试实施它，如果它有效，会告诉你。非常感谢！
其实，contiguousShift函数用在什么地方？
好的，这很棒。否则，您可以简单地使用 Or(And(xs[0], contiguousShift(bs)
使用contiguousShift，您不需要任何其他限定符。（假设列表不为空，您编写的内容将起作用，但相当于对 contiguousShift 的简单调用。）

【解决方案2】：

我通常在 MIP 模型中对此进行建模，如下所示。

让x[t] 成为二进制变量（即 0 或 1）。引入另一个变量start[t]，它指示 x 何时从 0 翻转到 1。即：

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

为了达到你想要的，你想将开始的次数限制为 1。或者就不等式而言：

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

x[0] 可以看作是初始状态。

我相信这可以很容易地翻译成 Z3。

【讨论】：