ABC + DEF + GHI = 123J, solve for J

9x.md

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.

9x.z3

; 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)