Frazioni maledette

cursed-fraction.py

from z3 import Int, Solver, Not, And, sat

a = Int("a")
b = Int("b")
c = Int("c")

s = Solver()
s.add(a > 0, a < 10)
s.add(b > 0, b < 10)
s.add(c > 0, c < 10)
s.add(a != c)
s.add((10 * a + b) * c == a * (b * 10 + c))
s.add((100 * a + 11 * b) * c == a * (b * 110 + c))
while s.check() == sat:
    m = s.model()
    print(f"Solution: {m[a]}{m[b]}/{m[b]}{m[c]} = {m[a]}/{m[c]}")
    s.add(Not(And(a == m[a], b == m[b], c == m[c])))

solutions.txt

16/64 = 1/4
26/65 = 2/5
19/95 = 1/5
49/98 = 4/8