Lịch lặp theo tuần và ngoại lệ học bù trong ASP

1. Hai lớp cùng ca có thể vẫn không xung đột

Một thời khóa biểu học kỳ thường được hiển thị bằng thứ trong tuần và giờ học. Nhưng hai lớp có cùng thứ, giờ và phòng chưa chắc chồng nhau nếu chúng xuất hiện ở các tuần khác nhau. Ngược lại, một buổi học bù có thể tạo xung đột mà bản lịch tuần mẫu không thể hiện. Nếu mô hình chỉ giữ ca học mà không biểu diễn tuần hoạt động, nó có thể loại quá nhiều phương án hoặc bỏ sót xung đột của tuần ngoại lệ.

Ví dụ gồm bốn tuần, ba lớp A, B, C và một nguồn lực dùng chung. A xuất hiện mọi tuần. B học tuần lẻ 1 và 3. C học tuần chẵn 2 và 4. Mỗi lớp chọn một ca cố định cho cả đợt học. Có hai ca không chồng nhau. Vì B và C không cùng xuất hiện ở tuần nào, chúng có thể dùng chung ca. A phải chọn ca còn lại. Đây là mô hình nhỏ để nghiên cứu phép giao tập tuần, chưa phải định dạng đầy đủ của một bộ đối sánh.

2. Chuẩn hóa lịch lặp thành các lần xuất hiện

Ta tách lịch chuẩn, danh sách hủy và danh sách bổ sung. Quan hệ standard(L,W) ghi nhận lớp L có lịch chuẩn ở tuần W. Một lần xuất hiện chuẩn được giữ khi không có cancelled(L,W). Quan hệ extra(L,W) bổ sung một lần xuất hiện hợp lệ. Sau khi hợp nhất, mọi ràng buộc xung đột chỉ đọc occurs(L,W), giúp tránh mỗi ràng buộc tự diễn giải tuần lẻ, tuần chẵn và ngoại lệ theo cách khác nhau.

occurs(L,W) :- standard(L,W), not cancelled(L,W).
occurs(L,W) :- extra(L,W), course(L), week(W).

Trong hai luật này, bổ sung được phép làm một lớp xuất hiện dù cùng cặp lớp–tuần có trong danh sách hủy. Đây là chính sách hợp nhất của ví dụ. Nếu nghiệp vụ quy định hủy có ưu tiên cao hơn mọi bổ sung, cần sửa luật thứ hai hoặc kiểm tra đầu vào mâu thuẫn. Khi lưu ngoại lệ thực, nên có mã buổi và nguồn quyết định để không đánh đồng hủy một buổi với hủy mọi buổi của lớp trong tuần đó.

3. Điều kiện xung đột gồm cả ca và tuần chung

Hai lớp L và M bị cấm cùng ca khi có ít nhất một tuần W mà cả hai xuất hiện và chúng tranh cùng nguồn lực. Với ví dụ chỉ có một nguồn lực chung, điều kiện tài nguyên được hiểu ngầm cho mọi cặp. Ràng buộc ASP nối hai phép gán cùng S với hai fact occurs có chung W. Điều kiện L < M chỉ dùng để xét mỗi cặp một lần, không phải quan hệ ưu tiên giữa hai lớp.

:- at(L,S), at(M,S), L < M, occurs(L,W), occurs(M,W).

Về tập hợp, một cặp có xung đột tuần khi weeks(L) ∩ weeks(M) không rỗng. A giao với B và C, còn B không giao C trong lịch chuẩn. Do đó đồ thị xung đột là hai cạnh A–B, A–C và có hai cách gán hai ca. Cả hai nghiệm đều cho B và C cùng ca. Nếu viết ràng buộc chỉ dựa vào at(L,S), at(M,S), ta đã biến đồ thị đó thành tam giác và kết luận sai rằng hai ca là không đủ.

4. Một buổi học bù thay đổi tính khả thi ra sao?

Thêm cancelled(b,3). và extra(b,2). khiến B và C cùng xuất hiện ở tuần 2. Cạnh B–C được thêm vào. Lúc này cả ba cặp đều xung đột, nên hai ca không đủ. Nếu cho ba ca, ba lớp cần nhận ba ca khác nhau và có sáu hoán vị. Kết luận này đến từ tập tuần sau hợp nhất, không đến từ việc số học phần hay số buổi trung bình trong học kỳ tăng lên.

Đây cũng là một phản ví dụ cho việc chỉ kiểm tra tải trung bình theo tuần. Chuyển một buổi từ tuần 3 sang tuần 2 giữ nguyên tổng số buổi của B, nhưng dồn thêm tranh chấp vào tuần 2. Một chỉ số tổng hợp bằng nhau không bảo đảm tập lịch khả thi bằng nhau. Khi báo cáo, cần giữ các tuần giao nhau hoặc ít nhất các lớp xung đột được suy ra từ chúng.

5. Chạy ASP và so với phép giao tập trong Python

Cài python -m pip install "clingo==5.8.3" rồi chạy python asp_lich_lap_theo_tuan.py. Python sinh mọi bộ ba ca, kiểm tra giao tập tuần và giữ các lịch không xung đột. Kết quả này được đối chiếu với toàn bộ nghiệm ASP ở lịch chuẩn, lịch ngoại lệ hai ca và lịch ngoại lệ ba ca.

