1 ポイント 投稿者 GN⁺ 2024-07-05 | 1件のコメント | WhatsAppで共有
  • 制約プログラミング(CP) は、離散最適化問題を手続き型コードではなく、変数・ドメイン・制約としてモデル化し、ソルバーに条件を満たす解を見つけさせる宣言型アプローチ
  • モデルの核となるのは、求めたい値である変数、取り得る値の範囲であるドメイン、変数間の関係を制限する制約であり、必要に応じて目的関数でより良い解を選べる
  • Alice、Bob、Carolのキャンディ代分担の例は、alldifferentmaximumminimizeを通じて、有効な解をより均等な解へ改善する流れを示している
  • 実践例では、Google OR-Toolsのオープンソースソルバー CP-SAT とPythonを使い、4人の従業員について7日間・3交代・2種類の役割の週間勤務表を作成する
  • 同じモデルに、週40時間の上限、授業スケジュール、一緒に働いてはいけない組み合わせ、週末勤務の均等配分、休暇希望、勤務数の差の最小化といった条件を段階的に追加できる

制約プログラミングの基本的な考え方

  • 制約プログラミング(CP) は、離散最適化問題を解くための宣言型パラダイム
  • 命令型プログラミングは結果に到達する手順を順番に書くが、宣言型では望む結果の条件を記述し、実行システムにその結果を見つけさせる
  • 成人の一覧を求める例では、命令型コードは人の一覧を走査して Age >= 18 を検査し、宣言型SQLは SELECT person_name FROM people WHERE age >= 18; のように条件を直接表現する
  • CPも望む結果をモデルとして記述し、中核となる構成要素は変数・ドメイン・制約
    • 変数は何を求めるかを表す
    • ドメインは変数が取り得る値の集合
    • 制約は変数間の関係を制限する

変数、ドメイン、制約、目的関数

  • 解とは、各変数が自分のドメイン内の値を取り、すべての制約を満たす割り当て
  • キャンディ代の例は、Alice、Bob、Carolがそれぞれ最大20ドルを持ち寄り、50ドルのキャンディを買うためにお金を集める問題
    • 変数 abc は各人が出す金額
    • 3つの変数のドメインは {0, ..., 20}
    • a + b + c == 50 で総額を合わせる
    • a >= b でAliceがBob以上の金額を出すようにする
    • c % 5 == 0 でCarolの金額を5の倍数に制限する
    • 3人が同じ金額を出さないように、a != ba != cb != c を置ける
  • 複数の変数にまたがる条件はグローバル制約(global constraints) として表現でき、alldifferent(a, b, c) は3つの変数がすべて異なる値を持つようにする
  • ソルバーはモデルを入力として受け取り、有効な解を返す
    • 例の解 a = 19b = 11c = 20 はすべての制約を満たす
    • ただしCarolがBobのほぼ2倍を出しているため、より均等な解があり得る
  • 目的関数は、制約を満たす解の中で特定の式を最小化または最大化する
    • 新しい変数 x を最大の分担額として置き、maximum(x, [a, b, c]) を使う
    • minimize: x を適用すると、a = 18b = 17c = 15x = 18 が返される
    • 最大分担額と最小分担額の差が9ドルから3ドルに縮まる

CP-SATとPythonで勤務表モデルを作る

  • 実践例は、小さな店舗の週間勤務表を生成する問題
    • 店は毎日午前8時から午後8時まで営業する
    • 1日はMorning、Afternoon、Eveningの3交代で、各交代は4時間
    • 役割はCashierとRestockerの2種類
    • 従業員はPhil、Emma、David、Rebeccaの4人
  • CP-SAT は、Google OR-Tools に含まれるオープンソースのCPソルバー
  • 空のモデルは ortools.sat.pythoncp_model.CpModel() で作成する
  • 従業員ごとに可能な役割は次のとおり
    • Phil: Restocker
    • Emma: Cashier、Restocker
    • David: Cashier、Restocker
    • Rebecca: Cashier
  • 勤務表は、従業員・役割・曜日・交代を組み合わせたブール変数で表現する
    • schedule["Emma"]["Restocker"]["Monday"]["Evening"] は、Emmaが月曜日の夕方交代にRestockerとして働くなら 1、そうでなければ 0
    • model.new_bool_var() はドメインが {0, 1} の変数を作る

