为何基于Z3与OR-Tools的问题建模比Python暴力解法更慢？

问题背景 #

我正尝试为一个源自树结构的复杂方程确定上界，输入通过one-hot变量编码，所有数值均为整数，所有项均为其他项与布尔值的和或积。根据建议，我采用整数线性规划（ILP）对问题建模，分别用Google OR-Tools生成模型、Microsoft Z3编写对应的SMT文件，同时在Python中实现暴力解法作为对比。但意外的是，Python暴力解法的速度远超两者，我原本以为暴力解法会是最慢的，因此想弄清楚其中原因。

代码实现 #

Python暴力解法 #

def w(c0, c1, c2, c3, c4, c5):
    a0,e0,i0,o0,u0 = c0     # exactly one of these will be True
    c1,h1,k1,m1,p1,t1 = c1  # (same for all the cN variables)
    a2,e2,i2,o2,u2 = c2     # ...
    l3,n3,r3,s3,y3 = c3     # ...
    b4,d4,f4,g4,j4,v4,w4,x4,z4 = c4  # ...
    c5,h5,k5,m5,p5,t5 = c5
    n_0=1+d4
    n_1=(s3*2)+(y3*2)
    n_2=1+n_1
    n_3=(d4*n_2)
    n_4=(e2*n_0)+(i2*n_3)
    n_5=(d4*2)
    # ...
    n_3293=n_3220+n_3281+n_3292
    n_3294=(c5*n_2914)+(h5*n_2973)+(k5*n_3016)+(m5*n_3119)+(p5*n_3202)+(t5*n_3293)
    n_3295=n_384+n_1082+n_1412+n_1938+n_2788+n_3294
    return n_3295

OR-Tools建模代码 #

from ortools.sat.python import cp_model
model = cp_model.CpModel()
cells = []

a0 = model.new_bool_var("a0")
e0 = model.new_bool_var("e0")
i0 = model.new_bool_var("i0")
o0 = model.new_bool_var("o0")
u0 = model.new_bool_var("u0")
model.AddExactlyOne(a0, e0, i0, o0, u0)
# ... similar "one-hot" encoding for the other free variables

n_0 = model.new_int_var(0, 2, "n_0")
model.add(n_0 == 1 + d4)
n_1 = model.new_int_var(0, 2, "n_1")
model.add(n_1 == (s3 * 2) + (y3 * 2))
n_2 = model.new_int_var(0, 3, "n_2")
model.add(n_2 == 1 + n_1)
p_0 = build_product_var(model, d4, n_2, "p_0")
n_3 = model.new_int_var(0, 3, "n_3")
model.add(n_3 == p_0)
p_1 = build_product_var(model, e2, n_0, "p_1")
p_2 = build_product_var(model, i2, n_3, "p_2")
n_4 = model.new_int_var(0, 3, "n_4")
model.add(n_4 == p_1 + p_2)
n_5 = model.new_int_var(0, 2, "n_5")
model.add(n_5 == (d4 * 2))
# ...
n_3294 = model.new_int_var(0, 45, "n_3294")
model.add(n_3294 == p_2589 + p_2590 + p_2591 + p_2592 + p_2593 + p_2594)
n_3295 = model.new_int_var(0, 250, "n_3295")
model.add(n_3295 == n_384 + n_1082 + n_1412 + n_1938 + n_2788 + n_3294)
model.add(n_3295 >= 45)

solver = cp_model.CpSolver()
status = solver.solve(model)

Z3 SMT文件代码 #

(declare-const a0 Bool)
(declare-const e0 Bool)
(declare-const i0 Bool)
(declare-const o0 Bool)
(declare-const u0 Bool)
(assert (= (+ a0 e0 i0 o0 u0) 1))
; ...
(declare-const n_0 Int)
(assert (= n_0 (+ 1 d4)))
(declare-const n_1 Int)
(assert (= n_1 (+ (* s3 2) (* y3 2))))
(declare-const n_2 Int)
(assert (= n_2 (+ 1 n_1)))
(declare-const n_3 Int)
(assert (= n_3 (+ (* d4 n_2))))
(declare-const n_4 Int)
(assert (= n_4 (+ (* e2 n_0) (* i2 n_3))))
(declare-const n_5 Int)
(assert (= n_5 (+ (* d4 2))))
; ...
(declare-const n_3294 Int)
(assert (= n_3294 (+ (* c5 n_2914) (* h5 n_2973) (* k5 n_3016) (* m5 n_3119) (* p5 n_3202) (* t5 n_3293))))
(declare-const n_3295 Int)
(assert (= n_3295 (+ n_384 n_1082 n_1412 n_1938 n_2788 n_3294)))
(assert (> n_3295 45))

(check-sat)

测试耗时（M2 MacBook） #

• Python暴力解法：4.755秒
• OR-Tools：8.7秒
• Z3：19.5秒

已尝试的优化 #

• 为Z3添加(check-sat-using (then simplify smt))：速度提升约50%。
• 为OR-Tools使用build_product_var方法：带来小幅提速。

疑问 #

我是否忽略了什么？还是说这个问题对这些求解器来说确实难度很高？

内容的提问来源于stack exchange，提问作者danvk