Bài báo này trình bày một bộ đếm mô hình SMT mới, được gọi là pact, để giải quyết bài toán đếm mô hình cho công thức SMT (Lý thuyết Môđun Khả Năng Đáp Ứng) lai. Trong khi các phương pháp tiếp cận dựa trên bit-blasting hiện có hạn chế là bị giới hạn ở các biến rời rạc, pact ước tính số lượng nghiệm với các đảm bảo lý thuyết bằng cách sử dụng phép đếm mô hình xấp xỉ dựa trên hàm băm. pact thực hiện các lệnh gọi trình giải SMT logarit cho các biến chiếu và cải thiện hiệu suất bằng cách sử dụng các hàm băm được tối ưu hóa. Các thử nghiệm chuẩn mở rộng cho thấy pact cải thiện đáng kể hiệu suất so với các phương pháp hiện có. Ví dụ, trong số 14.202 trường hợp, pact xử lý thành công 603 trường hợp, trong khi các phương pháp hiện có chỉ xử lý được 13.
