Thiết kế thực nghiệm so sánh ASP, CP, SAT/MaxSAT và MIP

1. Đặt câu hỏi trước khi chọn chỉ số

Một bộ giải có thể tìm được lịch khả thi sớm, trong khi bộ giải khác cải thiện chất lượng nhiều hơn về cuối. Một con số tổng hợp khó giải thích được cả hai hành vi. Hãy đặt câu hỏi đo được. Trong cùng 60 giây, mỗi phương pháp tìm được lịch hợp lệ ở bao nhiêu trường hợp? Trên những trường hợp cả hai đều giải được, điểm phạt thay đổi bao nhiêu? Phương pháp nào có thể chứng minh tối ưu hoặc vô nghiệm?

ASP, CP, SAT/MaxSAT và MIP là các hướng đối sánh. Mỗi hướng cần cách biểu diễn riêng, nhưng phải dùng cùng dữ liệu, ràng buộc và mục tiêu đã chốt. Nếu SAT thuần được gọi nhiều lần theo ngưỡng điểm để giải bài toán tối ưu, thời gian của toàn bộ chuỗi gọi cần nằm trong ngân sách chung.

2. Khóa dữ liệu, quy tắc và ngân sách chạy

1. Dùng tập phát triển để sửa mô hình, điều chỉnh tham số và thử các cách mã hóa. Chốt giao thức rồi mới dùng tập độc lập để đánh giá cuối.
2. Ghi phiên bản bộ giải, cấu hình, tài nguyên, giới hạn thời gian, số lần lặp và seed nếu bộ giải có sử dụng. Quy định trước thời gian nạp dữ liệu, tiền xử lý và grounding có nằm trong ngân sách hay không.
3. Xuất nghiệm về cùng một định dạng và kiểm tra bằng một bộ kiểm chứng độc lập. Dùng cùng cách tính điểm, giữ log nguyên gốc và ghi trạng thái dừng cho từng lượt.

ITC 2007 Track 3 dùng mô hình thời khóa biểu theo chương trình đào tạo. ITC 2019 kết hợp gán ca–phòng với phân sinh viên vào các lớp theo nhu cầu môn học. Hãy đối chiếu từng bộ với câu hỏi nghiên cứu và phân tích theo từng bộ. Hai điểm phạt chỉ có nghĩa khi được đọc theo cùng đặc tả và cách tính.

3. Báo cáo hai mẫu số và phân biệt trạng thái dừng

Tỷ lệ tìm được lịch hợp lệ dùng tổng số lượt đã lên kế hoạch làm mẫu số. So sánh điểm giữa hai phương pháp chỉ dùng những lượt ghép cặp mà cả hai đều có lịch hợp lệ, với cùng instance và số thứ tự lặp. Cần báo cả số cặp còn lại. Một kết quả dừng vì hết thời gian vẫn có thể có lịch hợp lệ, nhưng chưa chắc đã chứng minh tối ưu. Dừng mà chưa có nghiệm khác với chứng minh vô nghiệm.

"""Báo cáo minh họa bằng dữ liệu giả lập. Điểm nhỏ hơn là tốt hơn."""
from collections import Counter
from dataclasses import dataclass
from statistics import median


@dataclass(frozen=True)
class LuotChay:
    phuong_phap: str
    instance: str
    lap: int
    trang_thai: str
    hop_le: bool
    diem: int | None
    giay_co_nghiem_dau: float | None


DU_LIEU_MO_PHONG = [
    LuotChay("ASP", "I01", 1, "optimal", True, 10, 1.0),
    LuotChay("ASP", "I02", 1, "time_limit", True, 18, 5.0),
    LuotChay("CP", "I01", 1, "optimal", True, 10, 2.0),
    LuotChay("CP", "I02", 1, "time_limit", False, None, None),
    LuotChay("SAT/MaxSAT", "I01", 1, "time_limit", True, 12, 2.5),
    LuotChay("SAT/MaxSAT", "I02", 1, "time_limit", True, 15, 8.0),
    LuotChay("MIP", "I01", 1, "optimal", True, 10, 1.5),
    LuotChay("MIP", "I02", 1, "invalid", False, None, None),
]


