多くの難しいLeetCode問題は、実は簡単な制約充足問題

 (buttondown.com)
6 ポイント 投稿者 GN⁺ 2025-09-13 | 2件のコメント | WhatsAppで共有
  • 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（対称性の除去）のような高度な最適化手法を適用できる可能性も高い

まとめと参考

  • この記事は著者の週刊ニュースレターで、ソフトウェアの歴史、形式手法、新しい技術、ソフトウェア工学の理論を扱っている
  • 興味があれば 購読 または著者の メインウェブサイト を参照できる
  • 著者の新刊 "Logic for Programmers" も刊行中

関連記事

2件のコメント

 
kohs100 2025-09-15

普通、アルゴリズムの問題って時間・空間計算量の条件が付いていませんか？ 制約条件ソルバーで解けるというのは、結局のところ問題を制約式に変換する能力しか示せないわけで……。それが果たして実務で必要な能力なのかは、正直よく分かりませんね……
 
GN⁺ 2025-09-13
Hacker Newsの意見

  • Leetcode型の面接質問の最大の問題は、追加の説明を求められないことだと思う。自分の考え方が一般的なものと違うせいで、Leetcodeは正解を暗記する方向に依存しているように感じる。十分な文脈がある問題なら現実的に理解できるので問題ないが、ほとんどは説明不足で問題を正しく把握できない。だから最近はLeetcodeやAI自動化面接の段階は最初から断っている。課題や1対1、画面共有インタビューは大丈夫。Leetcodeのサイトにきちんとした解説と正答があれば独学もしやすいだろうが、実際には難しすぎる。単なる実力の問題ではなく、自分の思考方式と問題タイプの相性が合わない。質問もできない状態で選択式問題ばかり解かされるのは、失敗するように設計されたシステムのように思える。特に事前面接用のAI/Leetcode型問題を対象に話している。実際に人がいる面接で質問のやり取りができる環境は十分良いものだと思う

    • LC(Leetcode)面接は、訓練された100m走のスピードを測るのに近い。実際の仕事は、何度も立ち止まって戻りながら進む長いマラソンのようなものだ。それでも今はSMEGMAのような大企業で高い給料を得るには、こういうゲームをやらなければならない。たとえば自分は2Dゲームエンジンを自作したが、LCハード問題を何問も、しかもバックフリップまでしながら解けないと通らないようなLC面接は無理だと思う。もうそれは受け入れている。自作エンジン

    • 解法を暗記すればそれで済むというわけではない。暗記していても追加質問で詰まることはある。ただ、暗記したうえで追加質問もうまく解けるなら、Leetcodeスタイルの問題に対応できていると言ってよいと思う。問題解決力とはパターンマッチング能力であり、多くのパターンを知るほど問題解決力は高くなる。今ではGPTが問題も解いて解説もしてくれるので、こうした能力は以前より身につけやすい。今からでも身につけた方がいいと思う

    • 本当に共感する。自分も最近の面接で、課題は最高評価をもらい、エンジニアたちやCEOからの印象も良かったのに、CTOが突然ライブコーディング面接を入れてきて、結局落とされた。11週間にわたる面接が無駄になった。このばかげたプロセスがまだ残っていることにうんざりする。自分がやったデモ/課題はこちらのmonumentalリンクと成果物、GitHubコード

    • 明確な質問ができないこと自体が、実際に検証したい能力なのではないかとも思う。候補者が問題解決時にどうアプローチするかを見るためだ。もし人々に断定的なやり方しか取らせないなら、あらゆるソフトウェアはむしろ複雑でひどいものになってしまう。本当に難しいのはコードを数行書くことではなく、問題を解く過程だ

    • 自分が面接した会社では、LC問題を1〜2問出す場合でも、説明を求めたらすぐリアルタイムの会話とコーディングに移行した。こうすると欠点として、リアルタイムのライブコーディングによる心理的負担が大きくなる

  • こういう面接問題を受けると、制約ソルバーを「使う」ことではなく、限定された問題に合わせた制約ソルバーを「自分で実装する」ことを求められているように感じる

    • その通り。だからこういう面接アプローチは根本的に雑だと思う。実際のエンジニアリングでは、コーヒーを飲み、論文を読み、図書館を調べ、散歩しながら考え、既存のツール（制約ソルバーやLLM）を参照して問題を100%解ける。でも面接では0%も解けない気がする。こういう面接をする会社に入りたいと思ったことすらない

    • まさにそう。NP問題の大半は制約問題に変換できる。実際に制約ソルバーが正解になるかどうかは適用領域に強く依存するし、面接の場ではほぼ正解ではない。こうしたソルバーは単純な動的計画法よりずっと遅いことも多い

    • 会社によってはそういう面接もあるが、そうでないところも多い。一般にLCを面接で使うのは、一つの理由（非効率な採用プロセスのせい）だけで使われていることが多かった。参加者自身も仕組みの刷新が必要だと分かっているが、権限がないか、権限が分散しすぎていて変えられない。大企業ではHRが「標準化」のために同じ質問を複数チームに回すことがあるし、小さな会社は独自問題を用意する時間がなくてネットから拾ってくる。こういう場合、技術面接官自身もLC面接に批判的で、実際には光る候補者を見つけようと努めている。そういう環境では、制約ソルバーへの関心や知識があることを示すだけでもかなり高評価になることがある

    • 誰かがLCハード問題を制約ソルバーで解いたのに採用されないなら、それは面接官の方が愚かだ。制約ソルバーが何かを理解し、問題を定義して使える人自体が非常に少ない。自分も3年生のときに使ったが、制約式を書くこと自体が頭痛がするほど複雑な作業だった

    • この点は当たっている部分もあればそうでない部分もある。自分は面接でこういう質問をしたことがあり、候補者が制約ソルバーを思いついたら高評価を付けていた。実務エンジニアリングにおいて制約ソルバーは過小評価されており、適切な答えをすばやく出せるかどうかを示す指標になる。もちろんその後、本当のコーディング力を把握するためのホワイトボード質問は続けるだろう。しかし回答として制約ソルバーを提示すること自体は悪くないと判断する

  • 面白い洞察ではあるが、現実の面接にはあまり合わないと思う。こうした問題の核心は、候補者に「頭を使う」能力があるかを検証したい点にある。ただ制約式で解くのでは、経験や知識のレベルしか示せず、「頭を使ったか」は見えてこない

    • 面接官はLeetcodeの「Top Interview 150」にある「Array String」問題をよく出す傾向がある。自分のようなバックエンドのPython開発者からすると、その手の問題は普段の仕事とかけ離れていると感じる。大半がin-placeな配列操作アルゴリズムを要求するが、これはたいていCやRustのような性能重視の言語でしか必要にならない。むしろ「Hashmap」系の問題の方が、言語に合った道具の使い方を示すのに役立つ。また、難易度調整ができていない問題も多く、「Easy」扱いの問題（たとえばMajority Element）が、実際には歴史あるアルゴリズム（Boyer–Moore）を要求する水準だったりする。「Easy」と呼ぶには無理がある

    • 最近Metaで受けた最終ラウンドは、ひたすら彼ら特有の問題をどれだけ繰り返し暗記したかを確認する場だった。だから教科書的な答えと違う返答をすると、かえって戸惑われる。「賢さ」そのものはあまり重要視されていない気がした

    • ボトムアップDPアルゴリズムはある程度頭を使う必要があるが、大半の問題はトップダウン方式（再帰+メモ化）で解ける。たとえばコインチェンジ問題はA*探索の方がうまく解けることもある。しかし現実には、ほとんどのプログラマーがこうしたアルゴリズムを本当に使う機会はほぼない。本当に重要なのは、うっかり時間計算量O(n^2)のコードを書いてしまっていることに気づけるかどうかだ。accidentallyquadratic.tumblr.comを見れば、有名プロジェクトの優秀な人たちですらこうしたミスをよくしている。だから、テストでアルゴリズムを作る能力と、実務でアルゴリズム上のミスを見抜く能力は別物だ

    • 自分は面接で問題解決力を検証するとき、思考過程、コミュニケーションの仕方、問題の分解を重視する。難易度を調整できる質問を用意して、すべての候補者が自分の能力を示せる機会を持てるようにする方がずっと重要だ。思いついた答えをすぐ叫ぶか、長く詰まるかだけでは、面接官の立場から短時間で分かることはほとんどない。だから問題解決型の面接質問は非常に有用になり得るが、現実にはあまりうまく使われていないのが残念だ

    • こういう問題は本当に「賢さ」を測っているのではなく、12種類ほどの定型パターンをどれだけ暗記したかを試しているにすぎない。ほとんどすべての候補者が、創造的な問題解決ではなく準備してきた暗記力によって合否が決まる。LeetCode問題はあまりにもゲーム化されていて、準備する意思があるかどうかを見る手段になっているように感じる

  • たいていの面接は、「もし糖尿病患者が自宅で自分でインスリンを合成できなければ、人生ゲームで不正だ」とでも言いたげな前提で問題を出しているように思える。妻が血糖値が上がればインスリンを打つように、制約問題ならソルバーを使うのが正しい。会社が制約ソルバーのソフトウェアを作っているのでない限り、なぜわざわざ「そんなソフトウェアは存在しない」という前提を置いて、一から作り直させるのか分からない

    • 要するに、危機の際にインスリンを合成する能力を試しているのではなく、1週間で教本を暗記して電話面接でうまく唱えられるかを評価する事前適性テストだ

    • 制約ソルバーで効率よく問題を解く方法を見つけられるなら、forループを二つほどと補助の再帰関数くらいは簡単に書けるし、おもちゃのような問題なら全部解ける

    • （意味のある内容なし）

    • コーディングテストを擁護すると、簡単なDP問題すら解けない人は、実務でも力不足なことが多かった。もちろん例外はあるだろうが、自分の経験ではそうだった

  • 制約プログラミング言語の話が出たら、いつもHåkan Kjellerstrandに触れるべきだ。MiniZincを含む膨大な例題と問題集をまとめた素晴らしいサイトを運営している。hakank minizinc

    • しかも彼は良いWebサイトを作っただけでなく、実際にとても親切な人でもある

  • かなり昔、大学の計算機科学の課程で制約ソルバーを学んでいない青二才だったころ、スポーツクラブのスケジュール作成アプリを作ってくれと友人に頼まれてこの問題に出会った。最初は簡単そうに見えたが、実際に取り組んでみると自分がとんでもない問題にぶつかっていることに気づいていなかった。後になって、自分の傲慢さへの良い教訓だったと分かったし、その経験はスケジュール、締切、期待値の話をするときに大いに役立っている

    • 初歩的な質問かもしれないが、制約ソルバーの代わりに「線形最適化」でより簡単に解けるのではないかと気になる。自分で使った経験では、線形最適化はルール同士の衝突を重みとして扱い、最小限の「副作用」で済む方向に解を探せるのが利点だ

    • 25年前、高校生のころ、TI-BasicとVB6を学び始めたばかりの時期に、ハンバーガー店でアルバイトをしていた。マネージャーが毎週スタッフのシフトを組むのが大変だとこぼしているのを聞いて、「自分コンピュータちょっと分かるんで、スケジューリングプログラム作りますよ！」と言った。だがすぐに、スケジューラを作るのがどれほど難しいかを思い知って、あっさり断念した

  • 「こういう問題を面接で出すと、候補者が『このアルゴリズムの実行時間計算量は？』と聞いたときに答えに窮する、というのが著者の主張だ」。つまり、制約ソルバーも十分に速く解けないならLeetcodeハード問題の答えにはならない。実行時間要件が緩ければ単純な方法でも通るかもしれないが、効率的な解法を見つけること自体が挑戦の大きな部分だ

    • 実務では常に「最も効率的な解法」よりも、「新しい要求に素早く対応する解決策を考案すること」の方が多く求められる。だから、現実とかけ離れた効率性基準の面接に意味があるのか疑問だ（役割によっては違うかもしれない）。最も効率的な解法が、実際の業務能力を反映していないこともあり得る、という著者の見方に同意する。Leetcode批判の一つの文脈もそこにある。同じ問題でも、「新しい要求にどれだけ柔軟に対応できるか」という観点で見た方が、より客観的だ

  • 制約ソルバー？ 良いアイデアだし聞いたこともある。でも面接では、単にPythonで自分で実装してみせながら思考の流れを見たい、というのが現実だと思う。（面接で制約ソルバーを使うと説得するのは、ほぼ不可能だと感じる）

    • 実際にそういう話を面接官にしたことがあるのか、それともただの予想なのか気になる

    • import z3

  • DP（動的計画法）で解いたあとに、「今度は制約ソルバーでもやってみます」と言えば即採用だ

    • +1

  • 制約ソルバーの本当の強みは、「新しい要件」にどれだけ容易に対応できるかにある。自分もGoogleでデータセンター最適化をしていたとき、こうした汎用ソルバーが要件変更に柔軟に追従できる恩恵を大いに実感した