haskell - 为什么在这个 SBV/Z3 代码中 Int32 排序比整数排序慢得多？

Question

为了学习 Z3，我尝试使用 Haskell 绑定(bind) sbv 解决我最喜欢的代码出现问题之一(一个特别困难的问题，2018 day 23, part 2)。 .前面代码中的剧透...

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.smt2在 SMTLib 表示法中，可以将其提供给 Haskell 生态系统之外的求解器。您可以在以下位置提交此类错误:https://github.com/Z3Prover/z3/issues ，但请记住，SBV 生成的 SMTLib 文件可能很长而且很冗长:如果您能以某种方式减小问题大小，仍然可以证明问题，那将很有帮助。