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]])
almost-one-liner (though it will give you the full model):
import z3; z3.solve([z3.Sum([ord(a) == z3.Int(f"k{i}") for i, a in enumerate(r[0])]) == r[1] for r in [("bbababbabb", 7), ("baaababaaa", 5), ("baaabbbaba", 3), ("bbaaabbaaa", z3.Int("x"))]])
