chiark / gitweb /
Filled in the observations section.
[matchsticks-search.git] / tabulate.py
1 #!/usr/bin/env python
2
3 import sys, os, re, fractions
4 from fractions import Fraction
5
6 import bounds
7
8 header_re = re.compile(r'^(\d+) into (\d+).*:.* ([\d/]+)')
9 dissect_re = re.compile(r'\s+(\d+)\s+x\s+\((([\d/]+ \+ )*[\d/]+)\)')
10
11 dissections = {}
12
13 def find_min_frag(dissection):
14     ret = None
15     for side in dissection:
16         for count, pieces in side:
17             for piece in pieces:
18                 if piece > 0:
19                     if ret is None or ret > piece:
20                         ret = piece
21     assert ret is not None
22     return ret
23
24 def verify(n, m, dissection):
25     collections = [{}, {}]
26     total = 0
27     for count, pieces in dissection[0]:
28         assert sum(pieces) == n
29         total += count
30         for piece in pieces:
31             collections[0].setdefault(piece, 0)
32             collections[0][piece] += count
33     assert total == m
34     total = 0
35     for count, pieces in dissection[1]:
36         assert sum(pieces) == m
37         total += count
38         for piece in pieces:
39             collections[1].setdefault(piece, 0)
40             collections[1][piece] += count
41     assert total == n
42     assert collections[0] == collections[1]
43
44 def factor_dissector(n,m):
45     ret = []
46     gcd = fractions.gcd(n,m)
47     for i in range(1, gcd+1):
48         if gcd % i != 0: continue
49         prev = dissections[n/i, m/i]
50         ret.append(([[(i*count, [piece*i for piece in pieces])
51                       for count, pieces in prev[0]],
52                      [(i*count, [piece*i for piece in pieces])
53                       for count, pieces in prev[1]]],
54                     "multiply solution for (%d,%d) by %d" % (n/i, m/i, i)))
55
56 def add_m_dissector(n,m):
57     if n <= 2*m:
58         return []
59     prev = dissections[(n-m, m)]
60     ret = [prev[0][:], prev[1][:]]
61     for i in range(len(ret[0])):
62         ret[0][i] = (ret[0][i][0], ret[0][i][1] + [m])
63     ret[1].append((m, (m,)))
64     return [(ret, "extend solution for (%d,%d) by %d" % (n-m, m, m))]
65
66 def gcd_dissector(n,m):
67     gcd = fractions.gcd(n,m)
68     return [([[(m, (gcd,) * (n/gcd))],
69               [(n, (gcd,) * (m/gcd))]], "trivial gcd solution")]
70
71 def invent_dissection(n,m):
72     # Try to come up with a dissection by assorted simple methods.
73     best = 0
74     for dissector in [gcd_dissector, add_m_dissector]:
75         for dissection, this_reason in dissector(n, m):
76             if dissection is None: continue
77             verify(n, m, dissection)
78             this_best = find_min_frag(dissection)
79             if best < this_best:
80                 best, best_reason = this_best, this_reason
81     assert best > 0
82     return dissection, this_reason
83
84 details = {} # maps (n,m) to a snippet of HTML
85
86 def read_and_build_table_cell(n,m):
87     ret = ""
88
89     best = 0
90
91     # Look for appropriate file(s).
92     for filename, nature in [("data/main.%d.%d" % (n,m), "e"),
93                              ("data/partition.%d.%d" % (n,m), "p"),
94                              ("data/manual.%d.%d" % (n,m), "m")]:
95         if os.path.exists(filename):
96             with open(filename) as f:
97                 header = f.readline()
98                 match = header_re.match(header)
99                 assert match is not None
100                 assert int(match.group(1)) == n
101                 assert int(match.group(2)) == m
102                 this_best = Fraction(match.group(3))
103
104                 # Now read the actual dissection.
105                 dissection = [[],[]]
106                 for line in f.readlines():
107                     match = dissect_re.match(line)
108                     if match is not None:
109                         count = int(match.group(1))
110                         pieces = map(Fraction, match.group(2).split(" + "))
111                         length = sum(pieces)
112                         if length == n:
113                             dissection[0].append((count, pieces))
114                         elif length == m:
115                             dissection[1].append((count, pieces))
116                         else:
117                             assert False, "wrong length"
118                 verify(n, m, dissection)
119                 assert find_min_frag(dissection) == this_best
120                 dissections[(n,m)] = dissection
121
122                 if this_best > best:
123                     best = this_best
124                     best_nature = nature
125
126     if best == 0:
127         # We don't have a stored solution at all, so make up something
128         # plausible if we can.
129         dissection, auto_reason = invent_dissection(n, m)
130         best = find_min_frag(dissection)
131         dissections[(n,m)] = dissection
132         best_nature = 'a'
133
134     bound, bound_type = bounds.upper_bound(n, m)
135
136     if best == bound:
137         tdclass = "known"
138         show_bound = ""
139     elif best_nature == 'e':
140         tdclass = "believed"
141         show_bound = ""
142     elif best_nature == 'p':
143         tdclass = "probable"
144         show_bound = ""
145     else:
146         tdclass = "range"
147         show_bound = "&nbsp;&ndash;&nbsp;%s"
148     ret += "<td class=\"%s\"><a href=\"#details_%d_%d\">" % (tdclass, n, m)
149     ret += str(best)
150     if show_bound != "":
151         ret += show_bound % str(bound)
152     ret += "</a></td>\n"
153
154     dump = "<h3><a name=\"details_%d_%d\">n=%d, m=%d</a></h3>\n" % (n, m, n, m)
155     dump += "<p>Best dissection known for %d into %d: minimum fragment is %s.\n" % (n, m, str(best))
156     dump += "<ul><li>Cut up %d sticks of length %d as follows:<ul>\n" % (m, n)
157     for count, pieces in dissection[0]:
158         dump += "<li>%d &times; (%s)\n" % (count, " + ".join(map(str, pieces)))
159     dump += "</ul><li>Reassemble as %d sticks of length %d as follows:<ul>\n" % (n, m)
160     for count, pieces in dissection[1]:
161         dump += "<li>%d &times; (%s)\n" % (count, " + ".join(map(str, pieces)))
162     dump += "</ul></ul>\n"
163     if best == bound:
164         dump += "<p>This dissection is confidently believed optimal because an upper bound proof (%s) matches it.\n" % bound_type
165     elif best_nature == 'e':
166         dump += "<p>This dissection is believed optimal because it was found by an exhaustive search program, although the best upper bound proof (%s) gives an upper bound of %s.\n" % (bound_type, bound)
167         tdclass = "believed"
168         show_bound = ""
169     elif best_nature == 'p':
170         dump += "<p>This dissection was found by a search program which may not be exhaustive (if the conjectured denominator bound is false) and hence may not be optimal, though we think it <em>probably</em> is. The best upper bound proof (%s) gives an upper bound of %s.\n" % (bound_type, bound)
171     else:
172         dump += "<p>This dissection was found "
173         if best_nature == 'm':
174             dump += "by hand"
175         else:
176             dump += "by a simplistic automated method (%s)" % auto_reason
177         dump += ", and is not known to be optimal. The best upper bound proof (%s) gives an upper bound of %s.\n" % (bound_type, bound)
178
179     details[(n, m)] = dump
180
181     return ret
182
183 def main(args):
184     limit = 31 # FIXME: configurable
185
186     subst = {}
187
188     table = "<table>"
189     table += "<tr>\n"
190     table += "<th>n&nbsp;\\&nbsp;m</th>\n"
191     for m in range(2,limit-1):
192         table += "<th>%d</th>\n" % m
193     table += "</tr>\n"
194     for n in range(2,limit):
195         table += "<tr>\n"
196         table += "<th>%d</th>\n" % n
197         for m in range(2,n):
198             table += read_and_build_table_cell(n, m)
199         table += "</tr>\n"
200     table += "</table>\n"
201     subst["TABLE"] = table
202
203     subst["DISSECTIONS"] = "".join([data for ((n, m), data) in sorted(details.items())])
204
205     with open("template.html") as f:
206         for line in f:
207             if line[:1] == "%" and line[-2:] == "%\n":
208                 sys.stdout.write(subst[line[1:-2]])
209             else:
210                 sys.stdout.write(line)
211
212 if __name__ == "__main__":
213     main(sys.argv[1:])