Tìm số ca nhỏ nhất bằng tính đơn điệu của khả thi

1. Phát biểu giả định trước khi tìm biên

Có ba lớp cùng dùng một tài nguyên nên không được trùng ca. Với h ca, mỗi lớp chọn đúng một ca trong tiền tố 1 đến h. Nếu tăng h mà chỉ mở rộng miền, lịch cũ vẫn dùng được. Do đó khi một h khả thi, mọi h lớn hơn cũng khả thi trong mô hình này. Tính đơn điệu cho phép tìm giá trị đầu tiên chuyển từ sai sang đúng.

2. Giữ nguyên bài toán khi mở rộng miền

Việc tăng số ca có thể đồng thời thêm yêu cầu “mỗi ca phải có lớp” hoặc thay đổi chính sách nghỉ. Khi ấy, phương án ở miền nhỏ có thể không còn hợp lệ ở miền lớn. Không nên áp dụng tìm kiếm nhị phân chỉ vì biến h có ý nghĩa thời gian. Cần chứng minh rằng phép nhúng lịch cũ vào miền mới bảo toàn mọi điều kiện.

3. Chạy oracle khả thi trên mô hình nhỏ

Mẫu gọi Clingo cho h từ 1 đến 4 và nhận sai, sai, đúng, đúng. Hàm tìm biên trả 3. Cận trên được kiểm tra khả thi trước khi thu hẹp khoảng. Ví dụ dựng lại bộ giải ở mỗi lượt để giữ phép thử dễ đọc. Sau khi kiểm chứng, có thể so với cách tái sử dụng trạng thái ở các lượt giải.

Cài thư viện bằng python -m pip install clingo nếu môi trường chưa có Clingo.

Chạy ví dụ bằng python asp_tim_horizon_nho_nhat.py.

import clingo

def kha_thi(h):
    ctl = clingo.Control()
    ctl.add("base", [], f"""
        lop(a;b;c). ca(1..{h}).
        1 {{ xep(L,C) : ca(C) }} 1 :- lop(L).
        :- xep(L,C), xep(M,C), L<M.
    """)
    ctl.ground([("base", [])])
    return bool(ctl.solve().satisfiable)

def can_dau(ngan, dai):
    if not kha_thi(dai):
        raise ValueError("Cận trên chưa có lịch khả thi")
    while ngan < dai:
        giua = (ngan + dai) // 2
        if kha_thi(giua):
            dai = giua
        else:
            ngan = giua + 1
    return ngan

assert [kha_thi(h) for h in range(1, 5)] == [False, False, True, True]
assert can_dau(1, 4) == 3
print("Horizon nhỏ nhất bằng 3.")

4. Đánh giá chi phí toàn quy trình

Số lượt gọi bộ giải ít hơn chưa chắc làm tổng thời gian thấp hơn, vì chi phí một lượt ở gần biên có thể lớn. Báo cả số lượt, thời gian grounding, thời gian giải và trạng thái kết thúc. Khi một lượt hết hạn mà chưa biết khả thi, không được tự quy thành vô nghiệm để cập nhật cận, vì điều đó có thể loại mất đáp án đúng.

Đọc thêm Tài liệu Clingo về mô hình và điều khiển quá trình giải.