6

为了学习 Z3，我尝试使用 Haskell 绑定解决我最喜欢的代码出现问题之一（一个特别困难的问题， 2018 年第 23 天，第 2 部分sbv） 。前面代码中的剧透...

module Lib
    ( solve
    ) where

import Data.SBV

puzzle :: [((SInteger, SInteger, SInteger), SInteger)]
puzzle = (\((x, y, z), r) -> ((literal x, literal y, literal z), literal r)) <$> [
      ((60118729,58965711,8716524), 71245377),
      {- 999 more values that are large like the first one... -}
]

manhattan (a1, a2, a3) (b1, b2, b3) =
  abs (a1 - b1) + abs (a2 - b2) + abs (a3 - b3)

countInRange pos =
  foldr (\(nb, r) -> (+) $ oneIf (manhattan nb pos .<= r)) (0 :: SInteger) puzzle

answer = optimize Lexicographic $ do
  x <- sInteger "x"
  y <- sInteger "y"
  z <- sInteger "z"
  maximize "in-range"             $ countInRange (x, y, z)
  minimize "distance-from-origin" $ abs x + abs y + abs z

solve =
  answer >>= print

现在，这个问题不是一个真正的sbv问题，也不是一个 Haskell 问题，上面的代码并没有什么问题（它解决了 1000 个值puzzle列表，在我的机器上在一分钟多一点的时间内具有巨大的 X、Y 和 Z 坐标，即对我来说已经足够好了）。这个问题是关于(0 :: SInteger)在countInRange.

如果我更改(0 :: SInteger)它(0 :: SInt32)会导致解决方案需要很长时间（当我开始输入这个问题时我开始了它，那是 16 分钟前并且还在计数）。

那么，什么给了？为什么SInt32在这种情况下慢得多？是因为我在混合域（SInteger在其他地方使用）吗？我会认为 unboundedSInteger表示会比 bounded 慢Int32。

请注意，所讨论的符号类型仅用于计算匹配值puzzle（因此它总是 <= 1000，即 的长度puzzle）。

更新 我Int32在运行 40 分钟后终止了解决方案。

4

1 回答 1

6

当您在 SBV 中编写这样的问题时，有两个地方可以发挥性能：

  • SBV 可能需要很长时间才能生成查询本身
  • SBV 很好地将查询发送给求解器，但求解器需要很长时间才能响应

从你的描述来看，似乎是后者；但是您可以通过这样调用来确保是这种情况optimize：

optimizeWith z3{verbose=True} ...

这将打印 SBV 与后端求解器的交互。在某些时候，您会看到：

[SEND] (check-sat)

这意味着 SBV 已经完成了它的工作，现在正在等待求解器返回答案。打开此选项再次运行您的程序。如果 SBV 正在花时间，那么您将看不到上面的[SEND] (check-sat)行，这应该在此处报告为 SBV 问题：https ://github.com/LeventErkok/sbv/issues

更有可能的是，SBV 正在发送check-sat罚款，但是当您使用SInt32而不是SInteger.

假设是这种情况，那么这很可能是因为当底层类型为SInt32. 您正在做大量的算术运算并要求求解器最大化和最小化两个单独的目标。你可以想象，如果你有无限Integer的值，最大化数字的加法可能很容易处理：随着参数的增加，它们的总和也会增加。但对于SInt32: 一旦值开始溢出，由于环绕，总和将远低于参数。因此，使用模运算，搜索空间变得更有趣，与SInteger案例相比更大。底线是，虽然SInt32有一个有限的表示，优化问题SInt32 x SInt32 x SInt32（你有三个变量），由于与SInteger x SInteger x SInteger. 特别是，over 的解SInt32不一定与over 相同SInteger，这同样是由于模运算。

当然，在 z3 内部发生的事情更像是一个黑匣子，也许它们的速度慢得不合理。如果您认为是这种情况，您也可以将其报告给 z3 人员。SBV 可以生成一个成绩单供您发送给他们，当这样使用时：

optimizeWith z3{transcript = Just "longRun.smt2"} ...

这将创建一个longRun.smt2SMTLib 表示法的文件，该文件可以提供给 Haskell 生态系统之外的求解器。您可以在以下位置提交此类错误：https ://github.com/Z3Prover/z3/issues ，但请记住，SBV 生成的 SMTLib 文件可能很长且冗长：如果您可以以某种方式减少问题大小，仍然可以证明问题，那会很有帮助。

于 2020-02-26T17:23:40.003 回答