Lượng từ, an toàn biến và bẫy tập rỗng trong ASP

1. “Đủ mọi kỹ năng” có thể đúng khi chưa khai báo kỹ năng nào

Một bộ môn muốn phân công giảng viên cho các lớp. Lớp A cần Python và SQL, lớp B cần Java, còn lớp C chưa có danh sách kỹ năng. An có Python và SQL; Bình có Java; Cường chưa có kỹ năng nào trong dữ liệu. Người quản lý nói “chỉ chọn giảng viên đáp ứng mọi kỹ năng của lớp”. Nếu chỉ kiểm tra có thiếu kỹ năng nào hay không, cả ba người đều vượt qua phép kiểm tra đối với C. Kết quả dễ bị hiểu nhầm là bộ giải đã đánh giá C quá dễ.

Thực ra, mô hình chưa phân biệt “lớp không yêu cầu kỹ năng” với “chưa nhập yêu cầu của lớp”. Điều kiện phổ quát trên một tập rỗng được thỏa vì không có phần tử phản ví dụ. Bài này dùng chính tình huống đó để tách ba vấn đề: ngữ nghĩa lượng từ, an toàn biến khi grounding và chất lượng của dữ liệu đầu vào. Giải quyết một trong ba không tự giải quyết hai vấn đề còn lại.

2. Chuyển mệnh đề phổ quát thành việc tìm phản ví dụ

Với giảng viên g và lớp l, yêu cầu là: với mọi kỹ năng k mà l cần, g có k. Có thể kiểm tra mệnh đề này bằng cách tìm một k vừa được yêu cầu vừa không có ở g. Nếu tìm thấy, cặp g–l thiếu điều kiện. Nếu không tìm thấy phản ví dụ trong danh sách yêu cầu đã chốt, cặp đó vượt qua kiểm tra. Cách viết này thuận tiện cho việc giải thích: hệ thống có thể liệt kê kỹ năng cụ thể bị thiếu thay vì chỉ báo một giá trị đúng hoặc sai.

thieu(G,L) :- gv(G), can(L,K), not co(G,K).
du_ve_logic(G,L) :- gv(G), lop(L), not thieu(G,L).

Ở luật thứ nhất, G lấy từ danh mục giảng viên, L và K lấy từ các yêu cầu đã khai báo. Ở luật thứ hai, G và L đều có miền dương. Quan hệ thieu ở đây là kết luận tồn tại một phản ví dụ, không phải số kỹ năng bị thiếu. Nếu cần giải thích chi tiết hoặc tính điểm theo từng kỹ năng, nên giữ cả K trong một vị từ như thieu_ky_nang(G,L,K) rồi tổng hợp ở tầng khác.

3. Đọc đúng trường hợp lớp C

Không có fact can(c,K) nào nên không có cơ sở suy ra thieu(G,c) bằng luật đang xét. Vì vậy, cả ba cặp với C đều thuộc du_ve_logic. Muốn loại các lớp chưa khai báo yêu cầu, bài mẫu thêm co_yeu_cau(L) :- can(L,K). rồi yêu cầu vị từ này trong quan hệ ứng viên. Khi đó chỉ còn An–A và Bình–B. Đây là một quyết định về dữ liệu được chấp nhận, không phải việc sửa ngữ nghĩa của phép “mọi”.

Điều kiện tập yêu cầu không rỗng chỉ giải quyết một phần. Lớp A có một kỹ năng không có nghĩa danh sách đã hoàn chỉnh; có thể người nhập quên SQL. Trong hệ thống thực, cần trạng thái xác nhận riêng, chẳng hạn yêu cầu đã được duyệt, hoặc cờ cho phép không cần kỹ năng chuyên biệt. Một lớp có danh sách rỗng được duyệt hợp lệ cần được xử lý khác với một lớp chưa có dữ liệu.

4. Vì sao thêm miền dương vẫn cần thiết

Quy tắc du(G,L) :- not thieu(G,L). không cho biết grounder lấy G và L ở đâu. Trong phạm vi chương trình đang xét, các biến này không được ràng buộc an toàn. Việc thêm gv(G), lop(L) cung cấp miền hữu hạn rõ ràng. Tuy nhiên, sau khi đã an toàn, kết quả cho lớp C vẫn đúng theo logic tập rỗng. Không nên dùng việc chương trình hết báo lỗi grounding làm tiêu chí rằng đặc tả nghiệp vụ đã được phản ánh đầy đủ.

Cũng cần phân biệt miền một giảng viên–một lớp với miền kỹ năng cục bộ. Nếu buộc K phải lấy từ toàn bộ kỹ năng có trong khoa rồi yêu cầu giảng viên có tất cả K, ta đã thay “mọi kỹ năng của lớp này” bằng “mọi kỹ năng của cả khoa”. Một ca chỉ có hai lớp với yêu cầu khác nhau là đủ phát hiện lỗi đổi phạm vi lượng từ đó.

5. Đối chiếu ASP với một oracle nhỏ

Cài python -m pip install "clingo==5.8.3" rồi chạy python asp_luong_tu_tap_rong.py. Tệp tự tạo dữ liệu và chương trình ASP. Bộ kiểm tra Python dùng all() trên từng tập yêu cầu, sau đó so toàn bộ tập cặp đạt với kết quả Clingo. Cả hai cách cần đồng ý về miền giảng viên, lớp và kỹ năng trước khi việc đối chiếu có ý nghĩa.

