Đối đầu NuCS và Choco: Khi trình giải ràng buộc Python thuần túy thách thức "kỳ lão" Java

Đối đầu NuCS và Choco: Khi trình giải ràng buộc Python thuần túy thách thức "kỳ lão" Java

Trong thế giới lập trình ràng buộc (Constraint Programming), sự so sánh giữa một ngôn ngữ thông dịch như Python và một "cỗ máy" ảo Java (JVM) đã được tối ưu hóa hàng thập kỷ thường mang lại kết quả dễ đoán trước. Tuy nhiên, cuộc đối đầu mới đây giữa NuCS — một trình giải ràng buộc viết hoàn toàn bằng Python — và Choco — một thư viện Java lâu đời — đã mang đến những kết quả đầy bất ngờ.

NuCS, được phát triển bởi tôi và tăng tốc bằng NumPy cùng Numba, dường như yếu thế hơn hẳn so với Choco, vốn đã tồn tại hơn hai thập kỷ và sở hữu kho tàng các ràng buộc toàn cầu phức tạp. Thực tế chứng minh điều ngược lại: khi chạy trên cùng một mô hình, cả hai có tốc độ tương đương nhau về mặt thực tế. Đáng chú ý hơn, ở các bài toán có quy mô lớn nhất, NuCS thậm chí còn vượt lên dẫn đầu.

Biểu đồ so sánh hiệu suất All-interval series

Kiến trúc và Triết lý thiết kế

Sự khác biệt cốt lõi giữa hai công cụ này nằm ở cách chúng xử lý miền giá trị của biến số.

NuCS đại diện cho một cược kiến trúc táo bạo: viết một trình giải ràng buộc cạnh tranh hoàn toàn bằng Python. Để bù đắp cho nhược điểm của ngôn ngữ thông dịch, NuCS sử dụng Numba để biên dịch just-in-time (JIT) các vòng lặp nội tại thành mã máy gốc. Điều này giúp NuCS đạt được thông lượng kiểu C trong khi vẫn giữ được sự linh hoạt của Python. Một quyết định thiết kế quan trọng khác là NuCS chỉ biểu diễn miền giá trị dưới dạng khoảng [min..max]. Điều này giúp việc xử lý cực kỳ nhanh và dễ vector hóa bằng NumPy, nhưng cũng đồng nghĩa với việc NuCS bị giới hạn ở tính nhất quán biên (Bound Consistency - BC) và không thể xử lý các "lỗ hổng" trong miền giá trị.

Ngược lại, Choco là một cựu binh trên JVM, được phát triển chủ yếu tại IMT Atlantique. Choco hỗ trợ cả miền giá trị bị chặn (intervals) và miền liệt kê (enumerated/bitsets), cho phép biểu diễn các tập hợp con bất kỳ — bao gồm cả các miền có lỗ hổng. Khả năng này mở đường cho tính nhất cung (Arc Consistency - AC) mạnh mẽ và một thư viện khổng lồ các ràng buộc toàn cầu như allDifferent, cardinality, hay circuit.

Nhóm bài toán 1: Cùng mô hình, so sánh động cơ

Khi cả hai trình giải chạy cùng một mô hình với mức độ nhất quán tương đương, chúng ta đang thực sự so sánh hiệu năng của động cơ bên dưới.

All-interval series (Tìm một giải pháp)

Đây là bài toán tìm một hoán vị của các số nguyên sao cho chuỗi các khoảng cách tuyệt đối giữa các số liên tiếp cũng tạo thành một hoán vị. Cả hai đều sử dụng tính nhất quán biên (BC) và heuristic tương tự.

Kết quả cho thấy hai đường biểu đồ gần như trùng khít ở các kích thước nhỏ và trung bình. Tuy nhiên, khi kích thước bài toán tăng lên n=16000, NuCS bắt đầu tách khỏi nhóm dẫn đầu và hoàn thành bài toán nhanh hơn Choco (85 giây so với 120 giây). Điều này chứng minh rằng khi Numba đã biên dịch xong, chi phí trên mỗi nút tìm kiếm của NuCS thấp hơn đáng kể.

Schur’s lemma (Chứng minh vô nghiệm)

Bài toán này yêu cầu chia các số nguyên 1..n thành các tập hợp không chứa bộ ba (x, y, z) thỏa mãn x + y = z. Đây là bài toán vô nghiệm, buộc trình giải phải duyệt qua toàn bộ cây tìm kiếm.