基本的な勤務制約

  • レジ係はすべての時間帯にちょうど1人必要なため、各曜日・交代ごとにCashier役割の合計が 1 でなければならない
  • 在庫担当は1日に1交代だけ必要なため、各曜日のRestocker役割全体の合計を 1 とする
  • 前日のEveningの在庫担当交代と翌日のMorningの在庫担当交代が連続しないように、2つの割り当ての合計が 1 を超えないよう制限する
  • 1人の従業員が同じ交代で2つの役割を同時に担当することはできないため、従業員・曜日・交代ごとの役割合計は 1 以下でなければならない
  • 資格のない役割が割り当てられないよう、その従業員が担当できない役割の変数はすべて 0 に固定する
  • 1日の最大勤務は8時間、つまり2交代
    • MorningとEveningを同じ日に両方割り当てると、Afternoonの間に4時間の空き時間が生じる
    • 従業員・曜日ごとのMorningとEveningの割り当て合計を 1 以下に制限し、1日2交代超過と途中の空き時間を同時に防ぐ

ソルバーの実行と初期結果

  • モデルを解くときは cp_model.CpSolver() を作成し、solver.solve(model) を呼び出す
  • 解を得たら solver.value(...)schedule 変数の値を読む
  • 初期勤務表はすべての基本制約を満たすが、Rebeccaが1週間に14交代を担当する結果になる
  • 残業を避けるため、各従業員の週間勤務を最大40時間、つまり10交代に制限する制約を追加する
  • Philはフルタイムの学生なので、1週間にちょうど4交代だけ働き、平日のMorningとAfternoonは授業のため働けないようにする
  • PhilとEmmaが同じ交代で働かないように、各曜日・交代ごとに2人の割り当て合計を 1 以下に制限する
  • 全員が嫌がる週末勤務は、土曜日と日曜日の合計8交代を4人の従業員に2交代ずつ配分するよう制約を置く

解の状態: OPTIMAL、INFEASIBLE、FEASIBLE、UNKNOWN

  • ソルバーはモデルを入力として受け取り、状態と解を返す
  • OPTIMAL は、これ以上良い解が存在しない解を見つけたという意味
    • たとえば x + y >= 5x + y を最小化するとき、(x, y) = (5, 0) は最適解
    • (x, y) = (3, 2) も同じ目的値を持つため、最適解になり得る
  • INFEASIBLE は、変数にどう値を割り当てても制約を満たせないという意味
    • たとえば x ∈ {0, ..., 10} なのに x >= 15 を要求すると不可能
  • 大きな問題や複雑な目的関数のために時間制限でソルバーを中断すると、2つの状態が出ることがある
    • FEASIBLE: 制約を満たす解は見つかったが、最適かどうかは分からない
    • UNKNOWN: 解を見つけられず、解が存在するかどうかも分からない

休暇希望と公平な配分

  • Emmaが月曜日から金曜日まで休みたいという制約を追加すると、ソルバーの状態は INFEASIBLE になる
    • 他の制約を破らずに勤務表を埋められないため
  • Emmaが月曜日から水曜日までだけ休む条件に変えると、勤務表を作れる
    • Philは希望どおりちょうど4交代働く
    • Emmaは6交代、Davidは10交代、Rebeccaは8交代を担当する
  • Emma、David、Rebeccaの間の勤務数をより均等にするため、目的関数を追加する
    • 各従業員の総交代数を表す整数変数 total_shifts を作る
    • model.new_int_var(0, 10, ...) で0から10までの値を持つ整数変数を生成する
    • Philはパートタイムなので除外し、model.add_min_equality(...)model.add_max_equality(...) で最小・最大交代数を追跡する
    • model.minimize(max_shifts - min_shifts) で最大交代数と最小交代数の差を最小化する
  • 最終結果はPhilが4交代、Emmaが6交代、Davidが9交代、Rebeccaが9交代
    • Emmaは3日休むため6交代になる
    • DavidとRebeccaは同じ9交代で配分される