"""Một ca cố định cho mỗi lớp, xung đột xét trên tuần xuất hiện thực tế."""
from itertools import product
import clingo

PROGRAM = r"""
#const k=2.
week(1..4). course(a;b;c). slot(1..k).
standard(a,W) :- week(W).
standard(b,W) :- week(W), W\2 = 1.
standard(c,W) :- week(W), W\2 = 0.
occurs(L,W) :- standard(L,W), not cancelled(L,W).
occurs(L,W) :- extra(L,W), course(L), week(W).
1 { at(L,S) : slot(S) } 1 :- course(L).
:- at(L,S), at(M,S), L < M, occurs(L,W), occurs(M,W).
#show at/2.
"""

def schedules(extra="", slots=2):
    ctl = clingo.Control(["0", "--warn=none", "-c", f"k={slots}"])
    ctl.add("base", [], PROGRAM + extra)
    ctl.ground([("base", [])])
    result = set()
    def collect(model):
        mapping = {str(a.arguments[0]): a.arguments[1].number
                   for a in model.symbols(shown=True)}
        result.add(tuple(mapping[l] for l in ("a", "b", "c")))
    state = ctl.solve(on_model=collect)
    assert state.exhausted and not state.interrupted
    return result

def oracle(weeks, slots):
    return {x for x in product(range(1, slots+1), repeat=3)
            if all(x[i] != x[j] or not (weeks[i] & weeks[j])
                   for i in range(3) for j in range(i+1, 3))}

normal = ({1, 2, 3, 4}, {1, 3}, {2, 4})
changed = ({1, 2, 3, 4}, {1, 2}, {2, 4})
exception = "cancelled(b,3). extra(b,2)."
assert schedules() == oracle(normal, 2) == {(1, 2, 2), (2, 1, 1)}
assert schedules(exception) == oracle(changed, 2) == set()
assert schedules(exception, 3) == oracle(changed, 3)
assert len(schedules(exception, 3)) == 6
print("Lịch thường: 2 phương án.")
print("Chuyển buổi B từ tuần 3 sang tuần 2: vô nghiệm với 2 ca.")
print("Cho 3 ca: 6 phương án.")

Kết quả lần lượt là 2, 0 và 6 phương án. Mẫu chủ động giới hạn số tuần, số lớp và số ca để có thể kiểm tra trọn miền. Việc hai cách tính đồng ý trên dữ liệu này là bằng chứng cho ví dụ, chưa phải chứng minh mọi mô hình lịch tuần đều đúng. Khi mở rộng dữ liệu, vẫn cần lập luận về từng quy tắc hợp nhất và thêm ca biên ở đầu, cuối học kỳ.

6. Ca cố định cả học kỳ khác ca riêng từng tuần

Biến quyết định trong bài là at(L,S), vì vậy một lớp có cùng ca ở mọi tuần nó xuất hiện. Nếu dùng at(L,W,S) và chọn ca riêng cho từng tuần, miền phương án sẽ rộng hơn. Khi đó có thể sửa tuần 2 mà không di chuyển các tuần còn lại, nhưng lịch khó nhớ hơn và cần thêm tiêu chí hạn chế số lần đổi ca. Không nên so hai mô hình này như thể chúng mô tả cùng một chính sách ổn định lịch.

Ví dụ cũng chỉ cho mỗi lớp tối đa một lần xuất hiện trong một tuần. Với lý thuyết và thực hành tách buổi, cần mã buổi hoặc mã mẫu hoạt động. Hai buổi cùng lớp, cùng tuần không được gộp thành một fact nếu chúng cần hai quyết định khác nhau. Khi có ngày nghỉ, nên ánh xạ tuần và thứ sang ngày thực, rồi quyết định xử lý ngoại lệ trên ngày, không chỉ dựa vào tính chẵn lẻ của số tuần.

7. Thiết kế câu hỏi nghiên cứu theo mật độ giao tuần

Giữ số lớp và số phòng cố định, thay tỷ lệ lớp học cả kỳ, học tuần lẻ và học theo khối tuần. Sau đó thêm có kiểm soát các buổi học bù và đo số cạnh xung đột mới, số lịch giữ được, thời gian tìm phương án và số lớp phải đổi ca. Tách dữ liệu dùng điều chỉnh phương pháp khỏi dữ liệu kiểm tra cuối; không chọn riêng những ngoại lệ thuận lợi cho một mã hóa.

Bài tập: giữ hai ca nhưng cho phép B đổi ca riêng ở tuần 2, các tuần khác giữ ca cũ. Kiểm tra liệu chỉ đổi ca của B có đủ để có lịch hay không; dùng ba buổi cùng xuất hiện ở tuần 2 để lập luận. Sau đó đề xuất thêm ca, thêm nguồn lực hoặc chuyển tuần. Tiếp theo, cho buổi học bù cần một phòng khác cơ sở và nối thêm ràng buộc di chuyển. So sánh sửa theo tuần với sửa cả mẫu ca của B bằng số lần đổi ca và thông báo mà sinh viên phải nhận.

Nguồn cú pháp và biến điều khiển: Potassco Guide dòng Clingo 5. Liên hệ Thời gian di chuyển theo thời điểm thực và Sửa lịch đã công bố với ít xáo trộn.