РЕШИ + ЕСЛИ = СИЛЕН

RESHI_ESLI_SILEN.smt

;   R E SH I
;   E S L  I
; S I L E  N

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

(declare-const R Int)
(declare-const E Int)
(declare-const SH Int)
(declare-const I Int)
(declare-const S Int)
(declare-const L Int)
(declare-const N Int)

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

(assert (and (>= R 0) (<= R 9)))
(assert (and (>= E 0) (<= E 9)))
(assert (and (>= SH 0) (<= SH 9)))
(assert (and (>= I 0) (<= I 9)))
(assert (and (>= S 0) (<= S 9)))
(assert (and (>= L 0) (<= L 9)))
(assert (and (>= N 0) (<= N 9)))

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

(assert (not (= R 0)))
(assert (not (= E 0)))
(assert (not (= S 0)))

; Рязряды суммы равны не более 5

(assert (<= S 5))
(assert (<= I 5))
(assert (<= L 5))
(assert (<= E 5))
(assert (<= N 5))

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

(assert (not (= R E)))
(assert (not (= R SH)))
(assert (not (= R I)))
(assert (not (= R S)))
(assert (not (= R L)))
(assert (not (= R N)))

(assert (not (= E SH)))
(assert (not (= E I)))
(assert (not (= E S)))
(assert (not (= E L)))
(assert (not (= E N)))

(assert (not (= SH I)))
(assert (not (= SH S)))
(assert (not (= SH L)))
(assert (not (= SH N)))

(assert (not (= I S)))
(assert (not (= I L)))
(assert (not (= I N)))

(assert (not (= S L)))
(assert (not (= S N)))

(assert (not (= L N)))

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

(assert
   (=
      (+
          ; Первое слагаемое
          (+ (* R 1000) (+ (* E 100) (+ (* SH 10) I)))

          ; Второе слагаемое
          (+ (* E 1000) (+ (* S 100) (+ (* L  10) I)))
      )

      ; Результат
      (+ (* S 10000) (+ (* I 1000) (+ (* L 100) (+ (* E 10) N))))
   )
)

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

(check-sat)
(get-model)