Vấn đề giải quyết các bài toán Satisfiability Modulo Theories (SMT)hiện nay đang được nghiên cứu và phát triển ởnhiều nơi trên thếgiới. Cho đến ngày nay, nhiều trường đại học, tổ chức đã nghiên cứu và đưa ra những bộ giải giải quyết bài toán SMT (hay còn gọi là SMT solver). Ví dụnhưZ3 của Mcrosoft, yices của SRI, CVC3 của một sốtrường đại học danh tiếng của Mỹ. hay boolector, openSMT của một số trường đại học danh tiếng khác Tuy nhiên, mỗi solver có một lợi thế ưu điểm riêng đối với các dạng khác nhau của bài toán SMT. Vậy vấn đề đặt ra là làm sao đểtận dụng được hết các ưu điểm đó cho từng bài toán. Đểgiải quyết vấn đề ấy, nhóm nghiên cứu đã nghiên cứu và xây dựng một hệ thống giải quyết bài toán SMT trực tuyến, kết hợp nhiều bộgiải khác nhau để đưa ra được lời giải tối ưu cho từng bài toán SMT. Trong khuôn khổkhóa luận tốt nghiệp này của cá nhân tôi, tôi đã xây dựng hai hệthống con của hệthống đã nêu trên là hệthống trên máy khách (users) và trên máy trạm (sửdụng đểgọi các Solver). Hệthống trên máy khách sẽ đảm nhiệm việc cung cấp một giao diện lập trình ứng dụng (Application Programming Interface hay API) để người dùng sửdụng có thểxây dựng bài toán SMT theo chuẩn thưviện SMT (SMTLIB) và sau đó là gửi bài toán đến máy chủ(server). Hệthống trên máy trạm sẽtiếp nhận bài toán từmáy chủvà gọi các bộgiải đểgiải quyết bài toán đó và gửi vềmáy chủkết qu