最適化 · 開発中
Aria-Opt
最適化モデルを Aria で一度書けば、ひとつのインターフェースの背後で MILP、QUBO、ナップサックのソルバーへ振り分けます。HiGHS、CBC、SCIP、GLPK、CP-SAT、自社のシミュレーテッド分岐マシン、そして Pisinger の厳密なナップサックアルゴリズム。
オープンソースの MILP と QUBO ソルバーをまたいで、ひとつのモデル記述を使いたいオペレーションズ・リサーチとクオンツのチームへ。
現状 動作しテスト済み: モデル IR、設定、ルーター、QUBO とナップサックへの変換、LP / MPS / QUBO エクスポート、総当たりオラクル。仕様のみで未実装: ソルバーアダプタ、シミュレーテッド分岐の積分器、DSL パーサー。
例
ナップサック問題を、最初から最後まで。
整数パラメータとデータファイルがモデルをインスタンス化します。ルーターがナップサックの形を認識し、厳密な Pisinger ソルバーへ送ります。表示している出力は、そのソルバーが完成したときの目標出力です。
-- aria: opt
maximize sum i from 0 to n - 1 { p[i] * x[i] }
subject to capacity: sum i from 0 to n - 1 { w[i] * x[i] } <= C
$ aria-opt solve knapsack.aria --model Knapsack --int n=8 \
--data knapsack_8.json
status OPTIMAL obj 1458 bound 1458 gap 0.000% [knapsack]なぜ Aria-Opt か
商用ソルバーを使ったことがあれば、なじみやすいはずです。
インターフェース
ひとつのインターフェース
すべてのソルバーが同じ Solver トレイトを実装します。呼び出し側がバックエンド固有の型を目にすることはありません。
設定
すでに知っているパラメータ名
time_limit、mip_gap、threads、seed など。ほかの一般的な表記もエイリアスとして受け付けます。未対応のパラメータは警告を出し、黙って意味が変わることはありません。
変換
ソルバーが見ているものが見える
コアで整数はビットに、制約はペナルティに変換され、その過程のレポートを確認できます。だから QUBO ソルバーと MILP ソルバーが同じモデルを解きます。
検証
すべての例に答え合わせ
同梱のすべての例にオラクルが付いています: 総当たり、動的計画法、またはソルバー間の一致。aria-opt verify が受け入れゲートです。
ソルバー
接続を進めているソルバー。
- MILP / CPHiGHS、COIN-OR CBC、SCIP、GLPK、OR-Tools CP-SAT。
- シミュレーテッド分岐変換後の QUBO 向けの断熱 (aSB)、弾道 (bSB)、離散 (dSB) SB。GPU 加速は後続で。
- ナップサック0-1 および有界ナップサック向けの Pisinger の expknap と minknap。
- QUBO ヒューリスティックシミュレーテッド・アニーリングとタブー探索、参照オラクルとしての総当たり (現在動作中)。