[WIP] NUSMods Optimizer Prototyping

website/package.json

@@ -168,7 +168,8 @@
     "reselect": "4.0.0",
     "samlify": "^2.7.6",
     "searchkit": "2.4.1-alpha.5",
-    "use-subscription": "1.5.1"
+    "use-subscription": "1.5.1",
+    "worker-loader": "^3.0.8"
   },
   "browserslist": [
     "extends browserslist-config-nusmods"

website/src/actions/optimizer.ts

@@ -0,0 +1,7 @@
+export const TOGGLE_OPTIMIZER_DISPLAY = 'TOGGLE_OPTIMIZER_DISPLAY' as const;
+export function toggleOptimizerDisplay() {
+  return {
+    type: TOGGLE_OPTIMIZER_DISPLAY,
+    payload: null,
+  };
+}

website/src/reducers/index.ts

@@ -8,6 +8,7 @@ import { Actions } from 'types/actions';
 import requests from './requests';
 import app from './app';
 import createUndoReducer from './undoHistory';
+import optimizer from './optimizer';
 
 // Persisted reducers
 import moduleBankReducer, { persistConfig as moduleBankPersistConfig } from './moduleBank';
@@ -41,6 +42,7 @@ export default function reducers(state: State = defaultState, action: Actions):
     requests: requests(state.requests, action),
     timetables: timetables(state.timetables, action),
     app: app(state.app, action),
+    optimizer: optimizer(state.optimizer, action),
     theme: theme(state.theme, action),
     settings: settings(state.settings, action),
     planner: planner(state.planner, action),

website/src/reducers/optimizer.ts

@@ -0,0 +1,22 @@
+import { OptimizerState } from 'types/reducers';
+import { Actions } from 'types/actions';
+
+import { TOGGLE_OPTIMIZER_DISPLAY } from 'actions/optimizer';
+
+export const defaultOptimizerState: OptimizerState = {
+  isOptimizerShown: false,
+};
+
+function optimizer(state: OptimizerState = defaultOptimizerState, action: Actions): OptimizerState {
+  switch (action.type) {
+    case TOGGLE_OPTIMIZER_DISPLAY:
+      return {
+        ...state,
+        isOptimizerShown: !state.isOptimizerShown,
+      };
+    default:
+      return state;
+  }
+}
+
+export default optimizer;

website/src/types/optimizer.ts

@@ -0,0 +1,144 @@
+// Intermediate types used to contain timetable information relevant to the optimizer
+import { mapValues, groupBy } from 'lodash'
+import { Module, RawLesson } from 'types/modules'
+import { SemTimetableConfig } from 'types/timetables'
+
+// {module id}__{lesson type}__{lesson id} e.g., CS3203__Lecture__1
+export type UniqueLessonID = string;
+export type Z3LessonID = number;
+
+/**
+ * Main input format into the optimizer layers
+ * */
+export type OptimizerInput = {
+  moduleInfo: ModuleInfoWithConstraints[];
+  constraints: GlobalConstraints;
+}
+
+
+/**
+ * Callbacks to communicate with the caller of TimetableOptimizer
+ * */
+export interface OptimizerCallbacks {
+  onOptimizerInitialized: any;
+  onSmtlib2InputCreated(s: string): any;
+  onOutput(s: string): any;
+  // onTimetableOutput(timetable: TimetableOutput): any;
+  onTimetableOutput(timetable: OptimizerOutput): any;
+}
+
+/**
+ * Final timetable output to the optimizer caller
+ * */
+export type OptimizerOutput = SemTimetableConfig;
+
+/**
+ * Modules for optimizer to consider.
+ *  required is a constraint indicating if the module can be dropped to fulfil other constraints
+ * */
+export type ModuleInfoWithConstraints = {
+  mod: Module;
+  required: boolean;
+  lessonsGrouped: LessonsByGroupsByClassNo
+}
+
+// Mapping between lesson types -> classNo -> lessons.
+//  We have to take one classNo of each lessonType, so this indicates all the slots to be filled
+//    per classNo per lessonType
+export type LessonsByGroupsByClassNo = {
+    [lessonType: string]: { [classNo: string]: readonly RawLesson[] };
+}
+
+
+// User-selected constraints to pass to optimizer
+export interface GlobalConstraints {
+  // Min/max number of MCs + whether the constraint is active
+  workloadActive: boolean;
+  minWorkload: number;
+  maxWorkload: number;
+  // Find exactly N free days + whether the constraint is active
+  freeDayActive: boolean;
+  numRequiredFreeDays: number;
+  // Force these exact free days + whether the constraint is active
+  specificFreeDaysActive: boolean;
+  specificFreeDays: Array<string>;
+  // When lessons should start and end + whether the constraint is active
+  timeConstraintActive: boolean;
+  startTime: string;
+  endTime: string;
+  // The hours where a lunch break should be allocated,
+  //  how many half-hour slots to allocate, and whether the constraint is active
+  lunchStart: string;
+  lunchEnd: string;
+  lunchHalfHours: number;
+  lunchBreakActive: boolean;
+  // Ask optimizer to compact timetable to leave as few gaps between lessons as possible
+  preferCompactTimetable: boolean;
+}
+
+/**
+ * Defs for communicating between Optimizer <-> WebWorker <-> WASM wrapper
+ * */
+export enum Z3MessageKind {
+  // Request to init
+  INIT = 'INIT',
+  // Z3 initialized
+  INITIALIZED = 'INITIALIZED',
+  // Run the optimizer
+  OPTIMIZE = 'OPTIMIZE',
+  // Print output
+  PRINT = 'PRINT',
+  // Error
+  ERR = 'ERR',
+  // Z3 finished runnung
+  EXIT = 'EXIT',
+  // Z3 aborted
+  ABORT = 'ABORT',
+}
+
+/**
+ * Message to be sent back and forth between a Z3 webworker and any callers
+ * */
+export interface Z3Message {
+  kind: Z3MessageKind;
+  msg: string;
+}
+
+
+
+// TODO Shouldn't be here
+export const defaultConstraints: GlobalConstraints = {
+  workloadActive: false,
+  minWorkload: 0,
+  maxWorkload: 30,
+  freeDayActive: false,
+  numRequiredFreeDays: 1,
+  specificFreeDaysActive: false,
+  specificFreeDays: [],
+  startTime: '0800',
+  endTime: '2200',
+  lunchStart: '1100',
+  lunchEnd: '1500',
+  lunchHalfHours: 2,
+  lunchBreakActive: false,
+  timeConstraintActive: false,
+  preferCompactTimetable: false,
+};
+
+
+/**
+ * TODO move to utils
+ * Transforms a module's lessons into a mapping from
+ *  lessonType ==> (classNo ==> list of lessons)
+ * The optimizer cares that a classNo contains all the slots that should be filled.
+ * */
+export function lessonByGroupsByClassNo(lessons: readonly RawLesson[]): LessonsByGroupsByClassNo {
+  const lessonByGroups: { [lessonType: string]: readonly RawLesson[] } = groupBy(
+    lessons,
+    (lesson) => lesson.lessonType,
+  );
+  const lessonByGroupsByClassNo = mapValues(lessonByGroups, (lessonsOfSamelessonType: readonly RawLesson[]) =>
+    groupBy(lessonsOfSamelessonType, (lesson) => lesson.classNo),
+  );
+  return lessonByGroupsByClassNo;
+}

website/src/types/reducers.ts

@@ -83,6 +83,11 @@ export type ThemeState = Readonly<{
   showTitle: boolean;
 }>;
 
+/* optimizer */
+export type OptimizerState = Readonly<{
+  isOptimizerShown: boolean;
+}>;
+
 /* settings */
 export type ModRegRoundKey = { type: RegPeriodType; name?: string };
 

website/src/types/state.ts

@@ -4,6 +4,7 @@ import {
   Requests,
   SettingsState,
   ThemeState,
+  OptimizerState,
   TimetablesState,
   UndoHistoryState,
   VenueBank,
@@ -17,6 +18,7 @@ export type State = {
   timetables: TimetablesState;
   app: AppState;
   theme: ThemeState;
+  optimizer: OptimizerState;
   settings: SettingsState;
   planner: PlannerState;
   undoHistory: UndoHistoryState<State>;

website/src/utils/optimizer/timetableOptimizer.ts

@@ -0,0 +1,143 @@
+// import { TimetableOutput, TimetableSmtlib2Converter } from './timetable_to_smtlib2';
+import { OptimizerInputSmtlibConverter } from 'utils/optimizer/converter'
+import { OptimizerInput, OptimizerCallbacks, Z3Message, Z3MessageKind } from 'types/optimizer';
+import Z3WebWorker from 'worker-loader!utils/optimizer/z3WebWorker';
+
+import {
+    DAYS,
+    HOURS_PER_DAY,
+    DAY_START_HOUR,
+    DAY_END_HOUR,
+    NUM_WEEKS,
+    HOURS_PER_WEEK,
+} from 'utils/optimizer/constants'
+/**
+ * The TimetableOptimizer takes a generic timetable as input and manages the lifecycle of running the
+ * Z3 system to find a timetable solution.
+ * Runs the web worker, receives input/output, communicates through callbacks to the calling class.
+ *
+ * Only one TimetableOptimizer per application - allows stateless components to run manager methods
+ * */
+export class TimetableOptimizer {
+  static optInput: OptimizerInput;
+  static converter: OptimizerInputSmtlibConverter;
+  static smtString: string;
+  static callbacks: OptimizerCallbacks;
+  static printBuffer: string;
+  static errBuffer: string;
+  static worker?: Z3WebWorker = null;
+  static completedStage1Solve: boolean; // Need to complete week-solving before timetable-solving
+
+  static initOptimizer(callbacks: OptimizerCallbacks) {
+    console.log("Starting to initialize Z3...")
+    TimetableOptimizer.callbacks = callbacks;
+    TimetableOptimizer.resetBuffers();
+    TimetableOptimizer.completedStage1Solve = false;
+    // Set up worker if it's not set up
+    if (!TimetableOptimizer.worker) {
+      TimetableOptimizer.worker = new Z3WebWorker();
+      TimetableOptimizer.worker.onmessage = TimetableOptimizer.receiveWorkerMessage;
+    }
+    TimetableOptimizer.managerPostMessage(Z3MessageKind.INIT, '');
+  }
+
+  /**
+   * Register a generic timetable a set of callbacks to be called for different states in the Z3 solver lifecycle
+   * */
+  static loadTimetable(optInput: OptimizerInput) {
+      console.log('Loaded optimizer input');
+      console.log(optInput);
+      TimetableOptimizer.optInput = optInput;
+      TimetableOptimizer.converter = new OptimizerInputSmtlibConverter(
+          TimetableOptimizer.optInput,
+          NUM_WEEKS * HOURS_PER_WEEK * 2, // Number of "half-hour" slots
+          DAY_START_HOUR, // Start at 0800 (8 am)
+          DAY_END_HOUR /// End at 2200 (10 pm)
+      );
+  }
+
+  static solve() {
+      TimetableOptimizer.resetBuffers();
+      const weekSolveStr = TimetableOptimizer.converter.generateWeekSolveSmtLib2String();
+      TimetableOptimizer.managerPostMessage(Z3MessageKind.OPTIMIZE, weekSolveStr);
+  }
+
+  static receiveWorkerMessage(e: any) {
+    const message: Z3Message = e.data;
+    // console.log("Kind: %s, Message: %s", message.kind, message.msg)
+    switch (message.kind) {
+      case Z3MessageKind.INITIALIZED:
+        // Call the initialization callback
+        console.log("Manager initialized Z3!")
+        TimetableOptimizer.callbacks.onOptimizerInitialized();
+        break;
+      // case Z3MessageKind.PRINT:
+      //     TimetableOptimizer.printBuffer += message.msg + '\n';
+      //     break;
+      // case Z3MessageKind.ERR:
+      //     TimetableOptimizer.errBuffer += message.msg + '\n';
+      //     break;
+      // case Z3MessageKind.EXIT:
+      //     // Z3 Initialization exit
+      //     console.log('Z3 messages on exit: ');
+      //     if (TimetableOptimizer.printBuffer === '' && TimetableOptimizer.errBuffer === '') {
+      //         console.log('Premature exit - Z3 was initializing (this is normal)');
+      //         return; // Premature exit (probably initialization)
+      //     }
+
+      //     // Print buffers generically
+      //     if (TimetableOptimizer.printBuffer !== '') {
+      //         console.log(TimetableOptimizer.printBuffer);
+      //     }
+      //     if (TimetableOptimizer.errBuffer !== '') {
+      //         console.error(TimetableOptimizer.errBuffer);
+      //     }
+
+      //     if (!TimetableOptimizer.completedStage1Solve) {
+      //         // Indicate that next time we call this callback, we have the timetable result
+      //         TimetableOptimizer.completedStage1Solve = true;
+      //         // Update the converter with the week-solve result
+      //         // TODO: enable
+      //         TimetableOptimizer.conv.update_z3_weeksolve_output(TimetableOptimizer.printBuffer);
+      //         // Generate the SMTLIB2 string based on the week-solve:w
+      //         TimetableOptimizer.smtString = TimetableOptimizer.conv.generateTimetableSolveSmtLib2String();
+      //         // Run callback to update the generated smtlib2 string
+      //         TimetableOptimizer.callbacks.onSmtlib2InputCreated(TimetableOptimizer.smtString);
+      //         // Reset state for our next optimization run
+      //         TimetableOptimizer.resetBuffers();
+      //         // Two stage solve: first solve for the week constraints, then solve for the actual timetable
+      //         TimetableOptimizer.managerPostMessage(Z3MessageKind.OPTIMIZE, TimetableOptimizer.smtString);
+      //     } else {
+      //         // Reset solve state
+      //         TimetableOptimizer.completedStage1Solve = false;
+      //         // Deal with real solve state
+      //         // Call the output callback
+      //         TimetableOptimizer.callbacks.onOutput(
+      //             TimetableOptimizer.printBuffer + '\n' + TimetableOptimizer.errBuffer
+      //         );
+      //         // Process the output text we just got from the Z3 solver
+      //         const timetable: TimetableOutput = TimetableOptimizer.conv.z3_output_to_timetable(
+      //             TimetableOptimizer.printBuffer
+      //         );
+      //         TimetableOptimizer.callbacks.onTimetableOutput(timetable);
+      //     }
+
+      //     break;
+      default:
+        break;
+    }
+  }
+
+  /**
+   * Generically post a message to the worker
+   * */
+  static managerPostMessage(kind: Z3MessageKind, msg: string) {
+    const message: Z3Message = { kind, msg };
+    TimetableOptimizer.worker.postMessage(message);
+  }
+
+  static resetBuffers() {
+    TimetableOptimizer.printBuffer = '';
+    TimetableOptimizer.errBuffer = '';
+  }
+}