0

在我的一个 SMT 程序中，我使用了一个实数。我需要限制实数的精度以提高效率，因为这个数字几乎可以有无数种解决方案，尽管只需要小数点后的 5/6 位。例如，实数的可能估值如下，尽管如果我们取小数点后的前七位数字，所有这些都是相同的。

1197325/13631488 = 0.087835238530……

19157213/218103808 = 0.087835298134……

153257613/1744830464 = 0.087835245980……

1226060865/13958643712 = 0.087835243186……

我希望 SMT 求解器将所有这四个数字视为一个数字（以便减少搜索空间）。有没有办法控制实数的精度？

我尝试以编程方式（使用 Z3 Dot Net API）来解决上述问题，如下所示。这里 DelBP[j] 是一个实数。

{
    BoolExpr[] _Exprs = new BoolExpr[nBuses];
    for (j = 1; j <= nBuses; j++)
    {
        _Exprs[j - 1] = z3.MkEq(DelBP[j], z3.MkDiv(z3.MkInt2Real(DelBP_A[j]), z3.MkInt2Real(DelBP_B[j])));
    }

    BoolExpr Expr = z3.MkAnd(_Exprs);
    s.Assert(Expr);
    tw.WriteLine("(assert {0})", Expr.ToString());
}

{
    BoolExpr[] _Exprs = new BoolExpr[nBuses];
    for (j = 1; j <= nBuses; j++)
    {
        _Exprs[j - 1] = z3.MkAnd(z3.MkGe(DelBP_A[j], z3.MkInt(1)),
            z3.MkLe(DelBP_A[j], z3.MkInt(10000)));
    }

    BoolExpr Expr = z3.MkAnd(_Exprs);
    s.Assert(Expr);
    tw.WriteLine("(assert {0})", Expr.ToString());
}

{
    BoolExpr[] _Exprs = new BoolExpr[nBuses];
    for (j = 1; j <= nBuses; j++)
    {
        _Exprs[j - 1] = z3.MkAnd(z3.MkGe(DelBP_B[j], z3.MkInt(1)),
            z3.MkLe(DelBP_B[j], z3.MkInt(10000)));
    }

    BoolExpr Expr = z3.MkAnd(_Exprs);
    s.Assert(Expr);
    tw.WriteLine("(assert {0})", Expr.ToString());
}

但是，它没有用。谁能帮我解决这个问题？先感谢您。

4

1 回答 1

1

如果您觉得需要控制实数的“精度”，那么这强烈表明Real这不是您的问题的正确领域。一些想法，取决于你真正想做的事情：

  • 如果您只关心小数点后的 6 位数字，那么您可能会使用普通Integer的 s，将所有内容乘以1e6并将所有变量限制为小于1e6; 或其他类似的转换。

  • 请记住，Z3 目前已支持 IEEE 浮点数，根据有限精度的定义。因此，如果您的域确实是 IEEE-754 规定的浮点数，则可以使用它们。

  • 如果您试图生成“连续”的结果，即通过解决问题，然后添加结果应该与前一个不同的约束，并再次调用 Z3；那么您可以考虑添加一个约束，说明新结果与旧结果的绝对值差异应大于1e6绝对值。

这是否适用取决于您要解决的确切问题。如果您可以分享更多问题，人们可能会提出其他想法。但第一选择应该是弄清楚是否Real真的是您想要使用的域。

于 2013-08-29T19:59:12.420 回答