Instantly share code, notes, and snippets.

# t3rmin4t0r/9x.md

Last active November 25, 2021 22:08
Show Gist options
• Save t3rmin4t0r/a953450ac64b6868540bbce79df4e9a3 to your computer and use it in GitHub Desktop.
ABC + DEF + GHI = 123J, solve for J

# ABC + DEF + GHI = 123J

All letters represent unique numbers between 0-9

Basic starting point: If you subtract all the digits from a number, you get a multiple of 9

``````ABC = 100 x A + 10 x B + C = (99 x A + 9 x B) + A + B + C = 9 (11 x A + B) + A + B + C
``````

Inversely stated, it means

``````ABC = 9x + A + B + C

ABC + DEF + GHI = (9x + A + B + C) + (9y + D + E + F) + (9z + G + H + I)

ABC + DEF + GHI = 9 (x+y+z) + (A + B + C + D + E + F + G + H + I)

ABC + DEF + GHI + J = 9 (x+y+z) + (A + ... I + J)

123J = (9q + 1 + 2 + 3 + J)

(A + ... + I + J) = (9 + 1) + (8 + 2) + (7 + 3) + (6 + 4) + 5
(A + ... + I + J) = 45 = 9 x 5
ABC + DEF + GHI + J = 9 (x + y + z + 5)
``````

To restate original problem with additional J

``````123J + J = ABC + DEF + GHI + J = 9 (x + y + z + 5)

123J + J = (9q + (1 + 2 + 3 + J)) + J = 9q + 6 + 2J
``````

To remove the extra 9s, we can modulo the numbers (they are equal, so it should be the same)

``````(123J + J) % 9 = (ABC + DEF + GHI + J) % 9 = (9 (x + y + z + 5)) % 9 = 0

(123J + J) % 9 = (9q + 6 + 2J) % 9 = (6 + 2J) % 9 = 0
``````

Ending up with a single variable to solve for

``````(6 + 2J) % 9 = 0
``````

This implies it is a multiple of 2

``````2 (3 + J) = 9q = 9 x 2 x (m + 1)

J = 9 - 3 + 9 * m

J = 6 + 9 * m
``````

But we know J is < 9, so m = 0. Ending up with J = 6 without question.

This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 ; Variable declarations (declare-fun a () Int) (declare-fun b () Int) (declare-fun c () Int) (declare-fun d () Int) (declare-fun e () Int) (declare-fun f () Int) (declare-fun g () Int) (declare-fun h () Int) (declare-fun i () Int) (declare-fun j () Int) ; Constraints (assert (>= a 0)) (assert (>= b 0)) (assert (>= c 0)) (assert (>= d 0)) (assert (>= e 0)) (assert (>= f 0)) (assert (>= g 0)) (assert (>= h 0)) (assert (>= i 0)) (assert (>= j 0)) (assert (< a 10)) (assert (< b 10)) (assert (< c 10)) (assert (< d 10)) (assert (< e 10)) (assert (< f 10)) (assert (< g 10)) (assert (< h 10)) (assert (< i 10)) (assert (< j 10)) (assert(not (= a b))) (assert(not (= a c))) (assert(not (= a d))) (assert(not (= a e))) (assert(not (= a f))) (assert(not (= a g))) (assert(not (= a h))) (assert(not (= a i))) (assert(not (= a j))) (assert(not (= b a))) (assert(not (= b c))) (assert(not (= b d))) (assert(not (= b e))) (assert(not (= b f))) (assert(not (= b g))) (assert(not (= b h))) (assert(not (= b i))) (assert(not (= b j))) (assert(not (= c a))) (assert(not (= c b))) (assert(not (= c d))) (assert(not (= c e))) (assert(not (= c f))) (assert(not (= c g))) (assert(not (= c h))) (assert(not (= c i))) (assert(not (= c j))) (assert(not (= d a))) (assert(not (= d b))) (assert(not (= d c))) (assert(not (= d e))) (assert(not (= d f))) (assert(not (= d g))) (assert(not (= d h))) (assert(not (= d i))) (assert(not (= d j))) (assert(not (= e a))) (assert(not (= e b))) (assert(not (= e c))) (assert(not (= e d))) (assert(not (= e f))) (assert(not (= e g))) (assert(not (= e h))) (assert(not (= e i))) (assert(not (= e j))) (assert(not (= f a))) (assert(not (= f b))) (assert(not (= f c))) (assert(not (= f d))) (assert(not (= f e))) (assert(not (= f g))) (assert(not (= f h))) (assert(not (= f i))) (assert(not (= f j))) (assert(not (= g a))) (assert(not (= g b))) (assert(not (= g c))) (assert(not (= g d))) (assert(not (= g e))) (assert(not (= g f))) (assert(not (= g h))) (assert(not (= g i))) (assert(not (= g j))) (assert(not (= h a))) (assert(not (= h b))) (assert(not (= h c))) (assert(not (= h d))) (assert(not (= h e))) (assert(not (= h f))) (assert(not (= h g))) (assert(not (= h i))) (assert(not (= h j))) (assert(not (= i a))) (assert(not (= i b))) (assert(not (= i c))) (assert(not (= i d))) (assert(not (= i e))) (assert(not (= i f))) (assert(not (= i g))) (assert(not (= i h))) (assert(not (= i j))) (assert(not (= j a))) (assert(not (= j b))) (assert(not (= j c))) (assert(not (= j d))) (assert(not (= j e))) (assert(not (= j f))) (assert(not (= j g))) (assert(not (= j h))) (assert(not (= j i))) (assert (= (+ (+(* a 100) (+ (* b 10) c)) (+ (+(* d 100) (+ (* e 10) f)) (+(* g 100) (+ (* h 10) i)) )) (+ 1230 j))) ; Solve (check-sat) (get-model)