Đếm lịch sau phép chiếu thay vì đếm mọi answer set

1. Khi số nghiệm làm người đọc hiểu nhầm

Mô hình có thể dùng một nguyên tử phụ để ghi nhận đường suy luận, lựa chọn nội bộ hoặc một thông tin chưa hiển thị. Nếu nguyên tử đó được chọn độc lập, mỗi lịch nghiệp vụ có thể tương ứng với nhiều answer set. Báo tổng số answer set thành số thời khóa biểu sẽ làm phóng đại độ đa dạng. Cần xác định một lịch được nhận diện bằng những biến nào.

2. Phân biệt hiển thị và phép chiếu

Chỉ thị #show quyết định nguyên tử nào được đưa ra ở phần hiển thị. Nó không tự bảo đảm hai answer set cùng phần hiển thị chỉ được liệt kê một lần trong cách chạy thông thường. Ví dụ có hai phép gán xep và một nguyên tử phụ tùy chọn. Có bốn answer set nhưng chỉ hai tập nguyên tử xep khác nhau.

3. Kiểm chứng cả hai con số

Mẫu chạy một lần theo chế độ thường và một lần với --project=show trên Clingo 5.8. Lần đầu callback nhận bốn mô hình, nhưng đưa phần hiển thị vào set chỉ còn hai giá trị. Lần sau nhận hai đại diện sau chiếu. Việc chuẩn hóa thứ tự nguyên tử giúp hai tập tương đương không bị xem là khác chỉ vì thứ tự xuất hiện.

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_chieu_va_dem_nghiem.py.

import clingo

def dem(options):
    ctl = clingo.Control(["0", *options])
    ctl.add("base", [], "1 { xep(1); xep(2) } 1. { phu }. #show xep/1.")
    ctl.ground([("base", [])])
    hien_thi = []
    ctl.solve(on_model=lambda m: hien_thi.append(tuple(sorted(map(str, m.symbols(shown=True))))))
    return len(hien_thi), len(set(hien_thi))

assert dem([]) == (4, 2)
assert dem(["--project=show"]) == (2, 2)
print("Đếm thường", dem([]), "| Đếm sau chiếu", dem(["--project=show"]))

4. Chọn khóa lịch đúng với mục đích sử dụng

Nếu người dùng quan tâm cả phòng, chiếu lên ca mà bỏ phòng có thể gộp những lựa chọn khác nhau về nghiệp vụ. Ngược lại, dùng nguyên tử phụ làm khóa lại tạo nhiều bản sao. Khi có tối ưu, kiểm tra cách chế độ liệt kê tương tác với mục tiêu và chỉ đếm tập lịch đáp ứng mức chất lượng đã công bố. Lưu cả khóa chiếu và số lịch để người khác có thể tính lại.

Đọc thêm Tham chiếu Clingo và các tùy chọn liệt kê.