MIT Mystery Hunt 2020 answers
Best Song Ever
The Best Song Ever puzzle was a .wav file of a recording of Disney’s “It’s A Small World”. Its data segment encoded a .jpg file which suggested how to proceed. See BestSongEver.nb for a Mathematica notebook which processed the data segment (it depends on tiny_planet.wav), or BestSongEver.pdf for a statically rendered PDF; see out.jpg for the extracted JPG.
The Story puzzle was a collection of rather incoherent paragraphs. Embedded in the page source was also a collection of very large integers, which turned out to have binary expansions that were of exactly the same length as their corresponding paragraph. Selecting the letters from the paragraph corresponding to 0-valued bits of the integers yielded a message which told us how to proceed.
The Nauseator puzzle started with a coloured nonogram.
See Nauseator.nb for a Mathematica notebook to parse out the data into structured form and shell out to
z3 to solve it, or Nauseator.pdf for a statically rendered PDF.
(The PDF has a very blurry image at the end, for some reason; see the actual image for full resolution.)
The input spreadsheet is nauseator.xlsx.
The notebook relies on Z3Interop.wl (static: Z3Interop.pdf), an extremely janky DSL to express SAT problems to send to the Z3 SAT solver. See the application to Sudoku and to nonograms, at Z3Interop.nb (static: Z3Interop.pdf).