performance - Z3:如何提高性能？

Question

在以下 Python 代码中:

from itertools import product
from z3 import *

def get_sp(v0, v1):
    res = sum([v0[i] * v1[i] for i in range(len(v0))])
    return res

def get_is_mod_partition(numbers):
    n = len(numbers)
    mod_power = 2**n
    for signs in product((1, -1), repeat = len(numbers)):
        if get_sp(numbers, signs) % mod_power == 0:
            return 1
    return 0

def check_sat(numbers):
    n = len(numbers)
    s = Solver()
    signs = [Int("s" + str(i)) for i in range(n)]
    for i in range(n):
        s.add(Or(signs[i] == -1, signs[i] == 1))
    s.add(get_sp(numbers, signs) % 2**n == 0)
    print(s.check())

l = [1509, 1245, 425, 2684, 3630, 435, 875, 2286, 1886, 1205, 518, 1372]
check_sat(l)
get_is_mod_partition(l)

check_sat 需要 22 秒，get_is_mod_partition - 24 毫秒。没想到“高性能定理证明器”会有这样的结果。有没有办法大幅提高性能？

Answer 1

按照 Patrick 的建议，您可以编写如下代码:

from z3 import *

def get_sp(v0, v1):
    res = sum([If(v1[i], v0[i], -v0[i]) for i in range(len(v0))])
    return res

def check_sat(numbers):
    n = len(numbers)
    s = Solver()
    signs = [Bool("s" + str(i)) for i in range(n)]
    s.add(get_sp(numbers, signs) % 2**n == 0)
    print(s.check())
    m = s.model()
    mod_power = 2 ** n
    print ("("),
    for (n, sgn) in zip (numbers, signs):
        if m[sgn]:
           print ("+ %d" % n),
        else:
           print ("- %d" % n),
    print (") %% %d == 0" % mod_power)

l = [1509, 1245, 425, 2684, 3630, 435, 875, 2286, 1886, 1205, 518, 1372]
check_sat(l)

在我的机器上运行大约 0.14 秒，并打印:

sat
( - 1509 - 1245 - 425 + 2684 + 3630 + 435 - 875 + 2286 - 1886 - 1205 - 518 - 1372 ) % 4096 == 0

然而，正如帕特里克评论的那样，目前尚不清楚为什么这个版本比原来的版本快得多。我想做一些基准测试，并使用 Haskell 这样做，因为我更熟悉该语言及其 Z3 绑定(bind):

import Data.SBV
import Criterion.Main

ls :: [SInteger]
ls = [1509, 1245, 425, 2684, 3630, 435, 875, 2286, 1886, 1205, 518, 1372]

original = do bs <- mapM (const free_) ls
              let inside b = constrain $ b .== 1 ||| b .== -1
              mapM_ inside bs
              return $ sum [b*l | (b, l) <- zip bs ls] `sMod` (2^length ls) .== 0

boolOnly = do bs <- mapM (const free_) ls
              return $ sum [ite b l (-l) | (b, l) <- zip bs ls] `sMod` (2^length ls) .== 0

main = defaultMain [ bgroup "problem" [ bench "orig" $ nfIO (sat original)
                                      , bench "bool" $ nfIO (sat boolOnly)
                                      ]
                   ]

事实上，只有 bool 的版本快了大约 8 倍:

benchmarking problem/orig
time                 810.1 ms   (763.4 ms .. 854.7 ms)
                     0.999 R²   (NaN R² .. 1.000 R²)
mean                 808.4 ms   (802.2 ms .. 813.6 ms)
std dev              8.189 ms   (0.0 s .. 8.949 ms)
variance introduced by outliers: 19% (moderately inflated)

benchmarking problem/bool
time                 108.2 ms   (104.4 ms .. 113.5 ms)
                     0.997 R²   (0.992 R² .. 1.000 R²)
mean                 109.3 ms   (107.3 ms .. 111.5 ms)
std dev              3.408 ms   (2.261 ms .. 4.843 ms)

两个观察:

• Haskell 绑定(bind)比 Python 的绑定(bind)快得多!大约一个数量级
• 与整数相比，bool-only 版本大约快另一个数量级

对于前者，找出 Python 绑定(bind)性能如此差的原因可能很有趣；或者干脆切换到 Haskell :-)

进一步分析，还有一个可爱的把戏

看来问题出在对 mod 的调用上。在 Haskell 翻译中，系统内部为所有中间表达式命名；这似乎使 z3 运行得更快。然而，Python 绑定(bind)更全面地翻译表达式，并且检查生成的代码(您可以通过查看 s.sexpr() 看到它)表明它没有命名内部表达式。当涉及到 mod 时，我猜测求解器的启发式算法无法识别问题的基本线性并最终花费大量时间。

要缩短时间，您可以执行以下简单技巧。原文说:

s.add(get_sp(numbers, signs) % 2**n == 0)

相反，请确保总和有一个明确的名称。即，将上面的行替换为:

ssum = Int("ssum")
s.add (ssum == get_sp(numbers, signs))
s.add (ssum % 2**n == 0)

您会发现这也使 Python 版本运行得更快。

我仍然更喜欢 bool 转换，但是这个提供了一个很好的经验法则:尝试命名中间表达式，这会根据公式的语义为求解器提供不错的选择点；而不是一个庞大的输出。正如我提到的，Haskell 绑定(bind)不受此影响，因为它在内部将所有公式转换为简单的三操作数 SSA 形式，这使求解器可以更轻松地应用启发式方法。