Mystery Hunt is an annual puzzle hunt hosted at MIT during MLK weekend. At the first hunt I attended in person there was one puzzle in particular that grabbed my attention, Advisor’s Nightmare. While at the hunt we solved it using a smattering of ruby and prolog along with plenty of brute force pencil-and-paper. Since then I have spent time learning about modeling tools that are better suited for solving this type of problem. While learning Alloy I decided to revisit this puzzle.

Advisor’s Nightmare presents a series of increasingly obtuse constraints that a student must fulfill with their course selections in order to receive a degree in Modern Enigmatology. I modeled these constraints directly with Alloy with zero attempt to be clever. Once I fixed the syntax errors and hit go Alloy provided the desired schedule.

``````// The Advisor's Nightmare

open util/ordering[Time]
open util/ordering[Season]
open util/ordering[Year]

enum Time { pm1, pm2, pm3, pm4, pm5 }
enum Season { fall, winter, spring }
enum Year { y1, y2, y3, y4 }

enum Course {
engm102, engm115, engm128, engm145, engm156, engm176, engm180, engm199,
engm205, engm234, engm253, engm265, engm272, engm289,
engm308, engm332, engm343, engm344, engm361, engm373, engm390, engm397a, engm397b,
engm402, engm421, engm426, engm428, engm438, engm440, engm468, engm474, engm475,
engm504, engm512, engm516, engm530
}

sig Offering {
course: one Course,
time: one Time,
season: one Season,
year: one Year,
}

sig Schedule {
selection: set Offering
}

// Don't bother making more than one schedule since the puzzle requires a single schedule.
fact {
#Schedule = 1
}

pred Schedule.containsAllCourses [] {
all c : Course |
c in this.selection.course
}

pred Schedule.threeCoursePerTrimester [] {
all y : Year |
all s : Season |
#(this.selection & y.~year & s.~season) = 3
}

pred Schedule.disjointCourseTimes [] {
all y : Year |
all s : Season |
all t : Time |
lone (this.selection & y.~year & s.~season & t.~time)
}

pred Schedule.atMostOneSudokuSeminarPerTrimester [] {
all y : Year |
all s : Season |
lone (this.selection & y.~year & s.~season & ( engm402.~course
+ engm421.~course
+ engm426.~course
+ engm428.~course
+ engm438.~course
+ engm440.~course
+ engm468.~course
+ engm474.~course
+ engm475.~course
))
}

pred Schedule.atMostOneKonundrumKlassPerTrimester [] {
all y : Year |
all s : Season |
lone (this.selection & y.~year & s.~season & ( engm504.~course
+ engm512.~course
+ engm516.~course
+ engm530.~course
))
}

pred Schedule.allCoursesOnCalendar [] {
all o : this.selection | o.onCourseCalendar
}

pred wellFormed [s : Schedule] {
s.containsAllCourses
s.allCoursesOnCalendar
s.threeCoursePerTrimester
s.disjointCourseTimes
s.courseCatalogConstraints
s.atMostOneSudokuSeminarPerTrimester
s.atMostOneKonundrumKlassPerTrimester
}

pred Offering.sameTrimester [ other : Offering ] {
this.season = other.season && this.year = other.year
}

pred Offering.before [ other : Offering ] {
this.year in other.year.prevs || (this.year = other.year && this.season in other.season.prevs)
}

pred Offering.immediatelyBefore [ other : Offering ] {
(this.season = other.season.prev && this.year = other.year) ||
(this.season = spring && other.season = fall && this.year = other.year.prev)
}

pred Offering.immediatelyAfter [ other : Offering ] {
(this.season = other.season.next && this.year = other.year) ||
(this.season = fall && other.season = spring && this.year = other.year.next)
}

pred Offering.consecutive [ other : Offering ] {
this.immediatelyAfter [ other ] || this.immediatelyBefore [ other ]
}

