Pull to refresh

Comments 7

Проще и красивей всего такое решать с помощью SMT солверов. Например, запись под Z3 выглядит следующим образом (первый пример):


;    U  M
; SH U  M
;  V M SH

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

(declare-const U Int)
(declare-const M Int)
(declare-const SH Int)
(declare-const V Int)

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

(assert (and (>= U 0) (<= U 9)))
(assert (and (>= M 0) (<= M 9)))
(assert (and (>= SH 0) (<= SH 9)))
(assert (and (>= V 0) (<= V 9)))

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

(assert (not (= U 0)))
(assert (not (= SH 0)))
(assert (not (= V 0)))

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

(assert (not (= U M)))
(assert (not (= U SH)))
(assert (not (= U V)))

(assert (not (= M SH)))
(assert (not (= M V)))

(assert (not (= SH V)))

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

(assert
   (=
      (+
          ; Первое слагаемое
          (+ (* U 10) M)

          ; Второе слагаемое
          (+ (* SH 100) (+ (* U  10) M))
      )

      ; Результат
      (+ (* V 100) (+ (* M 10) SH))
   )
)

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

(check-sat)
(get-model)

Запускаем и получаем ответ:


sat
(
  (define-fun SH () Int
    8)
  (define-fun U () Int
    7)
  (define-fun M () Int
    4)
  (define-fun V () Int
    9)
)

Здорово! Вы предлагаете в процессе решения криптарифма генерировать для него такую программку?

Так обычно и делают.

Да. Возможно саму запись можно еще упростить, но я не эксперт в солверах.

А сможете сделать такой алгоритм, который не будет проверять по буквам, а будет смотреть на это с абсолютной точки зрения, то есть алгоритму будет без разницы какой там символ, А или G?

Так ему нет особой разницы, на A вы заменили , скажем, цифру 4 или на G! Не очень понял вопрос.

Sign up to leave a comment.

Articles