1. SCLib: Thư viện bộ đếm dùng chung & hệ sinh thái bộ giải
Thư viện C++ hiệu năng cao tối ưu việc sinh các biến thể bộ đếm tuần tự (NSC), mã hóa ràng buộc đếm dạng bậc thang (AMO/AMK) và chuyển đổi Pseudo-Boolean.
Các dự án trọng điểm đang triển khai nhằm phát triển bộ giải SAT/MaxSAT hiệu năng cao, công cụ lý giải tự động và các ứng dụng tối ưu hóa công nghiệp.
Thư viện C++ hiệu năng cao tối ưu việc sinh các biến thể bộ đếm tuần tự (NSC), mã hóa ràng buộc đếm dạng bậc thang (AMO/AMK) và chuyển đổi Pseudo-Boolean.
Hệ thống lập lại biểu đồ chạy tàu thời gian thực kết hợp kỹ thuật lan truyền Dynamic Decoupled Domain (DDD) với mô hình mã hóa MaxSAT cho mạng lưới đường sắt đơn và đa ray.
Mô hình mã hóa SAT giải quyết bài toán giảm thiểu đỉnh công suất tiêu thụ điện và thời gian hoàn thành (makespan) trong dây chuyền lắp ráp (SALBP / UALBP).
Mô hình mã hóa SAT và MaxSAT gọn giải chính xác các bài toán đóng gói dải 2D (Strip Packing), Bin Packing 2D và cắt cuộn nguyên liệu công nghiệp.
Thuật toán giải chính xác dựa trên SAT cho các bài toán Antibandwidth, Cyclic Antibandwidth, Radio-k Labeling, tô đa màu và phân bổ tần số mạng di động.