时间戳

首页 > 解决方案 > 变量的初始值

z3 - 变量的初始值

问题描述

我想以一种有效的方式为 z3py 中的变量设置初始值。

x,y = Ints(x,y)
s = Solver()
s.add(x>10)
s.check()
s.model()

我希望输出值是例如 x = 11，y = 0，而不是结果 x = 11，y = 7。

一种方法是：

x,y = Ints(x,y)
s = Optimize()
s.add_soft(x==0)
s.add_soft(y==0)
s.add(x>10)
s.check()
s.model()

但是由于我的程序包含许多变量，因此需要很多计算时间。有什么更好的方法吗？

标签： z3z3py

解决方案

减速是因为您正在强制优化器运行，这对于此目的来说是一种过度杀伤力。（优化求解器可以处理 max-sat 问题，在这里可以完成这项工作，但成本很高，并且在这种情况下不需要。）

相反，只需遍历模型并查看是否有分配：

from z3 import *

def model_with_zeros(s, vs):
    m = s.model()

    result = []
    for v in vs:
        val = m.eval(v)
        if val.eq(v):
            result.append((v, 0))
        else:
            result.append((v, val))

    return result


x, y = Ints('x y')
s = Solver()
s.add(x > 10)

print s.check()
print model_with_zeros(s, [x, y])

这打印：

sat
[(x, 11), (y, 0)]

请注意，您必须将求解器和您感兴趣的变量显式传递给model_with_zeros函数；因为这里的技巧正是要查看求解器未触及哪些变量。

如果您想要不同的初始值，则可以修改model_with_zeros以分别为每个变量考虑该值。

推荐阅读