サンプルコードと次のトピック

  • このモデルは、店主の要件と従業員の希望を同時に満たす勤務表を生成する
  • 同じCPモデルに制約を追加し続けながら要求が可能かどうかを確認し、可能な解の中からより公平な配分を目的関数で見つけられる
  • サンプルコードは pganalyze GitHub で公開されている
  • 次の記事のテーマは、Postgresでインデックス選択に制約プログラミングを使う方法

1件のコメント

 
GN⁺ 2024-07-05
Hacker News の意見
  • 以前に制約条件ソルバーを使ったことがあるが、できることは本当に魔法のようだった。問題は、初心者が読める資料があまり多くないこと
    ほとんどは数独を解くもの(この分野の Hello World)か、ドメイン専門家だけを対象にした非常に技術的な一次研究文献
    残念なのは、こうしたツールがもっと利用しやすくなれば、ものすごく多くの問題を解けそうだから。ここで言う利用しやすさも、依然としてプログラマーが必要という意味であり、問題を制約条件 DSL に落とし込む作業は、たいていの人が得意にできる領域ではない

    • こうしたツールが十分に利用しやすくない理由は、ほとんどのソルバーが**混合整数計画法(MIP)**ベースで、ドメインを数式として書かなければならないからだと思う。そのため、ユーザーは制約条件を正しく書くには、ドメインと数学の両方を理解している必要がある
      ただし、ソルバーは MIP だけではない。局所探索ベースの制約条件ソルバーもあり、この方式にはすべての制約条件を整数変数間の関係や方程式としてモデル化しなければならないという制限がない
      局所探索ソルバーでは、制約条件をおおむね、ある解がどれだけ良いかを教えてくれるブラックボックスとして扱う。そのため、すべての可能な解を試さない限り最適解は保証しにくいが、妥当な時間内に準最適解を見つける傾向がある
      Timefold Solver は、こうした局所探索ベースのソルバーの一つ。ユーザーはドメインにアノテーションを付け、ソルバーが変数と取り得る値を把握できるようにする。そのため制約条件は int ではなく ShiftEmployee を扱い、それらのメソッドにもアクセスできる
      開示:Timefold Solver で働いている
    • まさにその通り。制約条件ソルバーの実際の文法や API は非常に単純で、すぐに学べる。本当に時間と専門性が必要なのは、この方法で問題をモデル化する部分だが、参考にできる実規模・実複雑度の例はほぼゼロに近い
      MiniZinc でスケジューリング問題を解いた経験が5年ほどあるが、残念ながらそのコードはすべて非公開で、オープンソースとして公開されることはない
      コンテナ化、可視化、モデリングまで含む完成形の制約プログラミング例を作ってみたいが、実際に解く価値があり、利用可能なオープンソースデータがある問題を見つけることが障壁になっている
    • 理論そのものよりも**還元(reduction)**のほうがはるかに難しいという点に同意する。Dennis Yurichev の「SAT/SMT by Example」(https://smt.st/) はこのテーマの良い資料だが、かなり圧倒される
    • 「ほとんどの資料は数独を解くものか、ドメイン専門家向けの研究文献」という指摘は正確。ルールエンジンに SAT ソルバーを使おうとしたが、どう使えばよいのかまったく見当がつかなかった
      かなり推論した末に基本的な概念実証は作れたが、実際に必要なレベルまで拡張できなかった。おもちゃの実装と、それより実用的なものとの間には非常に大きな隔たりがあった
    • 長くコードを書いてきたが、今は少し勘が鈍っている。昨年、Google の OR-Tools でサッカーチーム最適化ツールを作った。友人と一緒にする、といった選択制約や、チーム間の実力バランスを取る条件があった
      LLM は、おおよそ正しい方向へかなり素早く連れていってくれる点で役に立った。今のところ正確に当てることには失敗するが、その後の残りを自分で仕上げられる程度には十分助けてくれた
  • このすべての核心は、何かをソルバーに渡せる形にモデル化する方法を学ぶことにある。その次は、出てきた解を人間が理解できる形で表現する方法
    残念なのは、ほとんどのプログラムがデータを一つの表現だけで保持しようとしており、この考え方とは逆に進んでいる点。たいていの場合、そのやり方は合理的ではなく、アルゴリズムを新しい表現に合わせるために多くのねじれが生じる
    この記事も序盤で宣言型に短く触れながら、この点を扱っている。自分のコードが表現間の変換をもっと頻繁に行っていないことを、いつも後悔している。そうすれば非常に簡潔な表現が得られ、簡潔になったことでさらに速くなるという二重の利点も得られる
    もちろん、これは結局、多くのデータパイプラインを説明する言葉だということは分かっている。時間の大半をデータ変換と複数の計算場所への分岐に費やす構造だ

  • 以前書いた本のうち、現在書き直している本に、Python で MiniZinc を使う短い章がある: https://leanpub.com/pythonai/read#constraint-programming-wit...
    MiniZinc は制約プログラミングシステム。MiniZinc を使う良い Coursera 講座もある

    • Coursera 講座へのリンクがあるか知りたい
  • 計量経済学を学んだ後、2000年代初頭のオペレーションズリサーチの修士課程でソルバーを多用した。今は Python を使う Web ソフトウェアの仕事をしているので、このテーマの深い記事を見られてうれしい
    このテーマが好きで、記事を読んで多くの記憶がよみがえった。制約条件をモデル(変数、構造など)に移す作業が仕事の90%で、最も難しい部分だということも改めて実感した

    • 修士のときに GAMS というプログラムを使った
      構文構造は完全な自由形式
      https://www.gams.com/latest/docs/UG_GAMSPrograms.html#UG_GAM...
    • 制約条件をモデルに移すには LLM がかなり役立つ可能性がある。LLM から制約モデルへ変換するアダプターを試してみたいと思っていた
      かなり簡単に取れる果実のように見えるが、ほかの人にも恩恵があるのかは気になる
    • 最も難しい部分は、本番環境で問題を最小化しながら回すことだと思う。スケールさせ、データの変化に堅牢にするには時間がかかる
  • 子ども向けスポーツキャンプを運営している顧客がいる。子どもたちは、やりたいスポーツや同じクラスになりたい友だちをリクエストできる。
    そのため、人手では解きにくいスケジューリング問題が発生し、以前は毎年この作業に数週間分の人員が投入されていた。顧客のデータを OR-Tools ベースのオプティマイザにつなぐ簡単なシステムを作ったところ、今では数回クリックするだけでスケジューリングが完了する。

    • その通り。データ、制約条件、効用関数をシステムにきちんと入れておけば、十分に良い解を非常に高速に大量に見つけられる。
      バスケットボールリーグのコーチをしていて、8つのピリオドがある。どの選手も、他の選手より2ピリオド以上多く出場してはならない。1試合あたり可能なラインアップ数は、出場時間の制約を満たしつつも天文学的に多い。
      制約を満たすラインアップの組み合わせを見つけるのはとても簡単だが、最適または準最適なラインアップの組み合わせを見つけるのは非常に難しい。遅れて来る選手や、何も言わずに欠席する選手を反映しなければならないとなると、さらに面白くなる。
      *常に完全に可能というわけではない
    • これをどう実現したのか詳しく書いたブログ記事は、間違いなく大人気になるはず。
  • 主に制約条件ソルバーとして動作するパラメトリック CADがあるのか気になる。
    最初は気にしないパラメータ値を適当に推定しなければならないことがあまりに多く、煩わしく感じる。関心のあるパラメータを制約として置き、残りを最適化できるとよいのだが。

  • この方式は混合整数計画法と比べてどうなのか気になる。物理問題ではどうだろう。

    • 多くの問題はどちらの方式でも定式化できる。MILP には常に目的関数があり、制約条件は常に決定変数の線形結合である。
      Gurobi は信じられないほど高速なので、解を得るために、多少無理をしてでも問題を MILP に押し込む価値があるかもしれない。
    • CP-SAT は整数専用なので、物理にはあまり向いていないと思う。実数をスケーリングすることはできるが、浮動小数点を直接扱うほど良くはない。
      CP-SAT の利点は、ブール変数や整数変数および制約条件を MIP ソルバーよりはるかに効率よく扱える点で、特に all_different のような高水準の制約で顕著だ。
    • 大まかには似ていると推測している。https://www.amazon.com/gp/product/1107658799/ がこのテーマで最後に読んだ本だが、同じアイデアを多く扱っている。
      特に、この記事で何らかの値を最小化しようとしている部分は、同じ内容を直接書いているのだと思う。