Z3: how to improve performance?

Question

In following Python code:

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 takes 22 seconds and get_is_mod_partition - 24 millseconds. I haven't expected such results from "high-performance theorem prover". Is there way to drastically improve performance?

Answer 1

按照帕特里克的建议，您可以将其编码如下：

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 绑定：

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-only 版本快了大约 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 绑定比 Python 的要快得多！大约一个数量级
• 与整数相比，bool-only 版本大约快了另一个数量级

对于前者，找出为什么 Python 绑定的性能如此糟糕可能会很有趣；或者干脆切换到 Haskell :-)

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

问题似乎出在调用mod. 在 Haskell 翻译中，系统内部为所有中间表达式命名；这似乎使 z3 走得更快。然而，Python 绑定更全面地翻译表达式，并且检查生成的代码（您可以通过查看 看到它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 版本运行得更快。

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