pred Offering.immediatelyBeforeSudoku [] {
this.immediatelyBefore [ engm402.~course ]
|| this.immediatelyBefore [ engm421.~course ]
|| this.immediatelyBefore [ engm426.~course ]
|| this.immediatelyBefore [ engm428.~course ]
|| this.immediatelyBefore [ engm438.~course ]
|| this.immediatelyBefore [ engm440.~course ]
|| this.immediatelyBefore [ engm468.~course ]
|| this.immediatelyBefore [ engm474.~course ]
|| this.immediatelyBefore [ engm475.~course ]
}

pred Offering.immediatelyAfterSudoku [] {
this.immediatelyAfter [ engm402.~course ]
|| this.immediatelyAfter [ engm421.~course ]
|| this.immediatelyAfter [ engm426.~course ]
|| this.immediatelyAfter [ engm428.~course ]
|| this.immediatelyAfter [ engm438.~course ]
|| this.immediatelyAfter [ engm440.~course ]
|| this.immediatelyAfter [ engm468.~course ]
|| this.immediatelyAfter [ engm474.~course ]
|| this.immediatelyAfter [ engm475.~course ]
}

pred Offering.exactlyFiveTrimestersBefore [ other : Offering ] {
// NOTE: Brute-forced because I am still learning Alloy (specifically dealing with sequences and nested orderings)
(this.year = y1 && this.season = fall    && other.year = y2 && other.season = winter)
|| (this.year = y1 && this.season = winter  && other.year = y2 && other.season = spring)
|| (this.year = y1 && this.season = spring  && other.year = y3 && other.season = fall)
|| (this.year = y2 && this.season = fall    && other.year = y3 && other.season = winter)
|| (this.year = y2 && this.season = winter  && other.year = y3 && other.season = spring)
|| (this.year = y2 && this.season = spring  && other.year = y4 && other.season = fall)
|| (this.year = y3 && this.season = fall    && other.year = y4 && other.season = winter)
|| (this.year = y3 && this.season = winter  && other.year = y4 && other.season = spring)
}

pred Offering.atLeastNineTrimestersBefore [ other : Offering ] {
// NOTE: Brute-forced for the same reason as 'exactlyFiveTrimestersBefore'
(this.year = y1 && other.year = y4 && (
(this.season = fall   && other.season in (fall + winter + spring))
|| (this.season = winter && other.season in (       winter + spring))
|| (this.season = spring && other.season in (                spring))
))
}

pred courseCatalogConstraints [s : Schedule] {
// Seasonal requirements
engm102.~course.season in fall
not engm128.~course.season in spring
not engm145.~course.season in spring
engm199.~course.season in fall
not engm205.~course.season in fall
engm253.~course.season in winter
engm272.~course.season in fall
engm343.~course.season in spring
engm344.~course.season in winter
engm397a.~course.season in fall
engm397b.~course.season in fall
engm440.~course.season in winter
not engm474.~course.season in spring
engm475.~course.season in spring
engm504.~course.season in spring
engm512.~course.season in spring
engm516.~course.season in spring
engm530.~course.season in spring

// Same/Different trimesters
not engm115.~course.sameTrimester [ engm265.~course ]
engm205.~course.sameTrimester [ engm128.~course ]
engm308.~course.sameTrimester [ engm332.~course ]
engm390.~course.sameTrimester [ engm373.~course ]

engm421.~course.year = engm426.~course.year

// Prerequesites
engm530.~course.before [ engm253.~course ]
engm145.~course.before [ engm397a.~course ]
engm397a.~course.before [ engm397b.~course ]
engm234.~course.before [ engm180.~course ]
engm344.~course.before [ engm199.~course ]
engm530.~course.before [ engm253.~course ]
engm512.~course.before [ engm272.~course ]
engm199.~course.before [ engm343.~course ]
engm145.~course.before [ engm344.~course ]
engm516.~course.before [ engm397a.~course ]
engm516.~course.before [ engm397a.~course ]
engm402.~course.before [ engm428.~course ]

// Consecutive
engm115.~course.consecutive [ engm102.~course ]
engm156.~course.consecutive [ engm512.~course ]
engm265.~course.consecutive [ engm102.~course ]

// Immediately after
engm176.~course.immediatelyAfter [ engm438.~course ]

// Between two Sudoku Seminars
engm289.~course.immediatelyBeforeSudoku
engm289.~course.immediatelyAfterSudoku

// Not first trimester
not (engm373.~course.season in fall && engm373.~course.year in y1) // TODO: Turn this in to a function

engm438.~course.exactlyFiveTrimestersBefore [ engm468.~course ]
engm390.~course.atLeastNineTrimestersBefore [ engm361.~course ]
}

