尝试用 Z3 证明二分查找终止，但 Z3 发现了无效的计数器示例

Question

我正在尝试学习和实验 z3 试图证明二分搜索。第一步是询问函数是否终止。这应该可以通过证明尺寸函数 (r - l) 总是递减来实现。这是我的代码

from z3 import *


# prove that binary search always terminates
# this can be proven by the fact that r - l
# is always decreasing regardless of the
# executed branch in the loop

l, r = Ints("l r")

preconditions = And([
    l >= 0,
    r > l, # assume the range is not empty
])

mid = Int("mid")
termination = And([
    mid == (l + r) / 2,
    (r - l) > (mid - l),
    (r - l) > (r - mid + 1),
])

claim = Implies(preconditions, termination)

prove(claim)

请注意，我假设搜索范围包含左侧且不包含右侧

但是当我执行代码 z3 时报告发现了一个反例

counterexample
[l = 0, mid = 1, r = 1]

这对我来说没有意义，因为终止中的第一个条件指出

mid == (l + r) / 2

。

我尝试在两种条件下内联中频，但仍然得到相同的结果

termination = And([
    (r - l) > ((l + r) / 2 - l),
    (r - l) > (r - (l + r) / 2 + 1),
])

counterexample
[l = 0, r = 1]

我通过在解释器中执行以下代码来检查 z3 不会将除法转换为 Real

>>> from z3 import *
>>> x, y = Ints("x y")
>>> ((x + y) / 2).sort()
Int

我还尝试使用找到的计数器示例 z3 创建一个约束，并检查它是否与我对 mid 的定义兼容，但是，z3 报告说，对于下面的内容，没有找到解决方案

solve(mid == 1, mid == (l + r) / 2, l == 0, r == 1)

我很困惑为什么 z3 认为它找到的反例是有效的？

期望z3证明我的说法是正确的

Answer 1

给你的z3型号就很好了。反例是：

[l = 0, mid = 1, r = 1]

让我们看看它是否满足您的前提条件：

preconditions = And([
    l >= 0,
    r > l, # assume the range is not empty
])

l >= 0

为真，因为

0 >= 0

，并且

r > l

为真，因为

1 > 0

。

既然你有暗示，如果这个模型不满足你的“终止”，那么反例就是合理的。让我们看看：

termination = And([
    mid == (l + r) / 2,
    (r - l) > (mid - l),
    (r - l) > (r - mid + 1),
])

mid == (l+r) / 2

失败，因为

1 != (0 + 1) / 2

。 （根据 SMTLib 除法语义，右侧是

0

。）我们不必查看其余的合取词。因此，使用此模型，您的“先决条件”并不意味着“终止”。这就是为什么你会得到一个反例。

如何修复

为了让事情变得具体，我们首先看看算法实际上是什么样子的。您还没有给我们您正在建模的“代码”，但我认为它看起来像：

int l = 0, r = (int)vec.size();
while(l != r) {
    int mid = (l + r) / 2;
    if (vec[mid] < val) l = mid + 1;
    else r = mid;
}

实际细节、语言、使用的数据类型等并不重要。重要的是控制流程。当

l == r

时循环终止。因此，我们应该证明在任何控制路径中，

l

和

r

之间的距离都会减小。换句话说，度量

r - l

始终为非负数，并且在每次迭代中都会下降。那么让我们编写代码：

from z3 import *


l, r = Ints("l r")

preconditions = And([l >= 0, r > l])

mid = (l+r) / 2

# Starting metric
startingMetric = r - l

# if vec[mid] < val, then l = mid + 1
metric1 = r - (mid + 1)

# if vec[mid] >= val, then r = mid
metric2 = mid - l

termination = And(
     And(metric1 >= 0, metric1 < startingMetric)
   , And(metric2 >= 0, metric2 < startingMetric)
   )

claim = Implies(preconditions, termination)

prove(claim)

如果你运行这个，你会得到

proved

。

这证实了这样一个事实：从

l >= 0 && r > l

开始，无论您采用哪条控制路径，度量

r - l

都会减少，但仍为非负值；从而确保终止。

旁白

我应该补充一点，二分搜索中的一个“理论”错误是，当使用机器整数时，值

mid = (l+r) / 2

并不总是计算中点。具体来说，如果

l

和

r

是由 z3 的

Int

类型建模的数学整数，那么一切都很好。但如果它们是 32 位或 64 位机器整数，则

l+r

可能会溢出，并且中点的计算将不正确。这在实践中通常不是什么大问题，因为当输入向量非常大时就会发生这种情况；无论如何，可能不适合你的记忆。但为了绝对安全，您应该以安全的方式计算中点。您可以在这里阅读有关此问题的更多信息：https://blog.research.google/2006/06/extra-extra-read-all-about-it-nearly.html