raynoldng commented 7 years ago

Introduction

A feature many users of NUSMods will find useful would be a timetable planner that can output timetables from user supplied modules that fulfills certain requirements, such as:

having one or more free days (a day that has no lessons)
no lessons during particular timeslots (e.g. no morning lessons)
minimal travelling time
picking from a subset of modules (e.g. 7 pick 5) that fulfills the above constraints

These are problems that can be solved using constraint solver. Wei Heng and I are thinking of using z3, a theorem prover by Microsoft research to support the aforementioned features.

Constraint Solving

We managed to support the following queries:

Having one or more free days by picking m out n user supplied mods
Picking from a set of compulsory mods and optional mods

A CLI-based prototype is available at nusmods-planner

Internal Representation

We currently represent the timetable as hourly slots every 2 weeks (excluding weekends). This is equivalent to 24 5 2 = 240 slots. This is to account for lessons that are on alternating weeks. For example, a lecture that is from 8-10 every Monday would map to [8, 9, 128, 129].

Each module is represented by a Boolean selector variable, which is true in the model returned by z3 if its in the timetable. For each module, we extract its lesson types (lecture, tutorial, sectional, recitation etc.). Due to the fact that different modules have different lesson types, and each lesson type can have varying hours, we have (integer) variables for each contact hour (per fortnight) in the module. For example, a CS2020 tutorial with 4 hours every 2 weeks will have the variables CS2020_Tut0, ..., CS2020_Tut3. These variables will help us check for timetable clashes. We then have boolean selector variables CS2020_Tut_0, ..., CS2020_Tut_10 (exactly one of which will be true) to force the integer variables into the hours corresponding to the slot timing.

Free Day Queries

We shall discuss how the free day query is composed.

Consider the module CS1010 in AY16/17-S2:

{
  "ModuleCode": "CS1010",
  "ModuleTitle": "Programming Methodology",
  "Timetable": [
    {
      "ClassNo": "1",
      "LessonType": "Sectional Teaching",
      "WeekText": "Every Week",
      "DayText": "Tuesday",
      "StartTime": "1200",
      "EndTime": "1500",
      "Venue": "COM1-B109"
    },
    {
      "ClassNo": "1",
      "LessonType": "Tutorial",
      "WeekText": "Every Week",
      "DayText": "Friday",
      "StartTime": "1000",
      "EndTime": "1200",
      "Venue": "COM1-B108"
    },
    {
      "ClassNo": "2",
      "LessonType": "Tutorial",
      "WeekText": "Every Week",
      "DayText": "Friday",
      "StartTime": "1200",
      "EndTime": "1400",
      "Venue": "COM1-B108"
    },
    {
      "ClassNo": "3",
      "LessonType": "Tutorial",
      "WeekText": "Every Week",
      "DayText": "Friday",
      "StartTime": "1400",
      "EndTime": "1600",
      "Venue": "COM1-0120"
    }
  ]
}

We would have the following Boolean variables: CS1010_Sec_1, CS1010_Tut_1, CS1010_Tut_2, CS1010_Tut_3 And the time variables: CS1010_Sec0, ..., CS1010_Sec5, CS1010_Tut0, ..., CS1010_Tut3. In addition, we can only pick one of each lesson type.

We have the following implications and constraints:

Implies(CS1010_Sec_1, And(CS1010_Sec0 = 36, CS1010_Sec1 = 37,
                          CS1010_Sec2 = 37, CS1010_Sec3 = 156,
                          CS1010_Sec4 = 157, CS1010_Sec5 = 158))

Implies(CS1010_Tut_1, And(CS1010_Tut0 = 226, CS1010_Tut1 = 227,
                          CS1010_Tut2 = 106, CS1010_Tut3 = 107))

Implies(CS1010_Tut_2, And(CS1010_Tut0 = 230, CS1010_Tut1 = 231,
                          CS1010_Tut2 = 110, CS1010_Tut3 = 111))

Implies(CS1010_Tut_3, And(CS1010_Tut0 = 228, CS1010_Tut1 = 229,
                          CS1010_Tut2 = 108, CS1010_Tut3 = 109))
