z3py：如何在 z3 中实现计数器？答案

【问题标题】：z3py: How to implement a counter in z3?z3py：如何在 z3 中实现计数器？
【发布时间】：2015-08-03 17:00:54
【问题描述】：

我想设计类似于 Z3py 中的计数器的逻辑。

如果编写python脚本，我们通常定义一个变量“counter”，然后在必要时不断增加它。但是，在 Z3 中，没有变体。因此，我没有定义变体，而是定义了该变体的踪迹。

这是一个示例代码。假设有一个大小为 5 的数组“myArray”，数组中的元素是 1 或 2。我想断言“myArray”中必须有两个 '2'

from z3 import *

s = Solver()
myArray = IntVector('myArray',5)
for i in range(5):
    s.add(Or(myArray[i]==1,myArray[i]==2))
counterTrace = IntVector('counterTrace',6)
s.add(counterTrace[0]==0)
for i in range(5):
    s.add(If(myArray[i]==2,counterTrace[i+1]==counterTrace[i]+1,counterTrace[i+1]==counterTrace[i]))
s.add(counterTrace[5]==2)
print s.check()
print s.model()

我的问题是，这是在 Z3 中实现计数器概念的有效方式吗？在我更复杂的实际问题中，这确实是低效的。

【问题讨论】：

标签： counter z3 smt z3py

【解决方案1】：

您可以这样做，但在myArray[i] == 2 ? 1 : 0 上创建总和要容易得多。这样你就不需要断言任何东西并且你正在处理正常的表达式。

【讨论】：

你说得对，但我更担心的是效率，或者说是检查时间短。我的实现的复杂度是 O(n)，其中 n 是数组的长度。在我真正的问题中，我循环遍历数组两次，复杂度变为 O(n^2)，这确实是低效的。
所以真正的问题是二次复杂度对吗？那么这与计数无关。从这个角度来看，这个问题似乎与您的问题无关？！ @Z.Jin
我想我应该改写我的问题：除了在 z3 中对其跟踪设置约束之外，是否还有另一种方法可以为变体设置约束？跟踪的想法很有效，但对我来说似乎效率低下，因为它增加了更多的变量和约束。
Z3 中的一切都是不可变的。我不清楚为什么跟踪的想法对你来说似乎是错误的。它添加了线性数量的变量。每个变量的大小必须是 ceil(log2(n)) 位，因此您可以争辩说所需的工作量是 n*log(n)，是的。在文献中，有一种想法是使用计数网络来有效地编码约束，例如“某物的计数必须在 x 和 y 之间”。这确实有助于求解器的性能。 Z3以战术的形式对其进行了一些支持。我对此不熟悉。