Add new faculty constraints; prevent course section overlaps

Signed-off-by: Will Killian <william.killian@outlook.com>

Author: willkill07

docs/configuration.md

@@ -59,6 +59,8 @@ The configuration system uses several type aliases for validation:
         "maximum_credits": 12,
         "minimum_credits": 6,
         "unique_course_limit": 3,
+        "maximum_days": 4,
+        "mandatory_days": ["MON", "WED"],
         "times": {
           "MON": ["09:00-17:00"],
           "TUE": ["09:00-17:00"],
@@ -218,13 +220,17 @@ The configuration system uses several type aliases for validation:
 - **`maximum_credits`**: Maximum credit hours they can teach (required, non-negative integer)
 - **`minimum_credits`**: Minimum credit hours they must teach (required, non-negative integer)
 - **`unique_course_limit`**: Maximum number of different courses they can teach (required, positive integer)
+- **`maximum_days`**: Maximum number of distinct days they will teach (optional, defaults to 5)
+- **`mandatory_days`**: Set of days they must teach on (optional, defaults to empty)
 - **`times`**: Available time slots by day (required, non-empty dict)
 - **`course_preferences`**: Course preference scores (0-10, higher = more preferred, optional)
 - **`room_preferences`**: Room preference scores (0-10, higher = more preferred, optional)
 - **`lab_preferences`**: Lab preference scores (0-10, higher = more preferred, optional)
 
 **Validation Rules:**
 - `minimum_credits` cannot be greater than `maximum_credits`
+- `mandatory_days` must be a subset of the days listed in `times`
+- `maximum_days` must be greater than or equal to the number of `mandatory_days`
 - All course IDs in preferences must exist in the courses list
 - All room names in preferences must exist in the rooms list
 - All lab names in preferences must exist in the labs list
@@ -244,6 +250,8 @@ The configuration system uses several type aliases for validation:
 
 **Best Practices:**
 - Set realistic credit limits based on faculty workload
+- Use `maximum_days` to cap teaching days when faculty want compressed schedules
+- Reserve `mandatory_days` for commitments like standing department meetings or required course coverage
 - Use preference scores to guide optimization
 - Ensure availability times are accurate and comprehensive
 - Consider faculty expertise when assigning course preferences

example.json

@@ -27,6 +27,7 @@
             "maximum_credits": 12,
             "minimum_credits": 12,
             "unique_course_limit": 3,
+            "maximum_days": 4,
             "times": {
                 "MON": ["11:00-16:00"],
                 "TUE": [],
@@ -54,11 +55,13 @@
             "maximum_credits": 14,
             "minimum_credits": 12,
             "unique_course_limit": 2,
+            "maximum_days": 4,
+            "mandatory_days": ["MON", "WED", "FRI"],
             "times": {
                 "MON": ["09:00-15:00"],
                 "TUE": ["09:00-15:00"],
                 "WED": ["09:00-15:00"],
-                "THU": [],
+                "THU": ["09:00-15:00"],
                 "FRI": ["09:00-15:00"]
             },
             "course_preferences": {
@@ -80,9 +83,11 @@
             "maximum_credits": 8,
             "minimum_credits": 8,
             "unique_course_limit": 2,
+            "maximum_days": 4,
+            "mandatory_days": ["MON", "WED"],
             "times": {
                 "MON": ["09:00-13:00"],
-                "TUE": [],
+                "TUE": ["09:00-15:00"],
                 "WED": ["09:00-15:00"],
                 "THU": ["09:00-15:00"],
                 "FRI": ["09:00-15:00"]
@@ -106,11 +111,13 @@
             "maximum_credits": 12,
             "minimum_credits": 12,
             "unique_course_limit": 2,
+            "maximum_days": 4,
+            "mandatory_days": ["WED"],
             "times": {
                 "MON": ["09:00-15:00"],
                 "TUE": ["09:00-15:00"],
                 "WED": ["09:00-15:00"],
-                "THU": [],
+                "THU": ["09:00-15:00"],
                 "FRI": ["09:00-15:00"]
             },
             "course_preferences": {
@@ -207,11 +214,13 @@
             "maximum_credits": 12,
             "minimum_credits": 12,
             "unique_course_limit": 2,
+            "maximum_days": 4,
+            "mandatory_days": ["WED"],
             "times": {
                 "MON": ["09:00-17:00"],
                 "TUE": ["09:00-17:00"],
                 "WED": ["09:00-15:00"],
-                "THU": [],
+                "THU": ["09:00-17:00"],
                 "FRI": ["09:00-17:00"]
             },
             "course_preferences": {

src/scheduler/config.py

@@ -443,6 +443,17 @@ class FacultyConfig(StrictBaseModel):
     Maximum credit hours they can teach
     """
 
+    maximum_days: int = Field(
+        default=5,
+        ge=0,
+        le=5,
+        description="Maximum number of days they are willing to teach (0-5, optional)",
+        json_schema_extra={"example": 3},
+    )
+    """
+    Maximum number of days they are willing to teach (optional)
+    """
+
     minimum_credits: int = Field(
         description="Minimum credit hours they must teach", ge=0, json_schema_extra={"example": 3}
     )
@@ -493,6 +504,15 @@ class FacultyConfig(StrictBaseModel):
     Dictionary mapping `Lab` IDs to `Preference` scores
     """
 
+    mandatory_days: set[Day] = Field(
+        default_factory=set,
+        description="Set of days the faculty must teach on",
+        json_schema_extra={"example": ["MON", "WED"]},
+    )
+    """
+    Set of days the faculty must teach on
+    """
+
     @field_validator("times", mode="before")
     @classmethod
     def _convert_time_strings(cls, v):
@@ -511,6 +531,13 @@ def _convert_time_strings(cls, v):
             return converted
         return v
 
+    @field_validator("mandatory_days", mode="before")
+    @classmethod
+    def _convert_mandatory_days(cls, v):
+        if isinstance(v, list | tuple):
+            return set(v)
+        return v
+
     @model_validator(mode="after")
     def validate(self):
         """
@@ -521,6 +548,18 @@ def validate(self):
                 f"Minimum credits ({self.minimum_credits}) cannot be greater than "
                 f"maximum credits ({self.maximum_credits})"
             )
+        if self.maximum_days < len(self.mandatory_days):
+            raise ValueError(
+                f"maximum_days ({self.maximum_days}) cannot be less than the number of mandatory days "
+                f"({len(self.mandatory_days)})"
+            )
+        available_days = {day if isinstance(day, str) else str(day) for day in self.times}
+        mandatory_days = {day if isinstance(day, str) else str(day) for day in self.mandatory_days}
+        unavailable_mandatory = mandatory_days - available_days
+        if unavailable_mandatory:
+            raise ValueError(
+                f"Mandatory days {sorted(unavailable_mandatory)} must be present in the availability times"
+            )
         return self
 
 
@@ -565,9 +604,11 @@ class SchedulerConfig(StrictBaseModel):
                 {
                     "name": "Dr. Smith",
                     "maximum_credits": 12,
+                    "maximum_days": 3,
                     "minimum_credits": 3,
                     "unique_course_limit": 3,
                     "times": {"MON": ["10:00-12:00"], "TUE": ["10:00-12:00"]},
+                    "mandatory_days": ["MON"],
                     "course_preferences": {"CS 101": 5},
                     "room_preferences": {"Room 101": 5},
                     "lab_preferences": {"Lab 101": 5},

src/scheduler/scheduler.py

@@ -123,11 +123,15 @@ def _initialize_faculty_data(self, config) -> None:
             faculty_name = faculty_data.name
             self._faculty.add(faculty_name)
             self._faculty_maximum_credits[faculty_name] = faculty_data.maximum_credits
+            self._faculty_maximum_days[faculty_name] = faculty_data.maximum_days
             self._faculty_minimum_credits[faculty_name] = faculty_data.minimum_credits
             self._faculty_unique_course_limits[faculty_name] = faculty_data.unique_course_limit
             self._faculty_course_preferences[faculty_name] = faculty_data.course_preferences
             self._faculty_room_preferences[faculty_name] = faculty_data.room_preferences
             self._faculty_lab_preferences[faculty_name] = faculty_data.lab_preferences
+            self._faculty_mandatory_days[faculty_name] = {
+                day if isinstance(day, Day) else Day[day] for day in faculty_data.mandatory_days
+            }
             self._faculty_availability[faculty_name] = get_faculty_availability(faculty_data)
 
     def _initialize_courses(self, config) -> tuple[list[Course], set[int]]:
@@ -246,11 +250,13 @@ def __init__(self, full_config: CombinedConfig):
         # Initialize data structures
         self._faculty: set[str] = set()
         self._faculty_maximum_credits: dict[str, int] = dict()
+        self._faculty_maximum_days: dict[str, int] = dict()
         self._faculty_minimum_credits: dict[str, int] = dict()
         self._faculty_unique_course_limits: dict[str, int] = dict()
         self._faculty_course_preferences: dict[str, dict[str, int]] = dict()
         self._faculty_room_preferences: dict[str, dict[str, int]] = dict()
         self._faculty_lab_preferences: dict[str, dict[str, int]] = dict()
+        self._faculty_mandatory_days: dict[str, set[Day]] = dict()
         self._faculty_availability: dict[str, list[TimeInstance]] = dict()
         self._initialize_faculty_data(config)
 
@@ -326,8 +332,8 @@ def _z3ify_time_constraint(
         false: list[tuple[z3.BoolRef, z3.BoolRef]] = []
 
         for slot_i, slot_j in itertools.combinations_with_replacement(self._slots, 2):
-            c_i = z3_data.time_slot_constants[slot_i]
-            c_j = z3_data.time_slot_constants[slot_j]
+            c_i = cast(z3.BoolRef, z3_data.time_slot_constants[slot_i])
+            c_j = cast(z3.BoolRef, z3_data.time_slot_constants[slot_j])
             if self._cached_slot_relationship(name, slot_i, slot_j):
                 true.append((c_i, c_j))
                 true.append((c_j, c_i))
@@ -361,7 +367,7 @@ def _z3ify_time_slot_fn(
         true: list[z3.BoolRef] = []
         false: list[z3.BoolRef] = []
         for slot in self._slots:
-            c = z3_data.time_slot_constants[slot]
+            c = cast(z3.BoolRef, z3_data.time_slot_constants[slot])
             if fn(slot):
                 true.append(c)
             else:
@@ -388,9 +394,9 @@ def _z3ify_faculty_time_constraint(
             true: list[tuple[z3.BoolRef, z3.BoolRef]] = []
             false: list[tuple[z3.BoolRef, z3.BoolRef]] = []
             faculty_times = self._faculty_availability[faculty]
-            faculty_constant = z3_data.faculty_constants[faculty]
+            faculty_constant = cast(z3.BoolRef, z3_data.faculty_constants[faculty])
             for slot in self._slots:
-                slot_constant = z3_data.time_slot_constants[slot]
+                slot_constant = cast(z3.BoolRef, z3_data.time_slot_constants[slot])
                 if slot.in_time_ranges(faculty_times):
                     true.append((faculty_constant, slot_constant))
                 else:
@@ -463,11 +469,23 @@ def _build_faculty_constraints(self, z3_data: _Z3SortsAndConstants) -> list[z3.B
             for faculty in c.faculties:
                 faculty_course_map[faculty].append(c)
 
+        # Pre-compute time slot constants per day for reuse
+        day_slot_map: defaultdict[Day, set[z3.ExprRef]] = defaultdict(set)
+        for slot in self._slots:
+            slot_constant = z3_data.time_slot_constants[slot]
+            for time_instance in slot.times:
+                day_slot_map[time_instance.day].add(slot_constant)
+        day_to_slot_constants: dict[Day, tuple[z3.ExprRef, ...]] = {
+            day: tuple(slot_constants) for day, slot_constants in day_slot_map.items()
+        }
+
         # Add faculty credit and unique course limits - batch generation
         faculty_constraints: list[z3.BoolRef] = []
         for faculty in self._faculty:
             faculty_courses = faculty_course_map.get(faculty, [])
             faculty_constant = z3_data.faculty_constants[faculty]
+            max_days = self._faculty_maximum_days[faculty]
+            mandatory_days = self._faculty_mandatory_days[faculty]
             if faculty_courses:
                 min_credits = self._faculty_minimum_credits[faculty]
                 max_credits = self._faculty_maximum_credits[faculty]
@@ -505,6 +523,54 @@ def _build_faculty_constraints(self, z3_data: _Z3SortsAndConstants) -> list[z3.B
                     )
                     faculty_constraints.append(limit)
 
+            # Track whether the faculty teaches on a given day
+            day_indicator_map: dict[Day, z3.BoolRef] = {}
+            for day in Day:
+                slot_constants = day_to_slot_constants.get(day, ())
+                course_day_assignments: list[z3.BoolRef] = []
+                if slot_constants and faculty_courses:
+                    for course in faculty_courses:
+                        slot_matches = [course.time == slot_const for slot_const in slot_constants]
+                        if slot_matches:
+                            course_day_assignments.append(
+                                cast(
+                                    z3.BoolRef,
+                                    self._simplify(
+                                        z3.And(
+                                            course.faculty == faculty_constant,
+                                            z3.Or(slot_matches),
+                                        )
+                                    ),
+                                )
+                            )
+                if course_day_assignments:
+                    day_indicator_map[day] = cast(
+                        z3.BoolRef,
+                        self._simplify(z3.Or(course_day_assignments)),
+                    )
+                else:
+                    day_indicator_map[day] = z3.BoolVal(False, ctx=self._ctx)
+
+            # Maximum-day constraint
+            day_sum_terms = [z3.If(indicator, 1, 0) for indicator in day_indicator_map.values()]
+            day_sum = z3.Sum(day_sum_terms) if day_sum_terms else z3.IntVal(0, ctx=self._ctx)
+            faculty_constraints.append(
+                cast(
+                    z3.BoolRef,
+                    self._simplify(day_sum <= max_days),
+                )
+            )
+
+            # Mandatory-day constraints
+            for mandatory_day in mandatory_days:
+                indicator = day_indicator_map.get(mandatory_day, z3.BoolVal(False, ctx=self._ctx))
+                faculty_constraints.append(
+                    cast(
+                        z3.BoolRef,
+                        self._simplify(indicator),
+                    )
+                )
+
         return faculty_constraints
 
     def _build_course_constraints(
@@ -659,6 +725,10 @@ def _build_resource_constraints(
                     diff_course_constraints.append(z3.Not(lab_next_to(i.time, j.time)))
                 constraint_parts.append(cast(z3.BoolRef, z3.And(diff_course_constraints)))
 
+            if i.course_id == j.course_id:
+                # prevent overlapping times for different sections of the same course
+                resource_constraints.append(cast(z3.BoolRef, z3.Not(overlaps(i.time, j.time))))
+
             if resource:
                 # add all resource constraints (room, lab, etc.)
                 resource_constraints.append(cast(z3.BoolRef, z3.And(resource)))