-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathclogic_puzzle_solver
executable file
·116 lines (102 loc) · 3.74 KB
/
clogic_puzzle_solver
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
#!/usr/bin/env python
from __future__ import print_function
import z3
def digit_var(name):
v = z3.BitVec(name, 32)
solver.add(v >= 0)
solver.add(v <= 9)
return v
def word_var(name):
v = z3.BitVec(name, 32)
digits = ([digit_vars[c] for c in name])
val_v = reduce(lambda a,b: a*10+b, digits, 0)
solver.add(val_v == v)
return v
solver = z3.Solver()
digits = ["b", "c", "d", "f", "g", "h", "i", "j", "l", "n", "o", "q", "s", "t", "u", "v", "w", "x", "y", "z"]
digit_vars = {v:digit_var(v) for v in digits}
words = [
"bytwycju",
"bzuwtwol",
"cgyoyfjg",
"ctvtwysu",
"dhcqxtfw",
"diffhlnl",
"fjivucti",
"htwizvwi",
"jqxizzxq",
"niiqztgs",
"nshtztns",
"nttuhlnq",
"oigsjgoj",
"oncycbxh",
"oqbctlzh",
"oqcnwbsd",
"sfgsoxdd",
"sugvqgww",
"syhjizjq",
"szblgodf",
"thhwohwn",
"ttligxut",
"uclfqvdu",
"udluvhcz",
"ugdztnwv",
"uxztiywn",
"vugljtyn",
"vyhyjivb",
"wwnnnqbw",
"xbfziozy",
"xsvuojtx",
"yjjowdqh",
"yzdgotby",
"yzvyjjdy",
"zoljwdfl",
]
wv = {w:word_var(w) for w in words}
# Everyone occurs twice, this is not quite that
solver.add(z3.Sum(digit_vars.values()) == 90)
solver.add(wv["bytwycju"] + wv["yzvyjjdy"] ^ wv["vugljtyn"] + wv["ugdztnwv"] | wv["xbfziozy"] == wv["bzuwtwol"])
solver.add(wv["wwnnnqbw"] - wv["uclfqvdu"] & wv["oncycbxh"] | wv["oqcnwbsd"] ^ wv["cgyoyfjg"] == wv["vyhyjivb"])
solver.add(wv["yzdgotby"] | wv["oigsjgoj"] | wv["ttligxut"] - wv["dhcqxtfw"] & wv["szblgodf"] == wv["sfgsoxdd"])
solver.add(wv["yjjowdqh"] & wv["niiqztgs"] + wv["ctvtwysu"] & wv["diffhlnl"] - wv["thhwohwn"] == wv["xsvuojtx"])
solver.add(wv["nttuhlnq"] ^ wv["oqbctlzh"] - wv["nshtztns"] ^ wv["htwizvwi"] + wv["udluvhcz"] == wv["syhjizjq"])
solver.add(wv["bytwycju"] ^ wv["wwnnnqbw"] & wv["yzdgotby"] + wv["yjjowdqh"] - wv["nttuhlnq"] == wv["fjivucti"])
solver.add(wv["yzvyjjdy"] ^ wv["uclfqvdu"] & wv["oigsjgoj"] + wv["niiqztgs"] - wv["oqbctlzh"] == wv["zoljwdfl"])
solver.add(wv["vugljtyn"] ^ wv["oncycbxh"] & wv["ttligxut"] + wv["ctvtwysu"] - wv["nshtztns"] == wv["sugvqgww"])
solver.add(wv["ugdztnwv"] ^ wv["oqcnwbsd"] & wv["dhcqxtfw"] + wv["diffhlnl"] - wv["htwizvwi"] == wv["uxztiywn"])
solver.add(wv["xbfziozy"] ^ wv["cgyoyfjg"] & wv["szblgodf"] + wv["thhwohwn"] - wv["udluvhcz"] == wv["jqxizzxq"])
key = "iw, hu, fv, lu, dv, cy, og, lc, gy, fq, od, lo, fq, is, ig, gu, hs, hi, ds, cy, oo, os, iu, fs, gu, lh, dq, lv, gu, iw, hv, gu, di, hs, cy, oc, iw, gc".split(", ")
if solver.check() == z3.sat:
model = solver.model()
print(model)
result = []
for (a,b) in key:
av = int(str(model[digit_vars[a]]))
bv = int(str(model[digit_vars[b]]))
r = chr(10*av+bv)
result.append(r)
print("".join(result))
else:
print("failed to solve")
# The puzzle:
"""
We've captured a strange message. It looks like it is encrypted somehow ...
iw, hu, fv, lu, dv, cy, og, lc, gy, fq, od, lo, fq, is, ig, gu, hs, hi, ds, cy, oo, os, iu, fs, gu, lh, dq, lv, gu, iw, hv, gu, di, hs, cy, oc, iw, gc
We've also intercepted what seems to be a hint to the key:
bytwycju + yzvyjjdy ^ vugljtyn + ugdztnwv | xbfziozy = bzuwtwol
^ ^ ^ ^ ^
wwnnnqbw - uclfqvdu & oncycbxh | oqcnwbsd ^ cgyoyfjg = vyhyjivb
& & & & &
yzdgotby | oigsjgoj | ttligxut - dhcqxtfw & szblgodf = sfgsoxdd
+ + + + +
yjjowdqh & niiqztgs + ctvtwysu & diffhlnl - thhwohwn = xsvuojtx
- - - - -
nttuhlnq ^ oqbctlzh - nshtztns ^ htwizvwi + udluvhcz = syhjizjq
= = = = =
fjivucti zoljwdfl sugvqgww uxztiywn jqxizzxq
Note:
assume q != 0
a letter is a decimal digit is a letter
each digit has exactly two different letter representations
C-like operator precedence
"""