forked from 0vercl0k/stuffz
-
Notifications
You must be signed in to change notification settings - Fork 0
/
mojette_z3.py
157 lines (135 loc) · 4.56 KB
/
mojette_z3.py
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
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
#!/usr/bin/env python
# -*- coding: utf-8 -*-
#
# mojette_z3.py - Solve the grid of the day (taken from mojette.net) via z3
# Copyright (C) 2012 Axel "0vercl0k" Souchet - http://www.twitter.com/0vercl0k
#
# This program is free software: you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation, either version 3 of the License, or
# (at your option) any later version.
#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
#
import sys
import urllib2
import operator
import BeautifulSoup
from z3 import *
def get_the_grid_of_the_day():
"""Gets the grid of the day on http://www.mojette.net"""
data = urllib2.urlopen('http://www.mojette.net/').read()
bins = map(
lambda bin: int(bin['value'], 10),
BeautifulSoup.BeautifulSoup(data).findAll(
'input',
{
'type' : 'text',
'name' : 'bin',
'class' : 7
}
)
)
# ATM: it exists only one type of grid
assert(len(bins) == 21)
projections = {
'-1,1' : bins[7 : 14],
'1,1' : bins[ : 7],
'0,-1' : bins[14 : ]
}
projections['1,1'].reverse()
return projections
def display_mojette_grid(bins):
"""Display one type of mojette grid (the only one ATM available on the website)"""
print '''
|%d|
|%d|%d|%d|
|%d|%d|%d|%d|%d|
|%d|%d|%d|%d|%d|%d|%d|
|%d|%d|%d|%d|%d|
|%d|%d|%d|''' % tuple(bins)
# thx baaabz
def create_int_constrainted(name, solver, A, B, C):
"""Each pixel must be in [0 - 9], but you must fill the
grid with only 3 digit among the range"""
x = Int(name)
solver.add(Or(x == A, x == B, x == C))
return x
def solve_mojette_grid(projections):
"""Solve the grid thanks to z3py
A bit of terminology:
- The grid is composed of 24 pixels
- A projection is composed of bins
- Each projection is identified by an angle (p, q)"""
s = Solver()
# This is the only 3 values we'll use to fill the grid
A, B, C = Ints('A B C')
s.add(A >= 0, A <= 9, B >= 0, B <= 9, C >= 0, C <= 9)
s.add(Distinct(A, B, C))
# Little schema of the pixel indexes:
# |00|
# |01|02|03|
# |04|05|06|07|08|
# |09|10|11|12|13|14|15|
# |16|17|18|19|20|
# |21|22|23|
pixels = [create_int_constrainted('b%d' % i, s, A, B, C) for i in range(24)]
projections_info = {
'-1,1' : [
# indexes of the pixels constrained by the first projection: -1,1
[0, 3, 8, 15],
[2, 7, 14],
[1, 6, 13, 20],
[5, 12, 19],
[4, 11, 18, 23],
[10, 17, 22],
[9, 16, 21]
],
'0,-1' : [
# indexes of the pixels constrained by the second projection: 1,0
[9],
[16, 10, 4],
[21, 17, 11, 5, 1],
[22, 18, 12, 6, 2, 0],
[23, 19, 13, 7, 3],
[20, 14, 8],
[15]
],
'1,1' : [
# indexes of the pixels constrained by the third projection: -1,1
[0, 1, 4, 9],
[2, 5, 10],
[3, 6, 11, 16],
[7, 12, 17],
[8, 13, 18, 21],
[14, 19, 22],
[15, 20, 23]
]
}
for projection_angle, pixels_constrained in projections_info.iteritems():
idx_projection = 0
for pixels_idx in pixels_constrained:
pixels_values = map(lambda pixel_idx: pixels[pixel_idx], pixels_idx)
s.add(Sum(pixels_values) == projections[projection_angle][idx_projection])
idx_projection += 1
if s.check() == unsat:
raise Exception('The model is not sat, i guess something went wrong.')
m = s.model()
return [m[pixel].as_long() for pixel in pixels]
def main(argc, argv):
print 'Getting the projections from the website..'
p = get_the_grid_of_the_day()
print 'Got it, %r' % p
print 'Now lets move on serious business aka solving..'
r = solve_mojette_grid(p)
print 'Alright done, displaying the grid filled..'
display_mojette_grid(r)
return 1
if __name__ == '__main__':
sys.exit(main(len(sys.argv), sys.argv))