MiniZincでOR-Toolsを使いたいんじゃ！

なにこれ

MiniZinc で制約プログラミングして遊んでいたら Google の OR-Tools というのを見つけ、Google教信者なので飛びつくも、構文がゴチャゴチャだしせっかく覚えた MiniZinc の構文でやりたいんじゃ！と思ったらサポートされてるっぽくて喜んだのもつかの間、Step-By-Step の手順が見つからないので自力でギリ動くようにした話。

制約プログラミングって? Prolog みたいな? MiniZinc って? CSP? という話はしない。私もよく知らない。好きな SCP は 1934-JP です。

注意

本記事の方法は公式のガイド等に頼ったものではなく、Stack Overflow や他コミュニティで調べたものをつなぎ合わせたり独自に対処したものですので、正しいかどうかわかりません。

2022/05/21 追記
3.1.2. Adding Solvers — The MiniZinc Handbook 2.6.3 にソルバー追加方法がちゃんと書いてありました。

検証した環境

• OS: Windows 10 Home
• MiniZinc / MiniZinc IDE: 2.6.3
• OR-Tools: 9.3.10497

手順

MiniZinc をインストール

MiniZinc - Software

適当にインストールする。

The MiniZinc Handbook のチュートリアルにあるソースなどを使って、素の状態でちゃんと動くことを確認。

OR-Tools をダウンロード

google/or-tools の GitHub から、or-tools_flatzinc_VisualStudio2022-64bit_vx.x.xxxxx.zip をダウンロード。

ファイルの配置と設定

zipファイルの中身で必要なのは下記のみ。

• bin\fzn-or-tools.exe
• minizinc\minizinc\ortools\*.mzn
• minizinc\solvers\ortools.msc

※以降のファイル配置手順は、ソルバー構成ファイル(.msc)をIDEやコマンドで活用することと、MiniZinc のインストールフォルダ内にそれっぽく格納することを目的としたものです。つまり、自分で .msc ファイルを構成するとかその他の方法で利用する場合には不要です。一例としてお読みください。
なお下記手順のとおりにすると MiniZinc IDE で認識され、IDE から実行できるようになります。(スレッド数増やすのを忘れずにね)

MiniZinc のインストールフォルダ(C:\Program Files\MiniZinc\)以下に下記のように配置する。

• fzn-or-tools.exe を bin\ へ
• minizinc\minizinc\ortools\*.mzn を share\minizinc\ortools\ へ
• minizinc\solvers\ortools.msc を share\minizinc\solvers\ へ

.msc ファイルの中で 実行ファイル(.exe) と ライブラリ(*.mzn) を指定する場所があるので、実態に合わせて書き換える。ファイルパスは .msc ファイルからの相対パス。

File: ortools.msc
6:   "mznlib": "../ortools",
7:   "executable": "../../../bin/fzn-or-tools.exe",

これで OK! のはずだが、現在の環境ではエラーが発生する。

エラー

現環境では下記のエラーが発生する。

stdlib_ann:441-1.449-9:
MiniZinc: type error: function with the same type already defined in C:\Program Files\MiniZinc\share\minizinc\ortools\redefinitions-2.0.mzn:101.1-106.28
Process finished with non-zero exit code 1.
Finished in 237msec.

minizinc 2.6.3 and or-tools 9.3: annotation warm_start conflict? MiniZinc - Google グループ で質問している人がいるので、少なくとも世界で2人以上は直面している。

エラー回避

状況が改善するまではワークアラウンドで対処する。(非公式な方法)

エラーメッセージに記載のファイルパスと行番号から確認すると、 redefinitions-2.0.mzn の warm_start アノテーションが名前衝突しているらしい。
私は今のところ warm_start を使わないので、問題の部分をコメントアウトしてしまおう(乱暴)。

annotation warm_start_array( array[int] of ann: w );
% annotation warm_start( array[int] of var bool: x, array[int] of opt bool: v ) =
%     assert(index_sets_agree(x, v), "index sets of warm_start arguments don't agree",
%     let {
%         any: xx = [ x[i] | i in index_set(x) where occurs(v[i])];
%         any: vv = [ deopt(v[i]) | i in index_set(x) where occurs(v[i])];
%     } in warm_start(xx, vv));

% annotation warm_start( array[int] of var int: x, array[int] of opt int: v ) =
%     assert(index_sets_agree(x, v), "index sets of warm_start arguments don't agree",
%     let {
%         any: xx = [ x[i] | i in index_set(x) where occurs(v[i])];
%         any: vv = [ deopt(v[i]) | i in index_set(x) where occurs(v[i])];
%     } in warm_start(xx, vv));

引数違いで2つあるが、両方個別にどこかと衝突しているらしいので、ともにコメントアウトする。

これできちんと動くようになる。

そこまでして使った感想

練習で作っていた時間割を生成するプログラムが爆速になり、非常に満足。Google教信者としても気分がいい。