Tìm một nhóm ràng buộc giải thích lịch vô nghiệm

1. Gắn mã cho từng điều kiện có thể giải thích

Một khoa có hai lớp A, B và một phòng chuyên dụng. Có ba ca sáng thứ Hai, thứ Tư và thứ Sáu. Hai yêu cầu cố định cùng ghim A và B vào thứ Hai, trong khi phòng chỉ chứa một lớp mỗi ca. Một yêu cầu khác cấm A vào thứ Sáu. Khi bộ giải trả vô nghiệm, người điều chỉnh lịch cần biết nhóm yêu cầu nào gây xung đột.

2. Thử bỏ từng điều kiện và dùng bộ kiểm tra khả thi

Giả sử tập điều kiện hiện tại vô nghiệm. Chọn một điều kiện và thử giải khi bỏ điều kiện đó. Nếu bài toán vẫn vô nghiệm, điều kiện vừa bỏ không cần có trong nhóm đang tìm. Nếu bài toán có nghiệm, giữ lại điều kiện. Lặp cho đến khi đã xét mọi điều kiện.

Vì đây là phép thử trên một miền lịch cố định, bỏ điều kiện chỉ mở rộng tập lịch có thể chọn. Nếu bỏ một điều kiện từng làm xuất hiện nghiệm, tiếp tục nới các điều kiện khác sẽ không làm mất nghiệm đó. Vì vậy kết quả là tối tiểu theo bao hàm. Bỏ bất kỳ phần tử nào khỏi nhóm còn lại đều làm nhóm đó khả thi. Tập tìm được có thể khác khi đổi thứ tự thử và chưa chắc có ít phần tử nhất trong tất cả các nhóm xung đột.

"""Tìm một tập vô nghiệm tối tiểu theo bao hàm trên ví dụ nhỏ."""
from itertools import product


CAC_CA = ("t2", "t4", "t6")
CAC_LICH = tuple(product(CAC_CA, repeat=2))
QUY_TAC = {
    "G1": lambda a, b: a == "t2",  # Lớp A phải học thứ Hai.
    "G2": lambda a, b: b == "t2",  # Lớp B phải học thứ Hai.
    "G3": lambda a, b: a != b,     # Hai lớp dùng chung một phòng.
    "G4": lambda a, b: a != "t6",  # A không học thứ Sáu.
}


def tim_lich(gia_dinh):
    return next((lich for lich in CAC_LICH
                 if all(QUY_TAC[key](*lich) for key in gia_dinh)), None)


def tap_xung_dot(gia_dinh):
    hien_tai = list(gia_dinh)
    if tim_lich(hien_tai) is not None:
        return None
    for key in list(hien_tai):
        thu = [rule for rule in hien_tai if rule != key]
        if tim_lich(thu) is None:
            hien_tai = thu
    return hien_tai


if __name__ == "__main__":
    core = tap_xung_dot(QUY_TAC)
    print("Nhóm gây vô nghiệm:", core)
    assert core == ["G1", "G2", "G3"]
    for key in core:
        chung = tim_lich([rule for rule in core if rule != key])
        print(f"Nới {key}, lịch làm chứng (A, B):", chung)
        assert chung is not None
    assert tap_xung_dot(["G1", "G3", "G4"]) is None

3. Đọc nhóm xung đột cùng các lịch làm chứng

Chạy python giai_thich_vo_nghiem.py. Mã duyệt chín cặp ca cho hai lớp. Kết quả giữ G1, G2 và G3. Sau đó chương trình lần lượt nới từng điều kiện trong nhóm và in một lịch làm chứng. Khi nới G1, A có thể sang thứ Tư. Khi nới G2, B có thể sang thứ Tư. Nếu bỏ G3, hai lớp có thể cùng thứ Hai trong mô hình đã nới.

Ví dụ cuối chỉ giải thích vai trò của G3. Nếu phòng thực tế chỉ chứa một lớp, cần xử lý nghiệp vụ bằng đổi ca hoặc cấp thêm phòng phù hợp. Các lịch làm chứng được kiểm tra trên nhóm xung đột đã nới, vì vậy khi đưa ra phương án thật phải kiểm tra lại toàn bộ điều kiện còn áp dụng.

4. Mở rộng sang bộ giải và dữ liệu thực tế

Với hàng nghìn lớp, dùng bộ giải làm hàm kiểm tra thay cho vét cạn. Mỗi điều kiện nghiệp vụ cần liên kết được với mã, dữ liệu nguồn và thông báo. Nếu bộ giải có thể trả về một tập giả định đủ gây vô nghiệm, có thể thu hẹp tiếp bằng các lần bỏ từng giả định. Khi hết thời gian mà chưa xác định được tính khả thi, hãy ghi kết quả là chưa kết luận và giữ điều kiện trong nhóm đang xét.

Câu hỏi nghiên cứu. Nên gộp giả định theo quy tắc, theo phòng, hay theo từng lớp? Nhóm thô dễ trình bày nhưng khó chỉ ra dữ liệu cần sửa. Nhóm chi tiết giúp truy vết tới dòng dữ liệu, song có thể tăng thời gian kiểm tra và làm báo cáo dài. Có thể so sánh hai cách theo kích thước nhóm, thời gian và khả năng giúp người dùng tìm phương án sửa.