Я новичок в изучении Z3 и пытаюсь решить с его помощью головоломку «ОТПРАВИТЬ + БОЛЬШЕ = ДЕНЬГИ». Я решил пару ошибок, скопировав чужой код, но не совсем понимаю, почему это работает.

Вопрос 1: Почему существует разница между этими двумя ограничениями?

Код:

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 также влияет на результат. Почему?

Обновлено: я только что заменил цикл for на solver.add([And(d>=0, d<=9) for d in digits]), и все прошло идеально, до сих пор не знаю почему.