z3 - 确定任意命题公式中变量的上限/下限

Question

关闭。这个问题不满足Stack Overflow guidelines .它目前不接受答案。












想改善这个问题吗？更新问题，使其成为 on-topic对于堆栈溢出。

7年前关闭。




Improve this question




给定一个任意命题公式 PHI(对某些变量的线性约束)，确定每个变量的(近似)上限和下限的最佳方法是什么？

一些变量可能是无界的。在这种情况下，算法应该得出结论，这些变量没有上限/下限。

例如，PHI = (x=3 AND y>=1)。 x 的上限和下限都是 3。y 的下限是 1，而 y 没有上限。

这是一个非常简单的例子，但是否有一般的解决方案(也许使用 SMT 求解器)？

Answer 1

这假设每个变量的 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;
}

和

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 则变量没有上限。