Sức chứa tài nguyên tích lũy theo thời gian trong ASP

1. Từ phòng độc quyền tới tài nguyên dùng chung

Ràng buộc “một phòng chỉ phục vụ một lớp tại một thời điểm” phù hợp khi phòng là tài nguyên độc quyền. Tuy nhiên, nhiều nguồn lực có thể được chia sẻ: máy chủ thực hành, bộ thiết bị đo, nhân viên hỗ trợ phòng máy hoặc giấy phép phần mềm đồng thời. Hai lớp có thể cùng hoạt động nếu tổng nhu cầu không vượt số đơn vị sẵn có. Cấm mọi cặp chồng lấn sẽ loại phương án hợp lệ; chỉ kiểm tra số lớp đồng thời lại bỏ qua việc mỗi lớp cần lượng tài nguyên khác nhau.

Xét hai công việc A và B, mỗi việc cần hai đơn vị thiết bị trong hai đơn vị thời gian. Kho có ba đơn vị. A được bắt đầu ở 0 hoặc 1; B được bắt đầu ở 0 hoặc 2. Chân trời quan sát là khoảng từ 0 đến 4. Chỉ cần nhìn dữ liệu đã thấy hai việc không thể chồng nhau, vì 2 + 2 lớn hơn 3. Nhưng điều kiện nên được phát biểu bằng tổng nhu cầu để sau này vẫn đúng khi có nhiều việc và nhiều mức tiêu thụ.

2. Định nghĩa khoảng chiếm dụng và hàm tải

Với công việc j có thời điểm bắt đầu s(j), thời lượng d(j) và nhu cầu q(j), công việc chiếm tài nguyên tại t khi s(j) ≤ t < s(j)+d(j). Tải tại t là tổng q(j) của mọi việc đang hoạt động. Điều kiện khả thi là load(t) ≤ C tại mọi thời điểm cần xét. Bài mẫu dùng thời gian nguyên và thời lượng nguyên; mỗi số t đại diện một đoạn đơn vị [t,t+1).

Khoảng nửa mở giúp xử lý hai việc nối nhau. A bắt đầu 0, kéo dài 2, chiếm các đoạn 0 và 1. B bắt đầu 2 chiếm các đoạn 2 và 3. Tại mốc 2, A đã giải phóng tài nguyên, B bắt đầu sử dụng. Nếu vô tình dùng t ≤ s+d ở cận phải, cả A và B bị tính ở t = 2, tạo một xung đột giả. Đổi riêng toán tử cuối là một đột biến hữu ích để đánh giá bộ ca thử.

3. Sinh điểm bắt đầu, suy ra hoạt động, kiểm tra tổng

1 { start(J,S) : startok(J,S) } 1 :- task(J,D,Q).
busy(J,T) :- start(J,S), task(J,D,Q), time(T), S <= T, T < S+D.
usage(T,N) :- time(T), N = #sum { Q,J : busy(J,T), task(J,D,Q) }.
:- usage(T,N), N > cap.

Luật chọn tạo đúng một thời điểm bắt đầu cho mỗi công việc. Quan hệ busy nối một quyết định bắt đầu với tất cả đoạn thời gian bị chiếm. Quan hệ usage cộng nhu cầu ở từng đoạn. Khóa J trong phần tử tổng giữ riêng hai công việc có cùng nhu cầu. Nếu chỉ dùng Q làm bộ giá trị, hai công việc cùng cần 2 có thể bị gộp thành một phần tử và tải sai thành 2 thay vì 4.

Miền bắt đầu phải bảo đảm công việc kết thúc trong chân trời hoặc mô hình phải xét toàn bộ phần vượt ra. Trong ví dụ, mọi lựa chọn đều kết thúc chậm nhất ở 4, nên time(0..3) bao phủ đầy đủ. Nếu bổ sung một lựa chọn bắt đầu 3 cho việc dài 2 mà vẫn chỉ kiểm tra đến 3, đoạn [4,5) bị bỏ sót. Việc cố định miền t hữu hạn cần đi cùng lập luận rằng miền đã bao phủ toàn bộ khoảng chiếm dụng.

4. Chạy ba mức sức chứa để đối chiếu

Cài python -m pip install "clingo==5.8.3" rồi chạy python asp_suc_chua_tich_luy.py. Tệp chứa cả mô hình ASP và một oracle Python duyệt bốn cặp thời điểm bắt đầu. Oracle tính tải trực tiếp ở từng đoạn, không gọi lại quan hệ usage của ASP. Hai tập lịch được so bằng phần tử để phát hiện cả nghiệm thừa lẫn nghiệm thiếu.

"""Sức chứa tích lũy trên thời gian nguyên, kiểm tra bằng vét cạn độc lập."""
from itertools import product
import clingo

PROGRAM = r"""
#const cap=3.
time(0..3). task(a,2,2). task(b,2,2).
startok(a,0). startok(a,1). startok(b,0). startok(b,2).
1 { start(J,S) : startok(J,S) } 1 :- task(J,D,Q).
busy(J,T) :- start(J,S), task(J,D,Q), time(T), S <= T, T < S+D.
usage(T,N) :- time(T), N = #sum { Q,J : busy(J,T), task(J,D,Q) }.
:- usage(T,N), N > cap.
#show start/2.
"""

