3 ms·
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:
by a_e_k 2y ago
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]])
- lheck 2y agoalmost-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"))]])
- happyhacks 2y agomy take - more writeup style for people new to z3 https://happyhacks.bearblog.dev/solving-a-layton-puzzle-with-z3/ https://happyhacks.bearblog.dev/solving-a-layton-puzzle-with...