It was fun to try to golf this a bit with Z3Py. I'm not an expert at writing for Z3, so it might be possible to do better, but here is a solution in 7 lines:
import z3
res = [("bbababbabb", 7), ("baaababaaa", 5), ("baaabbbaba", 3), ("bbaaabbaaa", z3.Int("x"))]
key = [z3.Int(f"k{i}") for i in range(10)]
z = z3.Solver()
z.add([z3.Sum([ord(a) == k for a, k in zip(r[0], key)]) == r[1] for r in res])
z.check()
print(z.model()[res[-1][1]])
