为什么我的Z3和Or-Tools的问题比Python中的蛮力要慢？ 我正在尝试建立一个来自树的相当复杂的方程式上的上限。它具有少数可以用“一击”变量编码的输入。所有数字...

Question

令我惊讶的是，到目前为止，Python中的蛮力解决方案是最快的！我本来会认为这是迄今为止最慢的，所以我想念什么？ python是Python的样子（

fullcode）：

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

the Or-tools配方的外观（

fullcode

）：

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（

fullCode

）的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.755S或工具：8.7S

Z3：19.5S

我本来希望蛮力搜索对求解器而言是最糟糕的情况，而Python几乎不是一种快速的语言，所以我想知道我的编码是否效率低下。我尝试过的几件事：

add

(check-sat-using (then simplify smt))

对于Z3：运行〜50％的速度。
• 用语this this Answer
为Or-Tools。这可能是一个很小的速度。
那里我缺少什么？还是对于这些求解器而言，这只是一个非常困难的问题？

建设性方法的速度比指数搜索要快。