This assumes the SAT/UNSAT domain of each variable is continuous.
Use an SMT solver to check for a solution to the formula. If there's no solution then that means no upper/lower bounds, so stop.
For each variable in the formula, conduct two binary searches over the domain of the variable, one searching for the lower bound, the other for the upper bound. The starting value in the search for each variable is the value for the variable in the solution found in step 1. Use the SMT solver to probe each search value for satisfiability and methodically bracket the bounds for each variable.
Pseudo code for the search functions, assuming integer domain variables:
lower_bound(variable, start, formula)
{
lo = -inf;
hi = start;
last_sat = start;
incr = 1;
do {
variable = (lo + hi) / 2;
if (SMT(formula) == UNSAT) {
lo = variable + incr;
} else {
last_sat = variable;
hi = variable - incr;
}
} while (lo <= hi);
return last_sat;
}
and
upper_bound(variable, start, formula)
{
lo = start;
hi = +inf;
last_sat = start;
do {
variable = (lo + hi) / 2;
if (SMT(formula) == SAT) {
last_sat = variable;
lo = variable + incr;
} else {
hi = variable - incr;
}
} while (lo <= hi);
return last_sat;
}
-inf/+inf are the smallest/largest values representable in the domain of each variable. If lower_bound returns -inf then the variable has no lower bound. If upper_bound returns +inf then the variable has no upper bound.
In practice most of such optimization problems require some sort of iterate-until-maximum/minimum kind of external driver on top of the SMT solver. Quantified approaches are also possible that can leverage the particular capabilities of the SMT solvers, but in practice such constraints end up being too hard for the underlying solver. See this discussion in particular: How to optimize a piece of code in Z3? (PI_NON_NESTED_ARITH_WEIGHT related)
Having said that, most high-level language bindings include the necessary machinery to simplify your life. For instance, if you use the Haskell SBV library to script z3, you can have:
The first result states x=3, y=1 maximizes x with respect to the predicate x==3 && y>=1. The second result says there is no value that maximizes y with respect to the same predicate. Third call says x=3,y=1 minimizes the predicate with respect to x. Fourth call says x=3,y=1 minimizes the predicate with respect to y. (See http://hackage.haskell.org/packages/archive/sbv/0.9.24/doc/html/Data-SBV.html#g:34 for details.)
You can also use the option "Iterative" (instead of Quantified) to have the library do the optimization iteratively instead of using quantifiers. These two techniques are not equivalent as the latter can get stuck in a local minima/maxima, but iterative approaches might solve problems where the quantified version is way too much to handle for the SMT solver.
发布评论
评论（2）
这假设每个变量的 SAT/UNSAT 域是连续的。
搜索函数的伪代码，假设整数域变量：
和
-inf/+inf 是每个变量的域中可表示的最小/最大值。如果 lower_bound 返回 -inf 则该变量没有下限。如果 upper_bound 返回 +inf 则该变量没有上限。
This assumes the SAT/UNSAT domain of each variable is continuous.
Pseudo code for the search functions, assuming integer domain variables:
and
-inf/+inf are the smallest/largest values representable in the domain of each variable. If lower_bound returns -inf then the variable has no lower bound. If upper_bound returns +inf then the variable has no upper bound.
实际上，大多数此类优化问题都需要在 SMT 求解器之上进行某种迭代直至最大/最小类型的外部驱动程序。量化方法也是可能的，可以利用 SMT 求解器的特定功能，但实际上，此类约束对于底层求解器来说太难了。特别请参阅此讨论：如何优化Z3中的一段代码？ （PI_NON_NESTED_ARITH_WEIGHT 相关）
话虽如此，大多数高级语言绑定都包含简化生活所需的机制。例如，如果您使用 Haskell SBV 库编写 z3 脚本，您可以得到：
第一个结果表明 x=3, y=1 相对于谓词 x==3 && 最大化 x y＞＝1。
第二个结果表明，对于相同的谓词，不存在使 y 最大化的值。
第三次调用表示 x=3,y=1 最小化关于 x 的谓词。
第四次调用表示 x=3,y=1 最小化关于 y 的谓词。
（参见http： //hackage.haskell.org/packages/archive/sbv/0.9.24/doc/html/Data-SBV.html#g:34 了解详细信息。）
您还可以使用选项“迭代”（而不是量化）使库迭代地进行优化而不是使用量词。这两种技术并不等同，因为后者可能会陷入局部最小值/最大值，但迭代方法可能会解决量化版本对于 SMT 求解器来说太大而无法处理的问题。
In practice most of such optimization problems require some sort of iterate-until-maximum/minimum kind of external driver on top of the SMT solver. Quantified approaches are also possible that can leverage the particular capabilities of the SMT solvers, but in practice such constraints end up being too hard for the underlying solver. See this discussion in particular: How to optimize a piece of code in Z3? (PI_NON_NESTED_ARITH_WEIGHT related)
Having said that, most high-level language bindings include the necessary machinery to simplify your life. For instance, if you use the Haskell SBV library to script z3, you can have:
The first result states x=3, y=1 maximizes x with respect to the predicate x==3 && y>=1.
The second result says there is no value that maximizes y with respect to the same predicate.
Third call says x=3,y=1 minimizes the predicate with respect to x.
Fourth call says x=3,y=1 minimizes the predicate with respect to y.
(See http://hackage.haskell.org/packages/archive/sbv/0.9.24/doc/html/Data-SBV.html#g:34 for details.)
You can also use the option "Iterative" (instead of Quantified) to have the library do the optimization iteratively instead of using quantifiers. These two techniques are not equivalent as the latter can get stuck in a local minima/maxima, but iterative approaches might solve problems where the quantified version is way too much to handle for the SMT solver.