run { Schedule.wellFormed } for 36

// Note: This is a brute force approach to modeling the time slots since the puzzle
//       provides no guidance on time slots other than a large table.
pred Offering.onCourseCalendar [] {
(this.year = y1 && this.season = fall && (
(this.time = pm1 && this.course in (engm102 + engm156 + engm332 + engm397a + engm397b + engm474))
||  (this.time = pm2 && this.course in (engm176 + engm265 + engm289 + engm361 + engm373))
||  (this.time = pm3 && this.course in (engm145 + engm199 + engm390 + engm402 + engm438))
||  (this.time = pm4 && this.course in (engm115 + engm234 + engm308 + engm426 + engm428))
||  (this.time = pm5 && this.course in (engm128 + engm180 + engm272 + engm421 + engm468))
))

|| (this.year = y1 && this.season = winter && (
(this.time = pm1 && this.course in (engm308 + engm361 + engm402 + engm440 + engm468))
|| (this.time = pm2 && this.course in (engm128 + engm176 + engm253 + engm390 + engm474))
|| (this.time = pm3 && this.course in (engm156 + engm265 + engm344 + engm421 + engm428))
|| (this.time = pm4 && this.course in (engm205 + engm234 + engm289 + engm332 + engm438))
|| (this.time = pm5 && this.course in (engm115 + engm145 + engm180 + engm373 + engm426))
))

|| (this.year = y1 && this.season = spring && (
(this.time = pm1 && this.course in (engm176 + engm421 + engm428 + engm468 + engm475))
|| (this.time = pm2 && this.course in (engm156 + engm205 + engm373 + engm390 + engm402))
|| (this.time = pm3 && this.course in (engm289 + engm308 + engm361 + engm512 + engm530))
|| (this.time = pm4 && this.course in (engm115 + engm234 + engm343 + engm426 + engm516))
|| (this.time = pm5 && this.course in (engm180 + engm265 + engm332 + engm438 + engm504))
))

|| (this.year = y2 && this.season = fall && (
(this.time = pm1 && this.course in (engm115 + engm390 + engm397a + engm397b + engm426 + engm468))
|| (this.time = pm2 && this.course in (engm128 + engm156 + engm373 + engm428 + engm438))
|| (this.time = pm3 && this.course in (engm180 + engm199 + engm265 + engm361 + engm421))
|| (this.time = pm4 && this.course in (engm145 + engm234 + engm272 + engm289 + engm308))
|| (this.time = pm5 && this.course in (engm102 + engm176 + engm332 + engm402 + engm474))
))

|| (this.year = y2 && this.season = winter && (
(this.time = pm1 && this.course in (engm176 + engm361 + engm421 + engm426 + engm440))
|| (this.time = pm2 && this.course in (engm180 + engm205 + engm234 + engm332 + engm344))
|| (this.time = pm3 && this.course in (engm128 + engm156 + engm373 + engm390 + engm438))
|| (this.time = pm4 && this.course in (engm115 + engm145 + engm289 + engm402 + engm474))
|| (this.time = pm5 && this.course in (engm253 + engm265 + engm308 + engm428 + engm468))
))

|| (this.year = y2 && this.season = spring && (
(this.time = pm1 && this.course in (engm176 + engm361 + engm468 + engm512 + engm516))
|| (this.time = pm2 && this.course in (engm234 + engm265 + engm343 + engm438 + engm475))
|| (this.time = pm3 && this.course in (engm156 + engm205 + engm332 + engm421 + engm504))
|| (this.time = pm4 && this.course in (engm180 + engm308 + engm402 + engm426 + engm530))
|| (this.time = pm5 && this.course in (engm115 + engm289 + engm373 + engm390 + engm428))
))

|| (this.year = y3 && this.season = fall && (
(this.time = pm1 && this.course in (engm145 + engm199 + engm332 + engm390 + engm397a + engm397b))
|| (this.time = pm2 && this.course in (engm115 + engm265 + engm373 + engm426 + engm438))
|| (this.time = pm3 && this.course in (engm102 + engm128 + engm272 + engm421 + engm468))
|| (this.time = pm4 && this.course in (engm176 + engm180 + engm289 + engm308 + engm474))
|| (this.time = pm5 && this.course in (engm156 + engm234 + engm361 + engm402 + engm428))
))

|| (this.year = y3 && this.season = winter && (
(this.time = pm1 && this.course in (engm145 + engm156 + engm176 + engm361 + engm426))
|| (this.time = pm2 && this.course in (engm205 + engm253 + engm265 + engm440 + engm468))
|| (this.time = pm3 && this.course in (engm115 + engm289 + engm373 + engm428 + engm438))
|| (this.time = pm4 && this.course in (engm128 + engm332 + engm344 + engm421 + engm474))
|| (this.time = pm5 && this.course in (engm180 + engm234 + engm308 + engm390 + engm402))
))

|| (this.year = y3 && this.season = spring && (
(this.time = pm1 && this.course in (engm289 + engm308 + engm332 + engm343 + engm428))
|| (this.time = pm2 && this.course in (engm176 + engm361 + engm421 + engm426 + engm468))
|| (this.time = pm3 && this.course in (engm115 + engm205 + engm402 + engm438 + engm504))
|| (this.time = pm4 && this.course in (engm156 + engm180 + engm475 + engm512 + engm516))
|| (this.time = pm5 && this.course in (engm234 + engm265 + engm373 + engm390 + engm530))
))

|| (this.year = y4 && this.season = fall && (
(this.time = pm1 && this.course in (engm115 + engm289 + engm426 + engm438 + engm474))
|| (this.time = pm2 && this.course in (engm145 + engm156 + engm176 + engm421 + engm468))
|| (this.time = pm3 && this.course in (engm102 + engm128 + engm265 + engm332 + engm390))
|| (this.time = pm4 && this.course in (engm234 + engm308 + engm361 + engm397a + engm397b + engm428))
|| (this.time = pm5 && this.course in (engm180 + engm199 + engm272 + engm373 + engm402))
))

|| (this.year = y4 && this.season = winter && (
(this.time = pm1 && this.course in (engm176 + engm332 + engm344 + engm361 + engm474))
|| (this.time = pm2 && this.course in (engm205 + engm253 + engm289 + engm373 + engm421))
|| (this.time = pm3 && this.course in (engm115 + engm156 + engm180 + engm428 + engm468))
|| (this.time = pm4 && this.course in (engm145 + engm234 + engm426 + engm438 + engm440))
|| (this.time = pm5 && this.course in (engm128 + engm265 + engm308 + engm390 + engm402))
))

|| (this.year = y4 && this.season = spring && (
(this.time = pm1 && this.course in (engm308 + engm361 + engm390 + engm475 + engm504))
|| (this.time = pm2 && this.course in (engm180 + engm205 + engm234 + engm265 + engm530))
|| (this.time = pm3 && this.course in (engm176 + engm289 + engm343 + engm421 + engm438))
|| (this.time = pm4 && this.course in (engm332 + engm426 + engm428 + engm468 + engm516))
|| (this.time = pm5 && this.course in (engm115 + engm156 + engm373 + engm402 + engm512))
))
}

``````