3 ms·
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
by lheck 1y ago
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"))]])
- happyhacks 1y 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...