Or(CS1010_Sec_1)

Or(CS1010_Tut_1, CS1010_Tut_2, CS1010_Tut_3)

We do the same for the other mods and add the final constraint:

Or([Distinct([all time variables + hours in a weekday]) for all weekdays])

A timetable is valid if and only if all time assignments are distinct, i.e there are no clashes. We can check whether a free day can be accomodated by inserting the appropriate 24-hour blocks. For example, a timetable has a free day on Monday if and only if after insertion of range(0, 24)+range(120,144), the elements are still distinct. If such a satisfying assignment exists then we can print out the model and in turn a candidate timetable.

Geospatial Queries

Work in Progress

We have yet to decide on an internal representation for geospatial data. This is likely to require more advanced z3 functions such as iterative solving and fixed points that could increase execution time and load on server. If it provides infeasible to support we might have to drop this feature or use over approximations.

Timeline

Phase 1: z3 queries (3 weeks)

We hope to implement all the timetable queries and benchmark them so that it will overload the server when it is eventually deployed. Based on our rudimentary testing, one free day query with 9 mods (with workload 20 MC) takes about 1-2 seconds. We will also run tests to ensure that the proposed timetables are indeed correct.

Next, we intend to add geospatial-based querying as well. Timetable might not be feasible if it places lessons that are far from each other back to back. The exact implementation and data representation has not been confirmed but will most likely involve mapping all lesson locations to a NUS bus stop.

Phase 2: UI Design (3 weeks)

We will now need to expose these features through the NUSMods website. This will involve adding new routes, views and models. We will also have to put some restraints on user input. For instance, the user should not be able to query more than say 10 mods to avoid straining the server.

Phase 3: User feedback (3 weeks)

We can provide beta access to a small group of users to gauge the serve load and responsiveness of the web application and make changes if necessary.

Implementation Plan

Unfortunately, z3 does not have bindings for javascript. So we decided to use python to interface with z3. If time permits, we could redo the SMT-LIB query composition natively in javascript so that we only need query z3 using the command line.

The UI can be implemented by extending the current NUS Mods project. No news software stacks or frameworks should be necessary.

ngzhian commented 7 years ago

Currently we represent the timetable as a block of hours in 2 weeks (excluding weekdays). You mean weekends?

I would like the explanation of the variable names to be a bit more clear. Specifically, how do you get the name CS1010_Sec_1, and why are there CS1010_Sec0 to CS1010_Sec5, and where do you get the values from? (I know what they mean but I think the explanation can be clearer if you break it down into more steps)

We can model a free day is a whole day occupied with a arbitrary lesson. What do you mean by this? A free day is a day without any lessons isn't it?

one free day query with 6-8 mods takes about 2 seconds Feels a bit too long. I checked out your implementation query, I observe some nested OR/AND, which might or might not affect the speed. I would like to bring this down to << 1 eventually.

I suggest you rework the timeline a bit. UI/UX implementation can be interleaved with the backend implementation. You will likely need to tweak the UI/UX along the way as you get users to try the feature.

raynoldng commented 7 years ago

Currently we represent the timetable as a block of hours in 2 weeks (excluding weekdays). You mean weekends?

Yeah, oops. Changed the typo

We can model a free day is a whole day occupied with a arbitrary lesson. What do you mean by this? A free day is a day without any lessons isn't it?

Yeah. A free day is defined as a day that does not have any lessons. We can represent that constraint by adding a mock module that has one 24 hour (full day) lesson on any weekday once per week and querying z3 if we can obtain a valid timetable.

Feels a bit too long. I checked out your implementation query, I observe some nested OR/AND, which might or might not affect the speed. I would like to bring this down to << 1 eventually.

I am afraid that is how we pose the query using first order logic, there isn't anyway around it. We will do more profiling and maybe some z3 tweaks to optimize its search.

li-kai commented 7 years ago

Closing this since Orbital has ended. The project was very impressive and well done!

Project URL: http://modsplanner.tk

P.S. We welcome you guys to contribute back 🍡

yangshun commented 7 years ago

@li-kai 👍

nusmodifications / nusmods

Optimal Timetable Planning using constraint solving [1324] #390