Một Bằng Chứng Máy Tính Giải Quyết Vấn Đề 'Tô Màu Xếp Hàng'

Là sinh viên đại học tại Đại học Chile, Bernardo Subercaseaux có cái nhìn không tích cực về việc sử dụng máy tính để thực hiện toán học. Điều này dường như đối lập với sự khám phá trí tuệ thực sự.

“Có một vài bản năng hoặc phản ứng nhanh chóng phản đối việc sử dụng máy tính để giải quyết vấn đề của bạn, như nó đi ngược lại với sự đẹp đẽ hoặc thanh lịch lý tưởng của một lập luận tuyệt vời,” anh ta nói.

Nhưng sau đó, vào năm 2020, Subercaseaux đắm chìm trong tình yêu và như thường lệ, ưu tiên của anh thay đổi. Đối tượng của sự ám ảnh của anh là một câu hỏi mà anh thấy trên một diễn đàn trực tuyến. Hầu hết các vấn đề anh quét qua và quên, nhưng vấn đề này đã thu hút anh. Anh chấm ngón tay phải.

“Điều đầu tiên tôi làm là thích bài đăng trong nhóm Facebook, hy vọng sẽ nhận được thông báo sau này khi ai đó đăng một giải pháp,” anh ta nói.

Câu hỏi đó liên quan đến việc điền số vào một lưới vô hạn. Nhưng đó không phải là loại vấn đề mà ai cũng giải quyết được một cách dễ dàng. Để giải quyết nó, Subercaseaux đã phải rời Chile để học sau đại học tại Đại học Carnegie Mellon.

Ở đó, vào tháng 8 năm 2021, anh có một cuộc gặp may mắn với Marijn Heule, một nhà khoa học máy tính sử dụng sức mạnh tính toán lớn để giải các vấn đề toán khó. Subercaseaux hỏi Heule liệu anh ấy có muốn thử sức với vấn đề này không, mở đầu cho một sự hợp tác kết thúc vào tháng 1 với một bằng chứng có thể tóm gọn bằng một con số duy nhất: 15.

Nhóm nghiên cứu thực sự không điền vào một lưới vô hạn. Họ không cần phải. Thay vào đó, đủ để lấy một phần nhỏ của lưới - chẳng hạn một hình vuông 10x10 - điền vào đó với các số, sau đó chứng minh rằng các bản sao của phần nhỏ đã điền có thể được đặt cạnh nhau, giống như bạn sẽ che phủ sàn nhà với bản sao của một viên gạch.

Khi Subercaseaux lần đầu tiên biết về vấn đề, anh bắt đầu tìm kiếm các viên gạch bằng bút và giấy. Anh sẽ vẽ lưới số, gạch chéo chúng, thử lại. Anh sớm chán mệt với cách tiếp cận đó và anh đã yêu cầu một người bạn thiết kế một công cụ trực tuyến giống như trò chơi Minesweeper để anh có thể kiểm tra các kết hợp nhanh hơn. Sau vài tuần nữa làm việc, anh đã thuyết phục chính mình rằng không có cách nào để điền một lưới với tám số, nhưng anh không thể tiến xa hơn vậy - có quá nhiều hình dạng tiềm ẩn của viên gạch và quá nhiều cách khác nhau chúng có thể được điền vào bằng các số.

Vấn đề, như sau này trở nên rõ ràng, là việc chứng minh rằng lưới không thể được che phủ bởi một tập hợp cụ thể các số khó hơn nhiều so với việc chứng minh rằng nó có thể. “Đó không chỉ là chứng minh rằng một cách không hoạt động, mà là chứng minh rằng mọi cách có thể không hoạt động,” Goddard nói.

Sau khi Subercaseaux bắt đầu tại CMU và thuyết phục Heule làm việc cùng anh, họ nhanh chóng tìm ra cách che phủ lưới với 15 số. Họ cũng có thể loại trừ khả năng giải quyết vấn đề chỉ với 12 số. Nhưng cảm giác chiến thắng của họ chỉ kéo dài ngắn ngủi, khi họ nhận ra rằng họ chỉ là tái tạo kết quả đã tồn tại từ lâu: Ngay từ năm 2017, các nhà nghiên cứu đã biết rằng câu trả lời không ít hơn 13 và không lớn hơn 15.