def asp_schedules(capacity):
    ctl = clingo.Control(["0", "-c", f"cap={capacity}"])
    ctl.add("base", [], PROGRAM)
    ctl.ground([("base", [])])
    schedules = set()
    def collect(model):
        starts = {str(a.arguments[0]): a.arguments[1].number
                  for a in model.symbols(shown=True)}
        schedules.add((starts["a"], starts["b"]))
    result = ctl.solve(on_model=collect)
    assert result.exhausted and not result.interrupted
    return schedules

def oracle(capacity):
    result = set()
    for sa, sb in product((0, 1), (0, 2)):
        # Duyệt trực tiếp từng đơn vị thiết bị ở mỗi thời điểm.
        loads = [sum(2 for start in (sa, sb) if start <= t < start + 2)
                 for t in range(4)]
        if max(loads) <= capacity:
            result.add((sa, sb))
    return result

for capacity in (1, 3, 4):
    actual = asp_schedules(capacity)
    assert actual == oracle(capacity)
    print(f"Sức chứa {capacity}: {len(actual)} lịch, {sorted(actual)}")
assert asp_schedules(3) == {(0, 2)}
assert len(asp_schedules(4)) == 4

Với sức chứa 1, ngay cả một việc riêng cũng cần quá nhiều thiết bị nên không có lịch. Với sức chứa 3, chỉ còn cặp (0,2). Với sức chứa 4, cả bốn cặp đều khả thi. Chuỗi 0–1–4 nghiệm này giúp kiểm tra đúng ý nghĩa của sức chứa. Nếu tăng C mà mất một nghiệm trước đó trong mô hình không có thay đổi khác, cần xem lại cách viết ràng buộc hoặc bộ chuyển đổi dữ liệu.

5. Mở rộng sang nhiều loại thiết bị

Để một việc cần cả máy tính cấu hình cao và trợ giảng, đưa mã tài nguyên R vào nhu cầu và sức chứa. Khi đó tải được tính theo từng cặp R–t. Khóa phần tử tổng cần nhận diện đúng đơn vị công việc. Hai dòng dữ liệu mô tả cùng một nhu cầu của cùng việc không nên bị hiểu thành hai nhu cầu độc lập; ngược lại, hai nhóm sinh viên khác nhau cần thiết bị riêng phải có định danh riêng nếu muốn cộng cả hai.

Sức chứa cũng có thể thay đổi theo thời gian. Một phòng máy có 30 máy nhưng 4 máy đang bảo trì trong buổi sáng thì sức chứa hiệu dụng của đoạn đó là 26. Cần phân biệt giảm lượng tài nguyên với cấm hoàn toàn tài nguyên. Nếu thiết bị yêu cầu thời gian chuẩn bị hoặc vệ sinh sau buổi học, hãy mở rộng khoảng chiếm dụng tương ứng và ghi rõ thời gian đệm có dùng cùng nguồn lực hay một loại nguồn lực khác.

6. Chọn độ phân giải thời gian có căn cứ

Mỗi đơn vị thời gian nhỏ hơn tạo mô hình ground lớn hơn. Tuy nhiên, làm tròn quá thô có thể đổi tập lịch khả thi. Một việc kết thúc 09:20 và việc khác bắt đầu 09:25 không thể được tùy tiện làm tròn thành hai ca tiếp giáp nếu còn thời gian chuẩn bị 10 phút. Nên chọn đơn vị dựa trên dữ liệu và chính sách làm tròn, sau đó tạo ca biên ngay quanh từng mốc thay đổi.

Với các khoảng cố định, tải chỉ thay đổi ở sự kiện bắt đầu hoặc kết thúc, nên có thể nghiên cứu cách kiểm tra theo các đoạn sự kiện thay vì mọi phút. Khi thời điểm bắt đầu là biến quyết định, tập sự kiện chưa biết trước và cần một mã hóa phù hợp hơn. Không nên xóa bớt thời điểm kiểm tra chỉ vì chúng chưa xuất hiện trong một lịch mẫu. Nếu dùng một công cụ hỗ trợ ràng buộc số học khác, cần đối chiếu lại ngữ nghĩa và phép đo trước khi so hiệu năng.

7. Thực nghiệm và bài tập mở rộng

Giữ số công việc cố định rồi tăng chân trời, số lựa chọn bắt đầu và số loại tài nguyên theo từng trục. Ghi số nguyên tử busy, thời gian grounding, thời gian giải và bộ nhớ đo được. Thêm một bộ kiểm chứng độc lập tính tải từ lịch xuất, đặc biệt tại thời điểm nhiều việc kết thúc và bắt đầu đồng thời. Bốn lựa chọn trong bài không đủ để kết luận cách mã hóa theo thời gian luôn nhanh hay chậm.

Bài tập: thêm việc C dài 1, cần 1 đơn vị, chỉ bắt đầu ở 1 hoặc 3. Với sức chứa 3, dự đoán những vị trí C có thể ghép vào lịch A = 0, B = 2. Tiếp theo cho B cần 3 đơn vị và giữ nguyên C; xác định đoạn nào trở thành nút thắt. Cuối cùng, viết một ca kiểm thử làm mô hình sai nếu bỏ J khỏi khóa tổng, rồi giải thích vì sao lỗi không xuất hiện khi mọi nhu cầu đều có giá trị khác nhau.

Nguồn cú pháp: Potassco Guide: aggregates và lựa chọn trong Clingo 5. Liên hệ Mã hóa lớp cần nhiều ca liên tiếp và Quét sự kiện để tìm nhu cầu phòng cực đại.