6 điểm bởi GN⁺ 2025-09-13 | Chưa có bình luận nào. | Chia sẻ qua WhatsApp
  • Ngay cả các bài LeetCode khó cũng có thể được giải dễ hơn nhiều nếu dùng constraint solver
  • Thay vì quy hoạch động phức tạp hay tự viết thuật toán, có thể dùng constraint solver như MiniZinc để giải các bài toán tối ưu toán học một cách đơn giản
  • Các ngôn ngữ lập trình truyền thống khó biểu đạt những bài toán tối ưu toán học kiểu này, vì vậy cách tiếp cận dựa trên ràng buộc có lợi thế rõ rệt
  • Ngay cả khi xuất hiện trường hợp ngoại lệ hoặc ràng buộc bổ sung, việc chỉnh sửa mô hình trong constraint solver cũng là tối thiểu
  • Độ phức tạp thời gian chạy có thể chậm hơn thuật toán tối ưu tự viết, nhưng xét về tính linh hoạt và năng suất phát triển thì có rất nhiều ưu điểm

Các bài LeetCode giải bằng constraint solver

Chọn đúng công cụ

  • Tác giả đã gặp bài toán “coin change” trong buổi phỏng vấn đầu tiên sau khi tốt nghiệp đại học

    • Khi đã cho các mệnh giá xu, cần tìm số lượng xu tối thiểu để trả lại đúng một số tiền nhất định
    • Tác giả dùng một thuật toán tham lam đơn giản, nhưng không đảm bảo nghiệm tối ưu trong mọi trường hợp
    • Quy hoạch động mới là đáp án đúng, nhưng vì không cài đặt được nên đã trượt phỏng vấn
  • Tuy nhiên, nếu không tự cài đặt thuật toán mà dùng constraint solver như MiniZinc thì có thể giải rất dễ

    • Mã ví dụ:

      int: total;
      array[int] of int: values = [10, 9, 1];
      array[index_set(values)] of var 0..: coins;
      
      constraint sum (c in index_set(coins)) (coins[c] * values[c]) == total;
      solve minimize sum(coins);
      
    • Có thể trực tiếp chạy thử ví dụ MiniZinc trên web

    • Solver sẽ dần dần tìm nghiệm tối ưu

Nhiều loại bài toán tối ưu/thỏa mãn khác nhau

  • Những bài toán tối ưu toán học thường gặp trên LeetCode v.v. (có hàm mục tiêu cực đại/cực tiểu và nhiều ràng buộc)
    khi giải bằng ngôn ngữ lập trình thì khó vì phải cài đặt ở mức thấp, nhưng lại rất phù hợp với constraint solver
  • Ví dụ, nhiều bài toán có tính chất như dưới đây đều thuộc nhóm này

Ví dụ 1: Bài toán lợi nhuận cổ phiếu tối đa

  • “Từ danh sách giá cổ phiếu, hãy tìm lợi nhuận lớn nhất có thể đạt được bằng cách mua một lần rồi bán vào thời điểm sau đó”
    • Theo cách truyền thống cần brute force O(n²) hoặc thuật toán tối ưu O(n)
    • Trong MiniZinc, có thể định nghĩa ngắn gọn như một bài toán ràng buộc như sau
      array[int] of int: prices = [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5, 8];
      var int: buy;
      var int: sell;
      var int: profit = prices[sell] - prices[buy];
      
      constraint sell > buy;
      constraint profit > 0;
      solve maximize profit;
      

Ví dụ 2: Cộng/trừ các số để tạo thành 0 (bài toán thỏa mãn)

  • “Có thể cộng hoặc trừ ba số trong danh sách để tạo thành 0 hay không?”
    • Chỉ cần tìm một nghiệm thỏa mãn, không phải giá trị tối ưu
    • Có thể biểu diễn trong constraint solver như sau
      include "globals.mzn";
      array[int] of int: numbers = [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5, 8];
      array[index_set(numbers)] of var {0, -1, 1}: choices;
      
      constraint sum(n in index_set(numbers)) (numbers[n] * choices[n]) = 0;
      constraint count(choices, -1) + count(choices, 1) = 3;
      solve satisfy;
      

