整数变量的最小值和最大值 [英] Minimum and maximum values of integer variable

问题描述

让我们假设一个非常简单的约束:solve(x > 0 && x <5).

Let's assume a very simple constraint: solve(x > 0 && x < 5).

Can Z3(或任何其他 SMT 求解器，或任何其他自动技术)计算满足给定约束的(整数)变量 x 的最小值和最大值?

Can Z3 (or any other SMT solver, or any other automatic technique) compute the minimum and maximum values of (integer) variable x that satisfies the given constraints?

在我们的例子中，最小值为 1，最大值为 4.

In our case, the minimum is 1 and the maximum is 4.

推荐答案

正如 Leonardo 指出的，这在之前已经详细讨论过:确定任意命题公式中变量的上/下界.另见:如何优化Z3中的一段代码?(PI_NON_NESTED_ARITH_WEIGHT 相关).

As Leonardo pointed out, this was discussed in detail before: Determine upper/lower bound for variables in an arbitrary propositional formula. Also see: How to optimize a piece of code in Z3? (PI_NON_NESTED_ARITH_WEIGHT related).

总而言之，可以使用量化的公式，也可以反复进行.不幸的是，这些技术不等效:

To summarize, one can either use a quantified formula, or go iteratively. Unfortunately, these techniques are not equivalent:

• 量化方法不需要迭代，并且可以在对求解器的单次调用中找到全局最小值/最大值；至少在理论上.然而，它确实会产生更难的公式.因此，后端求解器可以超时，或者简单地返回未知".

• Quantified approach needs no iteration, and can find global min/max in a single call to the solver; at least in theory. However, it does give rise to harder formulas. So, the backend solver can time-out, or simply return "unknown".

迭代方法为后端求解器创建了简单的公式来处理，但如果没有最优值，它可以永远循环；最简单的例子是试图找到最大的 Int 值.量化版本可以很好地解决这个问题，通过快速告诉你没有这样的价值，而迭代版本会无限期地继续下去.如果您事先不知道您的约束确实有最佳解决方案，这可能是一个问题.(不用说，足够"的迭代次数通常很难猜测，并且可能取决于随机因素，例如求解器使用的种子.)

Iterative approach creates simple formulas for the backend solver to deal with, but it can loop forever if there's no optimal value; simplest example being trying to find the largest Int value. Quantified version can solve this problem nicely by quickly telling you that there is no such value, while the iterative version would go on indefinitely. This can be a problem if you don't know ahead of time that your constraints do have an optimal solution. (Needless to say, the "sufficient" iteration count is typically hard to guess, and might depend on random factors, like the seed used by the solver.)

还请记住，如果手头有针对问题域的自定义优化算法，则通用 SMT 求解器不太可能胜过它.

Also keep in mind that if there is a custom optimization algorithm for the problem domain at hand, it's unlikely that a general purpose SMT solver can outperform it.

这篇关于整数变量的最小值和最大值的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！