def da_kiem_chung(run):
    return run.hop_le and run.diem is not None


def bao_cao(rows, danh_sach_phuong_phap, ke_hoach):
    """ke_hoach chứa mọi cặp (instance, lần lặp) đã lên lịch."""
    index = {}
    for run in rows:
        key = (run.phuong_phap, run.instance, run.lap)
        if key in index:
            raise ValueError(f"Trùng lượt chạy: {key}")
        if run.phuong_phap not in danh_sach_phuong_phap or (run.instance, run.lap) not in ke_hoach:
            raise ValueError(f"Lượt nằm ngoài kế hoạch: {key}")
        index[key] = run

    diem_hop_le = {}
    for pp in danh_sach_phuong_phap:
        found = {(i, lap): index[pp, i, lap] for i, lap in ke_hoach if (pp, i, lap) in index}
        valid = {key: run for key, run in found.items() if da_kiem_chung(run)}
        times = [run.giay_co_nghiem_dau for run in valid.values() if run.giay_co_nghiem_dau is not None]
        median_s = median(times) if times else None
        statuses = dict(sorted(Counter(run.trang_thai for run in found.values()).items()))
        print(pp, f"lịch hợp lệ {len(valid)}/{len(ke_hoach)}",
              f"| thiếu log {len(ke_hoach) - len(found)}",
              "| trung vị giây đến lịch đầu:", median_s,
              "| trạng thái:", statuses)
        diem_hop_le[pp] = {key: run.diem for key, run in valid.items()}
    return diem_hop_le


def so_sanh_cap(a, b):
    common = a.keys() & b.keys()
    hon = sum(a[key] < b[key] for key in common)
    bang = sum(a[key] == b[key] for key in common)
    return len(common), hon, bang, len(common) - hon - bang


if __name__ == "__main__":
    scores = bao_cao(DU_LIEU_MO_PHONG, ["ASP", "CP", "SAT/MaxSAT", "MIP"],
                     {("I01", 1), ("I02", 1)})
    result = so_sanh_cap(scores["ASP"], scores["CP"])
    print("ASP so với CP (cặp chung, tốt hơn, bằng, kém hơn):", result)
    assert result == (1, 0, 1, 0)
    assert so_sanh_cap(scores["ASP"], scores["SAT/MaxSAT"]) == (2, 1, 0, 1)

Chạy python bao_cao_thuc_nghiem.py. Dữ liệu được tạo để minh họa phương pháp báo cáo, không phải kết quả thực nghiệm của các bộ giải. ASP và CP hòa nhau trên một cặp hợp lệ chung. ASP có hai lượt hợp lệ còn CP có một. Bỏ cột tỷ lệ và chỉ xem cặp điểm chung sẽ che mất khác biệt về số lịch tìm được.

4. Từ bảng tổng hợp đến câu hỏi nghiên cứu tiếp theo

• Phân nhóm instance theo mật độ xung đột, độ khan hiếm phòng hoặc số cơ sở. Kiểm tra xem chênh lệch giữa các phương pháp tập trung ở nhóm nào.
• Chạy thí nghiệm loại bỏ một thành phần trong mô hình hoặc thuật toán mỗi lần. Giữ nguyên ngân sách, cách chấm và tập dữ liệu để quan sát tác động của thành phần đó.
• Với thực nghiệm có nhiều lần lặp, báo cáo biến thiên theo instance và chỉ rõ cặp nào thiếu nghiệm. Nếu vẽ thời gian đến nghiệm, xác định trước cách biểu diễn các lượt bị cắt bởi giới hạn thời gian.

Câu hỏi mở. Các đặc trưng nào của bài toán dự báo phương pháp nào có lợi thế? Có thể kiểm tra dự báo đó trên một tập độc lập khác hay chỉ thấy trong dữ liệu đã dùng để điều chỉnh?

Đọc thêm về hồ sơ hiệu năng khi đối sánh phần mềm tối ưu hóa.