Nghiên cứu lý thuyết phép mã hóa SAT/MaxSAT/Pseudo-Boolean, phát triển bộ giải chính xác ứng dụng trong lập lịch công nghiệp, đóng gói 2D, gán nhãn đồ thị và kiểm chứng phần mềm.
Chúng tôi xây dựng các phép mã hóa SAT và bộ giải chính xác có hiệu năng vượt trội so với các công cụ tối ưu hóa thương mại MIP/CPLEX/Gurobi trên các bài toán tổ hợp khó.
Bộ đếm tuần tự thích nghi (NSC), các ràng buộc đếm Cardinality (AMO/AMK/ALK), mã hóa Pseudo-Boolean và hệ sinh thái thư viện SCLib.
Tối ưu đỉnh công suất trong dây chuyền sản xuất (SALB, UALBP), lập lịch Job-Shop (JSSP/FJSSP) và điều hành tàu hỏa bằng MaxSAT-DDD.
Mô hình SAT/MaxSAT giải chính xác bài toán đóng gói dải chữ nhật 2D (Strip Packing), 2D Bin Packing và cắt cuộn nguyên liệu.
Thuật toán giải chính xác cho các bài toán Antibandwidth, Cyclic Antibandwidth, Radio-k Labeling, tô đa màu và phân bổ tần số di động.
Công trình chuyên khảo hệ thống hóa cơ sở lý thuyết và kỹ thuật thực thi các phép mã hóa SAT tối ưu cho bài toán tối ưu hóa tổ hợp.
Chúng tôi luôn chào đón các bạn sinh viên đại học, thạc sĩ và nghiên cứu sinh đam mê lĩnh vực thuật toán và tối ưu hóa tổ hợp.
Xem các đề tài & vị trí mở ↗