多くの難しいLeetCode問題は、実は簡単な制約充足問題
(buttondown.com)- LeetCodeの難問も、制約ソルバーを使えばずっと簡単に解ける
- 複雑な動的計画法や独自アルゴリズムの代わりに、MiniZincのような制約ソルバーを使うことで、数理最適化問題をシンプルに解決できる
- 従来のプログラミング言語では、この種の数理最適化問題を表現しにくいため、制約ベースのアプローチが強みを発揮する
- 例外ケースや追加の制約が出てきても、制約ソルバーではモデル変更を最小限に抑えられる
- 実行時の複雑さは手書きの最適化アルゴリズムより遅いことがあるが、柔軟性と開発生産性の面で多くの利点がある
制約ソルバーで解くLeetCode問題
正しい道具を選ぶ
-
筆者は大学卒業後の最初の面接で「コインのおつり問題」を出された
- コインの額面が与えられたとき、決められた金額を支払うために必要な最小のコイン枚数を求める問題
- 単純な貪欲アルゴリズムを使ったが、すべてのケースで最適解を保証できなかった
- 正解は動的計画法だが、それを実装できず面接に落ちた
-
しかし、自分でアルゴリズムを実装しなくても、MiniZincのような制約ソルバーを使えばとても簡単に解ける
-
例のコード:
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); -
オンラインで直接 MiniZincの例を実行 できる
-
ソルバーが段階的に最適解を見つけてくれる
-
さまざまな最適化問題・充足問題
- LeetCodeなどでよく出る数理最適化問題（目的関数の最大化・最小化と複数の制約を含む問題）は、
プログラミング言語で解こうとすると低レベルな実装のせいで難しくなるが、制約ソルバーには向いている - たとえば、次のような性質のさまざまな問題がこれに当てはまる
例1: 株式の最大利益問題
- 「リストで与えられた株価データから、1回買ってその後で売ることで得られる最大利益を求めよ」
- 従来は O(n²) のブルートフォースか O(n) の最適アルゴリズムが必要
- MiniZincでは次のように簡単な制約問題として定義できる
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;
例2: 特定の数の加減算で 0 を作る（充足問題）
- 「リスト内の3つの数を足したり引いたりして 0 を作れるか？」
- 最適値ではなく、充足可能な解が見つかればよい
- 制約ソルバーでは次のように表現できる
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;
例3: ヒストグラム内の最大長方形面積
- 「各棒の高さが与えられたヒストグラムで、作れる最大の長方形の面積を求めよ」
- 従来は複雑なアルゴリズムと多くの状態管理が必要
- 制約だけで簡潔に解法を記述できる
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)"]
制約ソルバーのアプローチは本当に優れているのか？
-
面接の場では、時間計算量などに関する質問に弱い
- 制約ソルバーは実行時間の予測が難しく、専用に最適化したアルゴリズムより一般に遅い
- それでも、誤って実装した低品質なアルゴリズムよりはましであり、ほとんどのプログラマが毎回最適解法を自力で書けるわけでもない
-
本当の強みは、新しい制約条件の追加に対する柔軟性にある
- たとえば株の例で、1回ではなく複数回の売買を許すように変更すると、アルゴリズムの複雑さは急増する
- MiniZincの制約モデルでは、少しコードを変えるだけで、はるかに複雑な要件を扱える
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)"];
-
オンライン上の制約問題の例は数独などパズル中心だが、実際にはビジネスロジックや最適化要件を持つ問題のほうが、より面白く実用的に使える
- たとえば symmetry breaking（対称性の除去）のような高度な最適化手法を適用できる可能性も高い
まだコメントはありません。