desafio_soma_cores.py

from z3 import *

y,g,r,b = Ints("y g r b")
c1, c2, c3, c4 = Ints("c1 c2 c3 c4")

s = Solver()
for v in [y,g,r,b]:
    s.add(z3.And(v > 0, v < 10))
    
    
s.add(c1 == g + g +g)
s.add( c1 % 10 == g )
s.add( c2 == (c1/10) + b + b + b )
s.add( c2 % 10 == r )
s.add( c3 == (c2/10) + r + r + r )
s.add( c3 % 10 == y )
s.add( c4 == (c3/10) + y + y + y)
s.add( c4 == g )

print(s.check())
print(s.model())

"""
[alcides@Alcidess-MacBook-Pro Desktop ]$ python3 desafio_soma_cores.py
sat
[b = 2,
 c1 = 15,
 c4 = 5,
 y = 1,
 c3 = 21,
 r = 7,
 c2 = 7,
 g = 5]

"""