Ở đây, NuCS một lần nữa vượt lên trên ở các quy mô lớn (n=1600) với tốc độ nhanh hơn 1.22 lần so với Choco. Sự vượt trội này đến từ chi phí cố định thấp trên mỗi nút của NuCS sau khi đã qua quá trình biên dịch JIT.

Nhóm bài toán 2: Mô hình khác nhau, so sánh chiến lược

Ở nhóm này, các mô hình khác nhau phản ánh sự khác biệt về triết lý thiết kế giữa hai trình giải.

Latin Square (Ô vuông Latin)

Bài toán điền các số vào lưới sao cho mỗi số xuất hiện đúng một lần ở mỗi hàng và cột.

Biểu đồ hiệu suất Latin Square

Khi sử dụng mô hình BC thuần túy, cả NuCS và Choco đều "bó tay" trước bài toán kích thước 50. Tuy nhiên, nhờ sự linh hoạt trong việc mô hình hóa bằng Python, NuCS có thể dễ dàng thêm vào các ràng buộc dư thừa (redundant constraints) và kênh (channeling). Kết quả là NuCS đã giải quyết bài toán n=50 chỉ trong 728 mili-giây — một chiến thắng về mặt chất lượng mà Choco (với mô hình BC mặc định) không thể đạt được.

Magic Sequence (Dãy ma thuật)

Bài toán này yêu cầu một dãy số tự mô tả, trong đó x_i đếm số lần giá trị i xuất hiện trong cả dãy.

Biểu đồ hiệu suất Magic Sequence

Choco sử dụng ràng buộc toàn cầu mạnh mẽ (AC) và rất nhanh ở các bài toán nhỏ (n=100). Tuy nhiên, khi quy mô tăng lên n=400, chi phí tính toán cao của AC khiến Choco bị chậm lại. Ngược lại, NuCS sử dụng BC đơn giản kết hợp với hai ràng buộc tuyến tính dư thừa. Chi phí trên mỗi nút thấp của NuCS giúp nó vượt lên dẫn đầu ở quy mô lớn, nhanh hơn Choco gần 1.9 lần tại n=400.

Golomb Ruler (Thước kẻ Golomb)

Đây là bài toán tối ưu hóa khó khăn, đòi hỏi các khoảng cách giữa các dấu trên thước phải là duy nhất.

Choco có lợi thế lớn nhờ miền giá trị liệt kê cho phép loại bỏ các giá trị ở giữa miền (lỗ hổng). Mô hình BC thuần túy của NuCS chậm hơn khoảng 2 lần. Tuy nhiên, khi viết một thuật toán nhất quán tùy chỉnh (custom propagator) bằng vài chục dòng Python được biên dịch bởi Numba, NuCS đã san bằng khoảng cách, đạt hiệu suất tương đương Choco.

Kết luận: Sự đánh đổi giữa Động cơ và Mô hình

Cuộc đối đầu này không chỉ đơn thuần là "ai nhanh hơn". Nó tiết lộ hai điểm thiết kế khác biệt trong không gian lập trình ràng buộc:

• NuCS: Tập trung vào chi phí trên mỗi nút cực thấp và khả năng mô hình hóa rẻ tiền. Sự hạn chế về tính nhất quán biên (BC) thường được bù đắp bằng việc thêm các ràng buộc dư thừa hoặc thuật toán tùy chỉnh dễ dàng trong Python.
• Choco: Cung cấp các ràng buộc toàn cầu mạnh mẽ (AC) ngay lập tức, lý tưởng cho các bài toán phức tạp cần lọc giá trị sâu, nhưng chi phí tính toán trên mỗi nút cao hơn.

Đối với những nhà phát triển muốn tận dụng sức mạnh của Java và các thư viện ràng buộc đã được kiểm chứng, Choco vẫn là lựa chọn tham chiếu. Nhưng đối với những người muốn thử nghiệm các mô hình trong Python và vẫn đạt được tốc độ mã máy, NuCS là một minh chứng mạnh mẽ cho thấy ngôn ngữ không còn là nút thắt cổ chai. Sự tự do trong việc định hình lại mô hình — thêm dư thừa, kênh, hoặc bộ lọc tùy chỉnh trong vài dòng code — thường quan trọng không kém tốc độ động cơ thô sơ hay sức mạnh của tính nhất quán.

"Khi một bài toán thực sự cần loại bỏ các giá trị ở giữa miền, các ràng buộc toàn cầu AC của Choco là công cụ đúng đắn. Nhưng khi mô hình tốt tồn tại, phong cách BC giá rẻ cộng với các ràng buộc dư thừa của NuCS có thể cạnh tranh và ngày càng thắng thế."