Đối với một sinh viên năm đầu đã thuê một giáo sư lớn vào việc giải quyết vấn đề cá nhân của mình, đó là một phát hiện không dễ chịu. “Tôi kinh ngạc. Tôi đã đang làm việc trong vài tháng trên một vấn đề mà không nhận ra điều này, và tệ hơn nữa, tôi đã khiến Marijn phí thời gian của anh ấy vào đó!” Subercaseaux viết trong một bài đăng blog tổng kết công việc của họ.

Tuy nhiên, Heule lại thấy phát hiện về kết quả quá khứ làm tăng cường năng lượng. Điều đó chứng minh rằng những nhà nghiên cứu khác cũng coi vấn đề này là quan trọng đủ để nghiên cứu và xác nhận với anh rằng kết quả duy nhất đáng đạt được là giải quyết vấn đề hoàn toàn.

“Khi chúng tôi nhận ra đã có 20 năm nghiên cứu về vấn đề này, điều đó đã làm thay đổi toàn bộ cảnh quan,” anh nói.

Tránh Nội Dung Thiếu Văn Hóa

Qua nhiều năm, Heule đã xây dựng sự nghiệp của mình bằng cách tìm cách hiệu quả để tìm kiếm giữa các tổ hợp có thể kết hợp lớn. Phương pháp của anh được gọi là giải SAT - viết tắt của “satisfiability.” Nó bao gồm việc xây dựng một công thức dài, gọi là công thức Boolean, có thể có hai kết quả: 0 hoặc 1. Nếu kết quả là 1, công thức là đúng và vấn đề được thoả mãn.

Đối với vấn đề tô màu gói hàng, mỗi biến trong công thức có thể đại diện cho việc một ô cụ thể có được chiếm bởi một số cụ thể hay không. Máy tính tìm cách gán giá trị biến để thoả mãn công thức. Nếu máy tính có thể làm được, bạn biết rằng có thể đóng gói lưới dưới các điều kiện bạn đã đặt ra.

Thật không may, một mã hóa trực tiếp của vấn đề tô màu gói hàng dưới dạng công thức Boolean có thể mở rộng đến hàng triệu điều kiện - máy tính, hoặc thậm chí là một đội máy tính, có thể chạy mãi mãi để kiểm tra tất cả các cách khác nhau của việc gán giá trị biến trong đó.

“Cố gắng làm điều này bằng cách thô tự nhiên sẽ mất đến khi vũ trụ kết thúc nếu bạn làm nó một cách ngây thơ,” Goddard nói. “Vì vậy, bạn cần một số đơn giản hóa tuyệt vời để đưa nó xuống một cái gì đó ngay cả khi có thể thực hiện được.”

Hơn nữa, mỗi khi bạn thêm một số vào vấn đề tô màu gói hàng, nó trở nên khó khăn khoảng 100 lần, do cách các tổ hợp có thể nhân lên. Điều này có nghĩa là nếu một nhóm máy tính hoạt động song song có thể loại bỏ 12 trong một ngày tính toán, họ sẽ cần 100 ngày thời gian tính toán để loại bỏ 13.

Heule và Subercaseaux coi việc mở rộng phương pháp tính toán bằng cách thô tự nhiên là điều thiếu văn hóa, theo một cách nào đó. “Chúng tôi có một số ý tưởng triển vọng, vì vậy chúng tôi chọn tư duy ‘Hãy cố gắng tối ưu hóa phương pháp của chúng tôi cho đến khi chúng ta có thể giải quyết vấn đề này trong thời gian ít hơn 48 giờ tính toán trên cụm máy,” Subercaseaux nói.

Để làm điều đó, họ phải nghĩ ra cách giới hạn số lượng tổ hợp mà cụm máy tính phải thử nghiệm.

“[Họ] không chỉ muốn giải quyết nó, mà còn muốn giải quyết nó một cách ấn tượng,” Alexander Soifer của Đại học Colorado, Colorado Springs nói.

Heule và Subercaseaux nhận ra rằng nhiều sự kết hợp về cơ bản là giống nhau. Nếu bạn đang cố gắng điền một ô hình kim cương với tám số khác nhau, không quan trọng nếu số đầu tiên bạn đặt là một lên và một sang phải so với ô trung tâm, hoặc một xuống và một sang trái so với ô trung tâm. Hai cách đặt này đối xứng với nhau và ràng buộc bước tiếp theo của bạn một cách chính xác giống nhau, vì vậy không có lý do gì bạn phải kiểm tra cả hai.