Ví dụ 3: Diện tích hình chữ nhật lớn nhất trong histogram

  • “Trong một histogram có chiều cao từng cột đã cho, hãy tìm diện tích hình chữ nhật lớn nhất có thể tạo được”
    • Theo cách truyền thống cần thuật toán phức tạp và quản lý nhiều trạng thái
    • Chỉ bằng các ràng buộc cũng có thể mô tả lời giải một cách ngắn gọn
      array[int] of int: numbers = [2,1,5,6,2,3];
      
      var 1..length(numbers): x; 
      var 1..length(numbers): dx;
      var 1..: y;
      
      constraint x + dx <= length(numbers);
      constraint forall (i in x..(x+dx)) (y <= numbers[i]);
      
      var int: area = (dx+1)*y;
      solve maximize area;
      
      output ["(\(x)->\(x+dx))*\(y) = \(area)"]
      

Cách tiếp cận bằng constraint solver có tốt hơn không?

  • Trong phỏng vấn, cách này có điểm yếu nếu bị hỏi về độ phức tạp thời gian

    • Constraint solver khó dự đoán thời gian chạy, và thường chậm hơn thuật toán tối ưu viết riêng
    • Tuy vậy, nó vẫn tốt hơn một thuật toán chất lượng thấp được cài đặt sai, và với đa số lập trình viên thì việc tự viết nghiệm tối ưu mỗi lần không hề dễ
  • Điểm mạnh thực sự là tính linh hoạt khi thêm các ràng buộc mới

    • Ví dụ, trong bài toán cổ phiếu, nếu đổi từ mua bán một lần sang mua bán nhiều lần thì độ phức tạp thuật toán sẽ tăng vọt
    • Nhưng trong mô hình ràng buộc của MiniZinc, chỉ cần chỉnh sửa mã rất ít là có thể đáp ứng các yêu cầu phức tạp hơn nhiều
      include "globals.mzn";
      int: max_sales = 3;
      int: max_hold = 2;
      array[int] of int: prices = [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5, 8];
      array [1..max_sales] of var int: buy;
      array [1..max_sales] of var int: sell;
      array [index_set(prices)] of var 0..max_hold: stocks_held;
      var int: profit = sum(s in 1..max_sales) (prices[sell[s]] - prices[buy[s]]);
      
      constraint forall (s in 1..max_sales) (sell[s] > buy[s]);
      constraint profit > 0;
      
      constraint forall(i in index_set(prices)) (stocks_held[i] = (count(s in 1..max_sales) (buy[s] <= i) - count(s in 1..max_sales) (sell[s] <= i)));
      constraint alldifferent(buy ++ sell);
      solve maximize profit;
      
      output ["buy at \(buy)\n", "sell at \(sell)\n", "for \(profit)"];
      
  • Các ví dụ bài toán ràng buộc trên mạng thường tập trung vào puzzle như Sudoku, nhưng trên thực tế chúng có thể được dùng thú vị và thực dụng hơn cho logic nghiệp vụ hoặc yêu cầu tối ưu hóa

    • Ví dụ, cũng có nhiều khả năng áp dụng các kỹ thuật tối ưu nâng cao như symmetry breaking

Kết lại và tham khảo

  • Bài viết này là một phần trong newsletter hằng tuần của tác giả, bàn về lịch sử phần mềm, phương pháp hình thức, công nghệ mới và lý thuyết kỹ nghệ phần mềm
  • Nếu quan tâm, có thể đăng ký hoặc xem website chính của tác giả
  • Cuốn sách mới của tác giả, "Logic for Programmers", cũng đang được phát hành

Chưa có bình luận nào.

Chưa có bình luận nào.