SEND+MORE=MONEY.smt

SEND_MORE_MONEY.smt

;   S E N D
;   M O R E
; M O N E Y

; Обявление уникальных букв

(declare-const S Int)
(declare-const E Int)
(declare-const N Int)
(declare-const D Int)
(declare-const M Int)
(declare-const O Int)
(declare-const R Int)
(declare-const Y Int)

; Ограничения для разрядов

(assert (and (>= S 0) (<= S 9)))
(assert (and (>= E 0) (<= E 9)))
(assert (and (>= N 0) (<= N 9)))
(assert (and (>= D 0) (<= D 9)))
(assert (and (>= M 0) (<= M 9)))
(assert (and (>= O 0) (<= O 9)))
(assert (and (>= R 0) (<= R 9)))
(assert (and (>= Y 0) (<= Y 9)))

; Лидирующие разряды не равны 0

(assert (not (= S 0)))
(assert (not (= M 0)))

; Разряды не равны друг другу

(assert (not (= S E)))
(assert (not (= S N)))
(assert (not (= S D)))
(assert (not (= S M)))
(assert (not (= S O)))
(assert (not (= S R)))
(assert (not (= S Y)))

(assert (not (= E N)))
(assert (not (= E D)))
(assert (not (= E M)))
(assert (not (= E O)))
(assert (not (= E R)))
(assert (not (= E Y)))

(assert (not (= N D)))
(assert (not (= N M)))
(assert (not (= N O)))
(assert (not (= N R)))
(assert (not (= N Y)))

(assert (not (= D M)))
(assert (not (= D O)))
(assert (not (= D R)))
(assert (not (= D Y)))

(assert (not (= M O)))
(assert (not (= M R)))
(assert (not (= M Y)))

(assert (not (= O R)))
(assert (not (= O Y)))

(assert (not (= R Y)))

; Формула суммы

(assert
   (=
      (+
          ; Первое слагаемое
          (+ (* S 1000) (+ (* E 100) (+ (* N 10) D)))

          ; Второе слагаемое
          (+ (* M 1000) (+ (* O 100) (+ (* R  10) E)))
      )

      ; Результат
      (+ (* M 10000) (+ (* O 1000) (+ (* N 100) (+ (* E 10) Y))))
   )
)

; Получить ответ

(check-sat)
(get-model)