Heule và Subercaseaux thêm các quy tắc cho phép máy tính xem xét các kết hợp đối xứng như nhau, giảm thời gian tìm kiếm tổng cộng một cách đáng kể. Họ cũng sử dụng một kỹ thuật mà Heule đã phát triển trong công việc trước đó gọi là cube and conquer, cho phép họ kiểm tra nhiều kết hợp đồng thời trên các bộ máy tính khác nhau. Nếu bạn biết một ô cụ thể phải chứa một trong ba số 3, 5 hoặc 7, bạn có thể chia nhỏ vấn đề và kiểm tra mỗi trong ba khả năng đồng thời trên các bộ máy tính khác nhau.

Đến tháng 1 năm 2022, những cải tiến này cho phép Heule và Subercaseaux loại bỏ số 13 như là câu trả lời cho vấn đề tô màu gói trong một thử nghiệm mà chỉ mất dưới hai ngày thời gian tính toán. Điều này để lại cho họ hai câu trả lời có thể: 14 hoặc 15.

Một Điểm Cộng Lớn

Để loại bỏ số 14—và giải quyết vấn đề—Heule và Subercaseaux phải tìm thêm cách để tăng tốc tìm kiếm của máy tính.

Ban đầu, họ đã viết một công thức Boolean gán biến cho từng ô cá thể trong lưới. Nhưng vào tháng 9 năm 2022, họ nhận ra rằng họ không cần phải tiến hành từng ô một cách chi tiết. Thay vào đó, họ khám phá ra rằng việc xem xét các khu vực nhỏ gồm năm ô theo hình dạng của một dấu cộng là hiệu quả hơn.

Họ viết lại công thức Boolean của mình sao cho một số biến đại diện cho các câu hỏi như: Có phải có số 7 nào đó trong khu vực hình dạng dấu cộng này không? Máy tính không cần phải xác định chính xác nơi nào trong khu vực có thể có số 7. Nó chỉ cần xác định liệu nó có ở đó hay không—một câu hỏi mà cần ít tài nguyên tính toán hơn để trả lời.

“Việc có các biến chỉ nói về dấu cộng thay vì vị trí cụ thể đã cho kết quả tốt hơn nhiều so với việc nói về chúng trong các ô cụ thể,” Heule nói.

Với sự hiệu quả của tìm kiếm dấu cộng, Heule và Subercaseaux loại bỏ số 14 trong một thử nghiệm máy tính vào tháng 11 năm 2022, kết thúc nhanh hơn thời gian họ đã sử dụng để loại bỏ số 13. Họ dành bốn tháng tiếp theo xác nhận rằng kết luận của máy tính là chính xác—gần bằng thời gian họ đã dành để máy tính đạt đến kết luận đó ban đầu.

“Đó là một trải nghiệm hết sức đáng mừng khi nghĩ rằng điều chúng tôi đã tạo ra như một dạng câu hỏi phụ trong một số tạp chí ngẫu nhiên đã khiến nhóm người dành, như đã thấy, tháng rưỡi thời gian của họ để cố gắng giải quyết nó,” Goddard nói.

Với Subercaseaux, đó là chiến thắng đầu tiên thực sự trong sự nghiệp nghiên cứu của anh ấy. Và mặc dù nó có thể không phải là loại khám phá mà anh ấy đã mơ ước khi anh ấy lần đầu tiên nghĩ đến làm việc trong toán học, anh ấy thấy rằng cuối cùng, nó có những đạt được của riêng nó về mặt trí tuệ.

“Đó không phải là sự hiểu biết về hình thức mà bạn đưa cho tôi một bảng đen và tôi có thể cho bạn thấy tại sao nó là 15,” anh ấy nói. “Nhưng chúng tôi đã có được sự hiểu biết về cách ràng buộc của vấn đề hoạt động, về việc có tốt hơn là có một số 6 ở đây hoặc một số 7 ở đó. Chúng tôi đã có được rất nhiều sự hiểu biết trực giác.”

Chuyện gốc được in lại với sự cho phép từ Tạp chí Quanta, một tờ báo độc lập biên tập thuộc Quỹ Simons với nhiệm vụ là nâng cao sự hiểu biết của công chúng về khoa học bằng cách đưa tin về các tiến triển và xu hướng nghiên cứu trong toán học và các ngành khoa học tự nhiên và sinh học.