为什么在此 SBV/Z3 代码中 Int32 排序比 Integer 排序慢得多？

Question

为了学习 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在其他地方使用）吗？我会认为无界SInteger表示会比有界表示慢Int32。

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

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

Answer 1

当您在 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. 特别是，该溶液中SInt32会不会不一定是相同的了SInteger，同样是由于模运算。

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

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

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