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