"""Đối chiếu điều kiện mọi kỹ năng với all() của Python; clingo 5.8.x."""
import clingo

PROGRAM = r"""
lop(a;b;c). gv(an;binh;cuong).
can(a,python). can(a,sql). can(b,java).
co(an,python). co(an,sql). co(binh,java).
co_yeu_cau(L) :- can(L,K).
thieu(G,L) :- gv(G), can(L,K), not co(G,K).
du_ve_logic(G,L) :- gv(G), lop(L), not thieu(G,L).
ung_vien(G,L) :- du_ve_logic(G,L), co_yeu_cau(L).
#show du_ve_logic/2.
#show ung_vien/2.
"""

def evaluate(extra=""):
    ctl = clingo.Control(["0", "--warn=none"])
    ctl.add("base", [], PROGRAM + extra)
    ctl.ground([("base", [])])
    found = []
    def collect(model):
        row = {"du_ve_logic": set(), "ung_vien": set()}
        for atom in model.symbols(shown=True):
            row[atom.name].add(tuple(str(x) for x in atom.arguments))
        found.append(row)
    result = ctl.solve(on_model=collect)
    assert result.exhausted and len(found) == 1
    return found[0]

skills = {"an": {"python", "sql"}, "binh": {"java"}, "cuong": set()}
requirements = {"a": {"python", "sql"}, "b": {"java"}, "c": set()}
oracle = {(g, l) for g in skills for l in requirements
          if all(k in skills[g] for k in requirements[l])}
row = evaluate()
assert row["du_ve_logic"] == oracle
assert row["ung_vien"] == {("an", "a"), ("binh", "b")}
assert all((g, "c") in oracle for g in skills)
updated = evaluate("can(c,python).")
assert updated["ung_vien"] == {("an", "a"), ("binh", "b"), ("an", "c")}
print("Đạt phép kiểm tra phổ quát:", sorted(oracle))
print("Ứng viên có yêu cầu không rỗng:", sorted(row["ung_vien"]))
print("Thêm kỹ năng cho c:", sorted(updated["ung_vien"]))

Chương trình xác nhận năm cặp thỏa phép kiểm tra phổ quát: An–A, Bình–B và ba cặp với C. Khi áp dụng điều kiện không rỗng, tập ứng viên giảm còn hai. Bổ sung can(c,python). làm C có yêu cầu cụ thể; khi đó An–C được chấp nhận, Bình–C và Cường–C bị loại. Bộ kiểm tra so cả phần tử của tập thay vì chỉ so số cặp, vì hai tập sai khác vẫn có thể cùng kích thước.

6. Khi dữ liệu kỹ năng giảng viên cũng chưa đầy đủ

Trong ví dụ, not co(G,K) được dùng như “không đạt kỹ năng K theo danh sách đã chốt”. Nếu hồ sơ kỹ năng chưa được xác minh, sự vắng mặt có thể chỉ là chưa biết. Khi ấy phép kiểm tra đang trộn thiếu bằng chứng với bằng chứng thiếu kỹ năng. Có thể bổ sung trạng thái xác nhận hồ sơ, hoặc dùng quan hệ đánh giá nhiều mức rồi chỉ gán những cặp đã đủ căn cứ theo chính sách của bộ môn.

Đối với bài toán phân công lớn, nên chuẩn hóa mã kỹ năng, quan hệ tương đương và điều kiện suy ra trước khi xây miền. Chứng chỉ SQL nâng cao có được suy ra SQL cơ bản không? Kinh nghiệm Android có thay thế yêu cầu Java không? Mỗi phép suy ra cần có căn cứ riêng. Nếu thay đổi quan hệ tương thích trong lúc chạy thực nghiệm, số ứng viên tăng có thể do thay chính sách chuyên môn chứ không phải do cải thiện kỹ thuật giải.

7. Bộ ca kiểm tra giúp phát hiện lỗi phạm vi

Ít nhất cần có lớp không có yêu cầu, lớp có một yêu cầu, lớp có hai yêu cầu và giảng viên chỉ đáp ứng một trong hai. Thêm ca cùng một kỹ năng xuất hiện ở hai lớp để kiểm tra việc dùng sai khóa tổng hợp. Thử dữ liệu có mã giảng viên chưa tồn tại: hệ thống nên từ chối đầu vào hoặc báo lỗi tham chiếu theo hợp đồng, thay vì để một quan hệ lẻ lọt vào miền quyết định.

Bài tập mở rộng: thêm trạng thái da_duyet_yeu_cau(L) và một fact xác nhận C không đòi kỹ năng chuyên biệt. Hãy viết hai phiên bản: một phiên bản cấm mọi lớp có tập yêu cầu rỗng, một phiên bản cho phép tập rỗng đã được duyệt. Tìm dữ liệu khiến hai tập nghiệm khác nhau, sau đó diễn giải bằng ngôn ngữ nghiệp vụ. Đây là bước cần làm trước khi đặt câu hỏi phiên bản nào chạy nhanh hơn.

Nguồn đối chiếu cú pháp và miền biến: ASP-Core-2 Input Language Format và Potassco Guide dòng 5. Đọc cùng bài Phủ định và dữ liệu chưa biết, rồi đối chiếu với Thu hẹp miền ứng viên khi grounding.