Grounding trong ASP và cách thu hẹp miền ứng viên

1. Chi phí bắt đầu trước khi bộ giải tìm lịch

Một mô hình ASP lập lịch thường có quyết định xep(L,C,P) cho lớp, ca và phòng. Cách viết dễ đọc nhất là sinh mọi bộ ba rồi dùng ràng buộc cấm các phương án sai sức chứa, sai loại phòng hoặc rơi vào ca bận. Trong mô hình nhỏ, cách này dễ kiểm tra. Khi số lớp, ca và phòng tăng, miền tích Descartes có thể chứa rất nhiều ứng viên mà nghiệp vụ đã loại ngay từ đầu.

Có thể xây quan hệ duoc(L,C,P) từ dữ liệu tĩnh rồi chỉ sinh quyết định trong miền đó. Câu hỏi nghiên cứu là ta giảm được phần nào của chương trình ground, và lợi ích có chuyển thành thời gian hoặc bộ nhớ tốt hơn không. Hai câu hỏi cần được đo riêng. Một mô hình có ít biến quyết định hơn vẫn có thể cần nhiều quan hệ phụ trợ hoặc có hành vi tìm kiếm khác.

2. Chỉ đưa điều kiện tĩnh vào miền ứng viên

Sức chứa phòng và ca bận đã biết trước nên có thể lọc khi tạo miền. Ràng buộc hai lớp không dùng cùng phòng trong cùng ca lại phụ thuộc các quyết định được chọn. Điều kiện này vẫn được kiểm tra sau khi sinh quyết định. Nếu nhầm một điều kiện liên quan nhiều lớp thành điều kiện tĩnh, ta có thể bỏ mất lịch hợp lệ hoặc giữ lịch sai.

Để so sánh, xét A có 30 sinh viên và B có 55, ba ca và ba phòng sức chứa 35, 60, 70. B bận ca 1. Miền đầy đủ có 18 bộ ba. Sau khi lọc, A giữ 9 lựa chọn, B giữ 4, tổng là 13. Có 36 cặp lựa chọn của hai lớp trước khi kiểm tra chung phòng và ca. Bốn cặp xung đột bị loại, nên còn 32 lịch.

3. Đếm miền và kiểm tra tập nghiệm bằng Clingo

"""Đếm nguyên tử quyết định, đối chiếu nghiệm của hai cách tạo miền."""
import clingo

DATA = """
lop(a,30). lop(b,55).
ca(1..3).
phong(p1,35). phong(p2,60). phong(p3,70).
ban(b,1).
:- xep(L,C,P), xep(M,C,P), L < M.
#show xep/3.
"""
DENSE = """
1 { xep(L,C,P) : ca(C), phong(P,_) } 1 :- lop(L,_).
:- xep(L,_,P), lop(L,N), phong(P,S), N > S.
:- xep(L,C,_), ban(L,C).
"""
SPARSE = """
duoc(L,C,P) :- lop(L,N), ca(C), phong(P,S), N <= S, not ban(L,C).
1 { xep(L,C,P) : duoc(L,C,P) } 1 :- lop(L,_).
"""


def run(encoding):
    ctl = clingo.Control(["0"])
    ctl.add("base", [], DATA + encoding)
    ctl.ground([("base", [])])
    atoms = sum(1 for _ in ctl.symbolic_atoms.by_signature("xep", 3))
    models = set()
    with ctl.solve(yield_=True) as handle:
        for model in handle:
            models.add(tuple(sorted(map(str, model.symbols(shown=True)))))
        assert handle.get().satisfiable
    return atoms, models


if __name__ == "__main__":
    dense, left = run(DENSE)
    sparse, right = run(SPARSE)
    print("Nguyên tử xep/3:", dense, "->", sparse)
    print("Lịch khả thi:", len(left))
    assert (dense, sparse) == (18, 13)
    assert left == right and len(left) == 32

Cài gói clingo cho Python rồi chạy python asp_grounding_domains.py. Chương trình đếm nguyên tử quyết định xep/3, liệt kê toàn bộ nghiệm ở kích thước nhỏ và so sánh hai tập lịch. Việc chỉ so số nghiệm là chưa đủ vì hai tập khác nhau có thể có cùng số phần tử. Ở đây từng lịch được chuẩn hóa theo chuỗi nguyên tử trước khi so.

Một ca cần thử thêm là lớp có sĩ số lớn hơn mọi phòng. Miền ứng viên rỗng và yêu cầu “đúng một phép gán” làm bài toán vô nghiệm. Nếu vì muốn tránh vô nghiệm mà vô tình thay ràng buộc đúng một bằng tối đa một, lớp đó có thể biến mất khỏi lịch. Đây là phản ví dụ để kiểm tra ý nghĩa của miền rỗng.

4. Thiết kế thực nghiệm cho dữ liệu lớn

Tạo nhiều instance theo quy mô và tỷ lệ ứng viên bị loại. Chạy hai mã hóa với cùng dữ liệu, cấu hình, giới hạn và cách chấm. Báo riêng thời gian grounding, thời gian giải, số quyết định và bộ nhớ nếu đo được. Nếu một lượt hết thời gian, ghi trạng thái và nghiệm tốt nhất tìm được thay vì thay bằng điểm 0.

Đối chiếu thêm tập vi mô có xung đột phòng, không có ứng viên và có nhiều nghiệm tối ưu. Câu hỏi đáng khảo sát là mức độ lọc tĩnh nào giúp giảm bộ nhớ rõ rệt, và ở nhóm instance nào thời gian giải tăng dù miền quyết định nhỏ hơn. Xem cú pháp và phạm vi biến trong tài liệu ngôn ngữ Clingo.