为什么 Z3 对于类似的约束返回 sat 和 unsat？

Question

我是学习 Z3 的新手，并试图用它解决“发送+更多=金钱”的难题。我通过复制别人的代码解决了一些错误，但我不太明白它为什么有效。

Q1:为什么两个约束有区别？

代码：

from z3 import *

digits = Ints('s e n d m o r y')
s,e,n,d,m,o,r,y = digits
sendmore = 1000*s+100*e+10*n+d+1000*m+100*o+10*r+e
money = 10000*m+1000*o+100*n+10*e+y

solver = Solver()

solver.add([s>0, m>0])
for d in digits:
    solver.add([d>=0, d<=9])
solver.add(Distinct(digits))

solver.add( sendmore == money )
print(solver.check())   #sat

solver.add( 1000*s+100*e+10*n+d+1000*m+100*o+10*r+e == 10000*m+1000*o+100*n+10*e+y )
print(solver.check())   #unsat

一开始我用的是第二种方法，发现不太满意。因此，我用谷歌搜索了第一种方法的解决方案，它返回了 sat。那么有什么区别呢？

Q2：改变定义的位置有何影响？

代码：

from z3 import *

digits = Ints('s e n d m o r y')
s,e,n,d,m,o,r,y = digits

solver = Solver()

solver.add([s>0, m>0])
for d in digits:
    solver.add([d>=0, d<=9])
solver.add(Distinct(digits))

sendmore = 1000*s+100*e+10*n+d+1000*m+100*o+10*r+e
money = 10000*m+1000*o+100*n+10*e+y
solver.add( sendmore == money )
print(solver.check())   #unsat

于是我在乱搞代码，无意中发现移动sendmore和money的定义也会影响结果。为什么？

编辑：我刚刚用

solver.add([And(d>=0, d<=9) for d in digits])

替换了 for 循环，一切都很顺利，但仍然不知道为什么。

Answer 1

缺陷在于

for

循环中，用于界定

digits

的范围：

solver = Solver()
solver.add([s>0, m>0])
for dig in digits:
    solver.add([dig>=0, dig<=9])
solver.add(Distinct(digits))
solver.add( 1000*s+100*e+10*n+d+1000*m+100*o+10*r+e == 10000*m+1000*o+100*n+10*e+y )
res = solver.check()
print(res)  
if res == sat:
    M = solver.model()
    print(M[s],M[e],M[n],M[d],"+",M[m],M[o],M[r],M[e])
    print(M[m],M[o],M[n],M[e],M[y])

循环变量

d

与决策变量

d

发生冲突。
因此，必须重新命名。