有没有一种方法来操纵Z3的上限？

Question

我试图尽量减少使用Z3值。我设置冗长为0，并且观察到，Z3找到一个上限，并开始从那里工作以最小化的值。例：

(optimize:check-sat)
(optimize:sat)
(optsmt upper bound: 3460)
(optsmt upper bound: 3455)
(optsmt upper bound: 3445)
(optsmt upper bound: 2430)
(optsmt upper bound: 2425)
(optsmt upper bound: 2325)
(optsmt upper bound: 2155)
(optsmt upper bound: 2150)
(optsmt upper bound: 2145)
(optsmt upper bound: 2135)
(optsmt upper bound: 2125)
(optsmt upper bound: 2055)
(optsmt upper bound: 2045)
(optsmt upper bound: 155)
(optsmt upper bound: 135)
(optsmt upper bound: 115)
(optsmt upper bound: 15)
(optsmt upper bound: 10)

我想知道是否有上限设置为低得多的水平，以获得更快的输出的任何方式。

Answer 1

如果你知道有一个绑定的，为什么不把那作为一个额外的断言：

(assert (< goal 200))

这并不能保证加快速度，当然，和一般的，如果你弄错了能错过最佳点。但它是一个简单的事情来尝试。

一般情况下，你提供的求解器的更多信息，更好的机会，它会收敛更快。

需要注意的是Z3优化过程中并没有真正的“搜索”，取而代之的是演算法判断和约束的范围，所以没有真正的‘开始’值。有关优化Z3是如何工作的更多参考资料，见这个优秀的最近答案帕特里克：What is the theory behind Z3 Optimize maximum and minimum functionality?