5

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

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

例如，PHI = (x=3 AND y>=1)。x 的上限和下限均为 3。y 的下限为 1，并且 y 没有上限。

这是一个非常简单的例子，但有没有一般的解决方案（可能使用 SMT 求解器）？

4

2 回答 2

3

这假设每个变量的 SAT/UNSAT 域是连续的。

  1. 使用 SMT 求解器检查公式的解。如果没有解决方案，那么这意味着没有上限/下限，所以停止。
  2. 对于公式中的每个变量，在变量的域上进行两次二进制搜索，一次搜索下限，另一次搜索上限。搜索每个变量的起始值是在步骤 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 则变量没有上限。

于 2012-01-26T02:24:00.953 回答
2

在实践中，大多数此类优化问题都需要在 SMT 求解器之上使用某种迭代直到最大/最小类型的外部驱动程序。量化方法也可以利用 SMT 求解器的特定功能，但在实践中，这样的约束最终对于底层求解器来说太难了。请特别查看此讨论：如何在 Z3 中优化一段代码？（PI_NON_NESTED_ARITH_WEIGHT 相关）

话虽如此，大多数高级语言绑定都包含简化生活的必要机制。例如，如果您使用 Haskell SBV 库编写 z3 脚本，您可以：

Prelude> import Data.SBV
Prelude Data.SBV> maximize Quantified head 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1]
Prelude Data.SBV> maximize Quantified (head . tail) 2 (\[x, y] -> x.==3 &&& y.>=1) 
Nothing
Prelude Data.SBV> minimize Quantified head 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1]
Prelude Data.SBV> minimize Quantified (head . tail) 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1]

第一个结果表明 x=3, y=1 使 x 相对于谓词 x==3 && 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 求解器来说太多无法处理的问题。

于 2012-01-30T02:18:48.000 回答