Giải ASP nhiều lượt khi dữ liệu lập lịch thay đổi

1. Một bài toán, nhiều lần cập nhật

Trong tuần xếp lịch, phòng có thể bận thêm một ca rồi mở lại khi một buổi họp bị hủy. Nếu mỗi thay đổi đều khởi tạo một tiến trình mới, hệ thống đọc lại mô hình và thực hiện lại các bước chuẩn bị. Giải nhiều lượt trong cùng một Control cho phép mô hình hóa những phần ổn định và các dữ kiện thay đổi theo từng lần giải.

Ví dụ chỉ có một lớp và ba ca. Chọn ca có chỉ số nhỏ nhất trong các ca khả thi. Ban đầu chọn ca 1. Sau khi khóa ca 1, chọn ca 2. Khóa tiếp ca 2 thì còn ca 3. Mở lại ca 1 thì ưu tiên trở về ca 1. Chuỗi thay đổi ngắn này kiểm tra cả việc bật và tắt một điều kiện.

2. Chọn thứ gì được điều khiển từ bên ngoài

#external ban(C) : ca(C). khai báo một nguyên tử điều khiển cho mỗi ca. Mô hình giữ quy tắc chọn một ca và điều kiện loại ca bị khóa. Chương trình Python gán True hoặc False cho từng nguyên tử external trước mỗi lần giải. Chương trình không thêm lại dữ kiện ban vào mọi lượt, nên việc mở khóa không cần xóa một luật đã ground.

Cần phân biệt thay đổi trạng thái của phần tử đã có với mở rộng miền. Nếu học kỳ phát sinh một ca hoàn toàn mới, ca đó chưa có trong miền đã ground. Khi ấy cần bổ sung khối chương trình phù hợp và ground phần mới, hoặc xây lại mô hình tùy thiết kế. Việc mở khóa một external đã khai báo không tự sinh thêm ca.

3. Chạy chuỗi cập nhật và lưu kết quả từng lượt

"""Xếp một lớp nhiều lần sau khi lịch phòng thay đổi."""
from clingo import Control, Function, Number

PROGRAM = """
ca(1..3).
#external ban(C) : ca(C).
1 { xep(C) : ca(C) } 1.
:- xep(C), ban(C).
#minimize { C@1,C : xep(C) }.
#show xep/1.
"""


def ca_tot_nhat(ctl):
    best = None
    with ctl.solve(yield_=True) as handle:
        for model in handle:
            [answer] = model.symbols(shown=True)
            best = answer.arguments[0].number
        if handle.get().unsatisfiable:
            return None
    return best


if __name__ == "__main__":
    ctl = Control(["0"])
    ctl.add("base", [], PROGRAM)
    ctl.ground([("base", [])])
    morning = Function("ban", [Number(1)])
    second = Function("ban", [Number(2)])
    result = [ca_tot_nhat(ctl)]
    ctl.assign_external(morning, True)
    result.append(ca_tot_nhat(ctl))
    ctl.assign_external(second, True)
    result.append(ca_tot_nhat(ctl))
    ctl.assign_external(morning, False)
    result.append(ca_tot_nhat(ctl))
    print("Ban đầu / khóa ca 1 / khóa thêm ca 2 / mở lại ca 1:", result)
    assert result == [1, 2, 3, 1]

Chạy python asp_multi_shot.py sau khi cài gói clingo. Mỗi lần gọi giải có thể in nhiều nghiệm trong quá trình cải thiện mục tiêu. Mã giữ nghiệm tốt nhất được trả về khi lượt giải kết thúc. Chuỗi mong đợi là [1, 2, 3, 1]. Hãy thử khóa cả ba ca để kiểm tra chương trình trả None, rồi mở lại một ca và quan sát nghiệm xuất hiện trở lại.

Trong một dịch vụ thật, cần đảm bảo lượt giải trước đã kết thúc hoặc đã được hủy trước khi thay đổi trạng thái của cùng đối tượng điều khiển. Ghi lại thứ tự cập nhật, ảnh chụp trạng thái dữ kiện và cấu hình giải. Nếu chỉ lưu lịch cuối, khó xác định lượt nào giữ lại một điều kiện cũ không mong muốn.

4. So sánh giải lặp với khởi tạo lại

Chuẩn bị cùng một chuỗi sự kiện và chạy hai cách trên cùng dữ liệu. So sánh tính khả thi, điểm và thời gian theo từng lượt. Ghi riêng thời gian lần đầu và các lần cập nhật. Thử thêm chuỗi ít thay đổi và chuỗi có nhiều thay đổi liên tiếp để tìm điều kiện mà cách giữ trạng thái có lợi.

Đo thêm mức xáo trộn nếu mục tiêu là điều chỉnh lịch đã công bố. Ví dụ, tính số lớp đổi ca hoặc đổi phòng so với lịch cũ và báo riêng với điểm chất lượng. Bài mẫu chỉ ưu tiên ca sớm để làm rõ cơ chế external. Đọc thêm Gebser và cộng sự · Multi-shot ASP solving with clingo.