给定一个任意命题公式 PHI(某些变量的线性约束),确定每个变量的(近似)上限和下限的最佳方法是什么?
有些变量可能是无界的。在这种情况下,算法应该得出结论:这些变量没有上限/下限。
例如,PHI = (x=3 AND y>=1)。 x 的上限和下限均为 3。y 的下限为 1,并且 y 没有上限。
这是一个非常简单的例子,但是有通用的解决方案吗(也许使用 SMT 求解器)?
这假设每个变量的 SAT/UNSAT 域是连续的。
- 使用 SMT 求解器检查公式的解。如果没有解决方案,则意味着没有上限/下限,因此停止。
- 对于公式中的每个变量,在变量的域上进行两次二分搜索,一次搜索下界,另一个搜索上限。每个变量搜索的起始值是步骤 1 中找到的解决方案中的变量值。使用 SMT 求解器探测每个搜索值的可满足性,并有条理地对每个变量的边界进行括号。
搜索函数的伪代码,假设整数域变量:
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 是每个变量的域中可表示的最小/最大值。如果 lower_bound 返回 -inf 则该变量没有下限。如果 upper_bound 返回 +inf 则该变量没有上限。
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)