原著: The MiniZinc Handbook -> 2. A MiniZinc Tutorial -> 2.1. Basic Modelling in MiniZinc
License: Creative Commons Attribution-NoDerivatives 4.0 International License http://creativecommons.org/licenses/by-nd/4.0/
ほぼ自動翻訳によるもので内容は正確ではありません。正確な情報は原著を参照してください。
2.1. Basic Modelling in MiniZinc
ここでは、2つの簡単な例を用いて、MiniZincモデルの基本構造を紹介します。
2.1.1. Our First Example
Fig. 2.1.1 Australian states
最初の例として、図2.1.1に示すようなオーストラリアの地図に色を付けたいとします。この地図は、7つの異なる州と準州で構成されており、それぞれの州と準州に色を付けて、隣接する地域が異なる色になるようにしなければなりません。
Listing 2.1.1 A MiniZinc model aust.mzn for colouring the states and territories in Australia
% Colouring Australia using nc colours
int: nc = 3;
var 1..nc: wa; var 1..nc: nt; var 1..nc: sa; var 1..nc: q;
var 1..nc: nsw; var 1..nc: v; var 1..nc: t;
constraint wa != nt;
constraint wa != sa;
constraint nt != sa;
constraint nt != q;
constraint sa != q;
constraint sa != nsw;
constraint sa != v;
constraint q != nsw;
constraint nsw != v;
solve satisfy;
output ["wa=\(wa)\t nt=\(nt)\t sa=\(sa)\n",
"q=\(q)\t nsw=\(nsw)\t v=\(v)\n",
"t=", show(t), "\n"];
この問題は、MiniZincで非常に簡単にモデル化することができます。そのモデルをリスト2.1.1に示します。モデルの最初の行はコメントです。コメントは、行の残りの部分がコメントであることを示す%で始まります。MiniZincには、/*で始まり*/で終わるC言語スタイルのブロックコメントもあります。
次の部分では、モデルの変数を宣言しています。
int: nc = 3;
この行では、問題のパラメータとして、使用する色の数を指定しています。パラメータは、ほとんどのプログラミング言語における（定数）変数に似ています。宣言し、型を与えなければなりません。この例ではint型です。パラメータには、代入によって値が与えられます。MiniZincでは、代入を宣言の一部として含めることも（上の行のように）、別の代入文にすることもできます。したがって、以下は上記の1行と同じです。
int: nc;
nc = 3;
多くのプログラミング言語の変数とは異なり、パラメータには1つの値しか与えることができないため、定数と呼ばれています。1つのパラメータが複数代入されることはエラーとなります。
基本的なパラメータの型は、整数(int)、浮動小数点数(float)、ブール型(bool)、文字列(string)です。また、配列や集合(set)もサポートされています。
MiniZincモデルは、決定変数(decision variable)と呼ばれる別の種類の変数を含むこともできます。決定変数は、数学的または論理的変数の意味での変数です。標準的なプログラミング言語のパラメータや変数とは異なり、モデラーは変数に値を与える必要はありません。むしろ、決定変数の値は未知であり、MiniZincモデルが実行されて初めて、解法システムは、決定変数にモデル内の制約を満たす値を割り当てることができるかどうか、可能であればそれは何であるかを決定します。
このモデルの例では、各地域のwa, nt, sa, q, nsw, v, tに決定変数を関連付けていますが、これは地域を埋めるために使用される（未知の）色を表しています。
各決定変数には、その変数が取り得る値のセットを与える必要があります。これは、変数のドメイン(variable’s domain)と呼ばれます。これは、変数宣言の一部として与えられ、決定変数のタイプは、ドメイン内の値のタイプから推測されます。
MiniZincでは、決定変数はブール(bool)、整数(int)、浮動小数点数(float)、または集合(set)です。また、決定変数を要素とする配列もサポートされています。MiniZincのモデルでは、異なる色をモデル化するために整数を使用しています。したがって、各決定変数はvar宣言を使用して、集合 $\{1,2, \ldots ,nc\}$ を示す整数の範囲表現であるドメイン 1..nc を持つように宣言されます。値の型は整数なので、モデル内のすべての変数は整数の決定変数です。
識別子(Identifiers)
パラメータや変数の名前に使われる識別子は、アルファベットの小文字と大文字、数字、アンダースコア_の文字の組み合わせで構成されています。識別子はアルファベットで始まる必要があります。したがって、myName_2は有効な識別子です。MiniZincのキーワードは識別子名として使用することはできず、それらはIdentifiersに記載されています。MiniZincの演算子は、識別子名として使用することはできません。
MiniZincは、2種類のモデル変数（パラメータと決定変数）を慎重に区別します。決定変数を使って構築できる式の種類は、パラメータを使って構築できる式よりも制限されています。しかし、決定変数を使用できる場所では、同じタイプのパラメータを使用することができます。
整数変数宣言(Integer Variable Declarations)
整数のパラメータ変数は、次のいずれかとして宣言されます。
int : <var-name>
<l> .. <u> : <var-name>
<l>と<u>は固定整数表現です。
整数の決定変数は、次のいずれかとして宣言されます。
var int : <var-name>
var <l>..<u> : <var-name>
<l>と<u>は固定整数表現です。
形式的には、パラメータ(parameters)と決定変数(decision variables)の区別は、変数のインスタンス化と呼ばれます。変数のインスタンス化と型の組み合わせは、type-instと呼ばれます。MiniZincを使い始めると、間違いなくtype-instのエラーの例を見ることになるでしょう。
モデルの次の構成要素は、制約です。これらは、モデルの有効なソリューションであるために、決定変数が満たさなければならないブール式を指定します。このケースでは、決定変数の間にいくつかの等しくない制約があり、2つの州が隣接している場合、異なる色でなければならないことを強制しています。
関係(比較?)演算子(Relational Operators)
MiniZincは、Relational演算子を提供しています。
等しい(=または==)、等しくない(!=)、less than(<)、greater than(>)、 less than or equal(<=)、greater than or equal(>=)。
次の行
solve satisfy;
は、それがどのような問題であるかを示しています。この場合は充足問題です。つまり制約を満たす決定変数の値を見つけたいということです。どの決定変数か指定は不要です。
モデルの最後の部分はoutput文です。これは、モデルが実行され、解が見つかったときに何を出力するかをMiniZincに伝えます。
出力と文字列(Output and Strings)
出力文の後には、文字列のリストが続きます。文字列は、二重引用符で囲まれたC言語のような特殊文字表記の文字列リテラルか、show(e)という形式の式（eはMiniZincの式）で表されます。この例では、\nは改行文字、\tはタブを表しています。
show_int(n,X)は、整数Xの値を少なくとも|n|文字で出力します。n > 0なら右揃え、それ以外は左揃えで出力します。
show_float(n,d,X)はfloat Xの値を少なくとも|n|個の文字で出力します。n > 0なら右揃え、それ以外は左揃えで、小数点以下d文字で出力します。
文字列リテラルは1行に収まらなければなりません。長い文字列リテラルは、文字列連結演算子++を使って複数行に分割することができます。
例えば、文字列リテラル
"Invalid datafile: Amount of flour is non-negative"
は、次の文字列リテラル表現と同じです。
"Invalid datafile: " ++
"Amount of flour is non-negative"
MiniZincは、文字列補間をサポートしています。式は、文字列リテラルに直接埋め込むことができ、"\(e)"という形式のサブ文字列は、show(e)の結果で置き換えられます。例えば、"t=\(t)\n"は、"t=" ++ show(t) ++ "\n"と同じ文字列を生成します。
1つのモデルに複数の出力文を含めることができます。その場合、すべての出力は、モデルに現れた順に連結されます。
モデルを評価するには、MiniZinc IDEの「Run」ボタンをクリックするか、次のように入力します。
$ minizinc --solver gecode aust.mzn
ここで、aust.mznはMiniZincモデルを含むファイルの名前です。MiniZincモデルであることを示すために、ファイルの拡張子として.mznを使用する必要があります。minizincコマンドに--solver gecodeオプションを付けると、Gecode有限領域ソルバーを使用してモデルを評価します。MiniZincのバイナリディストリビューションを使用している場合、このソルバーは実際にはデフォルトであるため、代わりにminizinc aust.mznを実行することができます。
これを実行すると、次の結果が得られます。
wa=3 nt=2 sa=1
q=3 nsw=2 v=3
t=1
----------
10個のダッシュ ---------- の行は、ソリューションが見つかったことを示すために、MiniZinc出力によって自動的に追加されます。
2.1.2. 算術最適化の例(An Arithmetic Optimisation Example)
2つ目の例は、地元の学校で行われる祭りのためにケーキを作るというものです。私たちは、2種類のケーキの作り方を知っています（注意：これらのレシピを家で使わないでください）。小麦粉250g、潰したバナナ2本、砂糖75g、バター100gで作るバナナケーキと、小麦粉200g、ココア75g、砂糖150g、バター150gで作るチョコレートケーキです。チョコレートケーキを4.50ドル、バナナケーキを4.00ドルで販売します。小麦粉が4kg、バナナが6本、砂糖が2kg、バターが500g、ココアが500gあります。問題は、利益を最大にするためには、それぞれの種類のケーキをいくつ焼くべきかということです。MiniZincモデルの例をリスト2.1.2に示します。
Listing 2.1.2 Model for determining how many banana and chocolate cakes to bake for the school fete (cakes.mzn)
% Baking cakes for the school fete
var 0..100: b; % no. of banana cakes
var 0..100: c; % no. of chocolate cakes
% flour
constraint 250*b + 200*c <= 4000;
% bananas
constraint 2*b <= 6;
% sugar
constraint 75*b + 150*c <= 2000;
% butter
constraint 100*b + 150*c <= 500;
% cocoa
constraint 75*c <= 500;
% maximize our profit
solve maximize 400*b + 450*c;
output ["no. of banana cakes = \(b)\n",
"no. of chocolate cakes = \(c)\n"];
最初は、算術式の使い方です。
整数の算術演算子(Integer Arithmetic Operators)
MiniZincは、標準的な整数の算術演算子を提供します。加算(+)、減算(-)、乗算(*)、整数除算(div)、整数倍(mod)です。また、単項演算子として + と - を提供しています。
整数の剰余は、配当のaと同じ符号を持つ結果a mod bを与えるように定義されています。
整数の除算は、$a = b (a \ div \ b) + (a\bmod b)$と定義されます。
MiniZincは、絶対値(abs)と累乗(pow)の標準的な整数関数を提供します。例えば、abs(-4)とpow(2,5)は、それぞれ4と32と評価されます。
算術リテラルの構文は、標準的なものです。整数リテラルは、10進数、16進数、8進数のいずれかです。例えば、0、5、123、0x1b7、0o777などです。
この例で示された2つ目の新しい機能は、最適化です。
solve maximize 400 * b + 450 * c;
は，solve文の中の目的(objective)と呼ばれる式を最大化する解を求めることを指定しています．目的はどんな種類の算術式でも構いません。キーワードmaximizeをminimizeに置き換えることで、最小化問題を指定することができます。
これを実行すると、次のような結果が得られます。
no. of banana cakes = 2
no. of chocolate cakes = 2
----------
==========
ライン ========== は、最適化問題において、システムが解が最適であることを証明したときに自動的に出力されます。
2.1.3. データファイルとアサーション(Datafiles and Assertions)
このモデルの欠点は、次に学校でケーキを焼くときに（これはよくあることですが）、同じような問題を解決しようとすると、食料品貯蔵室にある材料を反映してモデルの制約を変更する必要があることです。もしモデルを再利用したいのであれば、各材料の量をモデルのパラメータにして、その値をモデルの一番上で設定するのが良いでしょう。
もっと良いのは、これらのパラメータの値を別のデータファイルに設定するのが良いでしょう。MiniZincは、他の多くのモデリング言語と同様に、オリジナルのモデルで宣言されたパラメータの値を設定するためにデータファイルを使用することができます。これにより、異なるデータファイルで実行することで、同じモデルを異なるデータで簡単に使用することができます。
データファイルにはMiniZincデータファイルを示す.dznというファイル拡張子が必要で、1つのモデルをいくつのデータファイルでも実行することができます（ただし、1つの変数/パラメータは1つのファイルでしか値を割り当てることができません）。
Listing 2.1.3 Data-independent model for determining how many banana and chocolate cakes to bake for the school fete (cakes2.mzn)
% Baking cakes for the school fete (with data file)
int: flour; %no. grams of flour available
int: banana; %no. of bananas available
int: sugar; %no. grams of sugar available
int: butter; %no. grams of butter available
int: cocoa; %no. grams of cocoa available
constraint assert(flour >= 0,"Invalid datafile: " ++
"Amount of flour should be non-negative");
constraint assert(banana >= 0,"Invalid datafile: " ++
"Amount of banana should be non-negative");
constraint assert(sugar >= 0,"Invalid datafile: " ++
"Amount of sugar should be non-negative");
constraint assert(butter >= 0,"Invalid datafile: " ++
"Amount of butter should be non-negative");
constraint assert(cocoa >= 0,"Invalid datafile: " ++
"Amount of cocoa should be non-negative");
var 0..100: b; % no. of banana cakes
var 0..100: c; % no. of chocolate cakes
% flour
constraint 250*b + 200*c <= flour;
% bananas
constraint 2*b <= banana;
% sugar
constraint 75*b + 150*c <= sugar;
% butter
constraint 100*b + 150*c <= butter;
% cocoa
constraint 75*c <= cocoa;
% maximize our profit
solve maximize 400*b + 450*c;
output ["no. of banana cakes = \(b)\n",
"no. of chocolate cakes = \(c)\n"];
新しいモデルをリスト2.1.3に示します。このモデルを実行するには、次のコマンドを使用します。
$ minizinc cakes2.mzn pantry2.dzn
ここで、データファイルpantry.dznはリスト2.1.4で定義されています。これはcakes.mznと同じ結果になります。コマンドを実行したときの出力を、リスト2.1.5で定義した代替データセットで実行したときの出力は以下のとおりです。
no. of banana cakes = 3
no. of chocolate cakes = 8
----------
==========
cakes.mznからoutputステートメントを削除すると、MiniZincはデフォルトの出力を使用します。この場合、出力結果は次のようになります。
b = 3;
c = 8;
----------
==========
デフォルト出力(Default Output)
outputのないMiniZincモデルでは、宣言時に式が代入されていない限り、各決定変数にその値が1行ずつ出力されます。出力がまさにデータファイル形式になっていることに注目してください。
Listing 2.1.4 Example data file for cakes2.mzn (pantry.dzn)
flour = 4000;
banana = 6;
sugar = 2000;
butter = 500;
cocoa = 500;
Listing 2.1.5 Example data file for cakes2.mzn (pantry2.dzn)
flour = 8000;
banana = 11;
sugar = 3000;
butter = 1500;
cocoa = 800;
小さなデータファイルは、直接.dznファイルを作成せずに、コマンドラインフラグ -D string（stringはデータファイルの内容）を使って入力できます。例えば、次のようなコマンドです。
$ minizinc cakes2.mzn -D\
"flour=4000;banana=6;sugar=2000;butter=500;cocoa=500;"
は
$ minizinc cakes2.mzn pantry.dzn
と同じ結果になります。
データファイルには、対象となるモデルの決定変数やパラメータの代入文しか記述できません。
防御的プログラミングでは、データファイルの値が妥当であるかどうかをチェックする必要があります。この例では、すべての成分の量が非負であることをチェックし、それが真でない場合はランタイムエラーを発生させるのが賢明です。MiniZincは、パラメータ値をチェックするためのブール演算子を内蔵しています。形式は assert(B,S) です。ブール式Bが評価され、偽の場合は実行を中断し、文字列式Sが評価され、エラーメッセージとして出力されます。小麦粉の量が負の場合にチェックして適切なエラーメッセージを生成するには、次の行を追加するだけです。
constraint assert(flour >= 0, "Amount of flour is non-negative");
という行をモデルに追加します。assert式はブール式なので、制約の一種であると考えられることに注意してください。同様の行を追加して、他の材料の量が非負であることをチェックすることができます。
2.1.4. 実数の問題を解く(Real Number Solving)
MiniZincは、浮動小数点の変数と制約を使った実数の制約解決もサポートしています。
1年間の短期ローンを組み、四半期ごとに4回に分けて返済するという問題を考えてみましょう。この問題のモデルをリスト2.1.6に示します。このモデルでは、単純な利息計算を用いて各四半期後の残高を計算します。
Listing 2.1.6 Model for determining relationships between a 1 year loan repaying every quarter (loan.mzn)
% variables
var float: R; % quarterly repayment
var float: P; % principal initially borrowed
var 0.0 .. 10.0: I; % interest rate
% intermediate variables
var float: B1; % balance after one quarter
var float: B2; % balance after two quarters
var float: B3; % balance after three quarters
var float: B4; % balance owing at end
constraint B1 = P * (1.0 + I) - R;
constraint B2 = B1 * (1.0 + I) - R;
constraint B3 = B2 * (1.0 + I) - R;
constraint B4 = B3 * (1.0 + I) - R;
solve satisfy;
output [
"Borrowing ", show_float(0, 2, P), " at ", show(I*100.0),
"% interest, and repaying ", show_float(0, 2, R),
"\nper quarter for 1 year leaves ", show_float(0, 2, B4), " owing\n"
];
整数変数と同じように、intではなくfloatというキーワードを使って、float変数fを宣言していることに注意してください。
同じモデルを使って、さまざまな質問に答えることができます。最初の質問は、「1000ドルを4%で借りて、四半期ごとに260ドルを返済すると、最終的にいくらになるか」というものです。この質問は、データファイルloan1.dznによってエンコードされています。
実数の変数と制約を使用したいので、この種の問題をサポートするソルバーを使用する必要があります。Gecode（MiniZincバンドルバイナリディストリビューションのデフォルトソルバー）は浮動小数点変数をサポートしていますが、混合整数線形計画（MIP）ソルバーの方がこの種の問題に適しているかもしれません。MiniZinc ディストリビューションには、このようなソルバーが含まれています。IDEのソルバーメニュー（Runボタンの下の三角形）からCOIN-BCを選択するか(訳注1)、コマンドラインでminizinc --solver cbcというコマンドを使用して呼び出すことができます。
訳注1: IDEで"COIN-BC 2.10.5/1.17.5"を選択してもエラーになりました。正常に実行できる他の選択肢は無さそうです。コマンドラインでは下のとおりで問題なかったです。
$ minizinc --solver cbc loan.mzn loan1.dzn
出力は
Borrowing 1000.00 at 4.0% interest, and repaying 260.00
per quarter for 1 year leaves 65.78 owing
----------
訳註:「1000ドルを利息4%で借りて、各四半期260ドル返済すると、1年後に65.78ドル負債が残る」
2つ目の質問は、もし私が1000ドルを利息4％で借りて、最後には借りが無い状態にしたい場合、各四半期いくら返済すればいいのでしょうか？この質問は、データファイルloan2.dznによってエンコードされています。
以下のコマンド
$ minizinc --solver cbc loan.mzn loan2.dzn
を実行したときの出力です。
Borrowing 1000.00 at 4.0% interest, and repaying 275.49
per quarter for 1 year leaves 0.00 owing
----------
3つ目の質問は、もし私が各四半期に250ドルを返済できるなら、利息4％で幾ら借りれば、最終的に完済できるでしょうか？この質問は、データファイルloan3.dznによってエンコードされています。
以下のコマンド
$ minizinc --solver cbc loan.mzn loan3.dzn
を実行したときの出力は
Borrowing 907.47 at 4.0% interest, and repaying 250.00
per quarter for 1 year leaves 0.00 owing
----------
Listing 2.1.7 Example data file for loan.mzn (loan1.dzn)
I = 0.04;
P = 1000.0;
R = 260.0;
Listing 2.1.8 Example data file for loan.mzn (loan2.dzn)
I = 0.04;
P = 1000.0;
B4 = 0.0;
Listing 2.1.9 Example data file for loan.mzn (loan3.dzn)
I = 0.04;
R = 250.0;
B4 = 0.0;
浮動小数点演算子(Float Arithmetic Operators)
MiniZincは、標準的な浮動小数点演算子である加算(+)、減算(-)、乗算(*)、浮動小数点除算(/)を提供します。また、単項演算子として+と-を提供しています。
MiniZincは、自動的に整数を浮動小数点数に強制変換することができます。しかし、強制を明示的に行うには、組み込み関数int2floatを使用することができます。自動変換の結果として、a / bという式は常に浮動小数点数の割り算とみなされることに注意してください。整数の除算が必要な場合は、必ずdiv演算子を使用してください。
MiniZincは、さらに以下の浮動小数点関数を提供します。絶対値(abs)、平方根(sqrt)、自然対数(ln)、底を2とする対数(log2)、底を10とする対数(log10)、指数関数$e^x$(exp)、正弦(sin)、余弦(cos)、正接(tan)、アークサイン(asin)、アークコサイン(acos)、アークタンジェント(atan), ハイパボリックサイン(sinh), ハイパボリックコサイン(cosh), ハイパボリックタンジェント(tanh), ハイパボリックアークサイン(asinh), ハイパボリックアークコサイン (acosh), ハイパボリックアークタンジェント(atanh), 冪(pow)
冪(pow)は唯一の二項関数で、その他は単項関数です。
算術リテラルの構文は合理的に標準化されています。floatリテラルの例としては、1.05、1.3e-5、1.3E+5があります。
2.1.5. モデルの基本構造(Basic structure of a model)
ここで、MiniZincモデルの基本構造をまとめておきます。複数の項目で構成されており、それぞれの項目の最後にはセミコロン;が付いています。項目はどのような順序でも使用できます。例えば、識別子は、使用する前に宣言する必要はありません。
アイテムは8種類あります。
-
includeは、別のファイルの内容をモデルに挿入するためのものです。以下のような形をしています。
include <filename>;
ここで、<filename>は文字列リテラルです。これにより、大きなモデルを小さなサブモデルに分割したり、ライブラリファイルで定義された制約条件を含めることができます。その例をリスト2.2.4で見てみましょう。
- 変数宣言では、新しい変数を宣言します。このような変数はグローバル変数であり、モデルのどこからでも参照することができます。変数には2つの種類があります。モデルやデータファイルに固定値が割り当てられているパラメータ(parameter)と、モデルを解いたときに初めて値が決まる決定変数(decision variable)です。パラメータは固定されており、決定変数は固定されていません。変数は、宣言の一部として値を割り当てることもできます。その形式は以下の様になります。
<type inst expr>: <variable> [ = ] <expression>;
<type-inst expr>では、変数のインスタンス化と型を指定します。これらは、MiniZincの複雑な側面の1つです。インスタンス化は、パラメータには
parを、決定変数にはvarを使って宣言します。明示的なインスタンス化の宣言がない場合、その変数はパラメータとなります。型は、基本型か、整数または浮動小数点の範囲(range)、配列(array)または集合(set)です。基本型にはfloat、int、string、bool、annがありますが、決定変数に使用できるのはfloat、int、boolのみです。基本型annはアノテーションです。アノテーションについては"Search"で説明します。int型の代わりに、整数の範囲表現を使用することができます。同様に、float型の代わりにfloatの範囲表現を使用することができます。これらは通常、決定変数の領域を指定するために使用されますが、パラメータの範囲を制限するためにも使用できます。変数宣言のもう一つの使い方は、列挙型を定義することです。これについては列挙型で説明します。割り当ては、変数に値を割り当てるものです。以下のような形式になります。
<variable> = <expression>;
決定変数に値を代入することができますが、その場合、代入はconstraint <variable> = <expression>を記述するのと同じです。
- 制約(constraint)項目は、モデルの中心となるものです。それらは以下のような形をしています。
constraint <Boolean expression>;
これまでに、算術比較と組み込みのアサート演算子を使った単純な制約の例を見てきました。次のセクションでは、より複雑な制約の例を見てみましょう。
- 解決(solve)項目では、どのような解決策が求められているかを指定します。これまで見てきたように、これらは3つの形式のうちのどれか1つです。
solve satisfy;
solve maximize <arithmetic expression>;
solve minimize <arithmetic expression>;
モデルには、最大でも1つのsolve項目です。省略された場合は、solve satisfyとして扱われます。
- 出力項目は、モデルの実行結果をきれいに表現するためのものです。これらは、以下のような形式になっています。
output [ <string expression>, ..., <string expression> ];
出力項目がない場合、MiniZincはデフォルトで、オプションで値を割り当てられていないすべての決定変数の値を、割り当て項目の形式で出力します。
列挙型の宣言。これらについては、配列(Arrays)と集合(Sets)と列挙型(Enumerated Types)で説明します。
述語(predicate)、関数(function)、テストは新しい、制約、関数、ブールテストを定義するためのものです。これらについては、述語と関数で説明します。
アノテーションは、新しいアノテーションを定義するために使用されます。これらについては、Searchで説明します。