mzn2fzn変換中にintドメインセットを伝播する方法はありますか？

Question

私は、次のMiniZincのコードサンプルがあります。もともとyがあることを宣言されたことがわかり、ここで

var set of 1..10: X_INTRODUCED_0_; 
var set of 1..10: X_INTRODUCED_1_; 
var set of 1..10: X_INTRODUCED_2_; 
var set of 1..10: X_INTRODUCED_3_; 
var set of 1..10: X_INTRODUCED_4_; 
var set of 1..10: X_INTRODUCED_5_; 
var set of 1..10: X_INTRODUCED_6_; 
var -3..3: i:: output_var; 
var set of 1..10: y:: output_var; 
var 1..7: X_INTRODUCED_9_ ::var_is_introduced :: is_defined_var; 
array [1..7] of var set of int: x:: output_array([-3..3]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_,X_INTRODUCED_3_,X_INTRODUCED_4_,X_INTRODUCED_5_,X_INTRODUCED_6_]; 
constraint array_var_set_element(X_INTRODUCED_9_,[X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_,X_INTRODUCED_3_,X_INTRODUCED_4_,X_INTRODUCED_5_,X_INTRODUCED_6_],y):: defines_var(y); 
constraint int_lin_eq([1,-1],[i,X_INTRODUCED_9_],-4):: defines_var(X_INTRODUCED_9_):: domain; 
solve satisfy; 

：

include "globals.mzn"; 

var int: i; 
array[-3..3] of var set of 1..10: x; 
var set of 1..100: y; 

constraint element(i, x, y); 

solve satisfy; 

output [ 
    show(i), "\n", 
    show(x), "\n", 
    show(y), "\n", 
]; 

標準ライブラリで実行mzn2fznコマンドは、以下のFlatZincコードを出力のモデルのset of 1..100ですが、mzn2fznは配列xの要素の境界をyに正しく伝播しますFlatZincモデルはyがset of 1..10と宣言しています。

今、私は私自身の述語がelement_setを使用した場合に呼び出されるので、次のように私がすることに変更されるようelement_set.mznの内容をカスタマイズしたい：

predicate element_set(var int: i, array[int] of var set of int: x, 
     var set of int: y) = 
    min(index_set(x)) <= i /\ i <= max(index_set(x)) /\ 
    optimathsat_element_set(i, x, y, index_set(x)); 

predicate optimathsat_element_set(var int: i, 
            array[int] of var set of int: x, 
            var set of int: y, 
            set of int: xdom); 

しかし、このコードはないます

predicate optimathsat_element_set(var int: i,array [int] of var set of int: x,var set of int: y,set of int: xdom); 
var set of 1..10: X_INTRODUCED_0_; 
var set of 1..10: X_INTRODUCED_1_; 
var set of 1..10: X_INTRODUCED_2_; 
var set of 1..10: X_INTRODUCED_3_; 
var set of 1..10: X_INTRODUCED_4_; 
var set of 1..10: X_INTRODUCED_5_; 
var set of 1..10: X_INTRODUCED_6_; 
var -3..3: i:: output_var; 
var set of 1..100: y:: output_var; %%% OFFENSIVE LINE %%% 
array [1..7] of var set of int: x:: output_array([-3..3]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_,X_INTRODUCED_3_,X_INTRODUCED_4_,X_INTRODUCED_5_,X_INTRODUCED_6_]; 
constraint optimathsat_element_set(i,x,y,-3..3); 
solve satisfy; 

：得 FlatZincファイル yがまだ set of 1..100であると宣言しているように、 yに配列 xの要素に境界を伝播します210

ドメインxをyに伝播するための正しいエンコード方法がわかっているかどうかを知りたいと思います。私は他のelement_Tの制約のためにこれを行うことができましたが、私は適切なの組み込みを見つけることができないので、element_setの優雅な解決策を見つけることができません。。言い換えれば

、私はそれを行うだろうか

var set of 1..10: y:: output_var; 

代わり

var set of 1..100: y:: output_var; 

の取得したいですか？

Answer 1

述語はelement/element_Tファミリに内部的にマップされています。

2.0.2バージョンMiniZincにおいて上記、これらの機能は、以下の述語にマッピングされている：

% This file contains redefinitions of standard builtins for version 2.0.2 
% that can be overridden by solvers. 

...  

predicate array_var_bool_element_nonshifted(var int: idx, array[int] of var bool: x, var bool: c) = 
    array_var_bool_element((idx-(min(index_set(x))-1))::domain,array1d(x),c); 

predicate array_var_int_element_nonshifted(var int: idx, array[int] of var int: x, var int: c) = 
    array_var_int_element((idx-(min(index_set(x))-1))::domain,array1d(x),c); 

predicate array_var_float_element_nonshifted(var int: idx, array[int] of var float: x, var float: c) = 
    array_var_float_element((idx-(min(index_set(x))-1))::domain,array1d(x),c); 

predicate array_var_set_element_nonshifted(var int: idx, array[int] of var set of int: x, var set of int: c) = 
    array_var_set_element((idx-(min(index_set(x))-1))::domain,array1d(x),c); 

最善の解決策ではなくelement/element_Tものいじりこれらの述語をオーバーライドすることです。

Answer 2

インデックスのドメインは実際にはelement関数のMiniZinc定義に反映されています。

function var set of int: element(var int: idx, array[int] of var set of int: x) = 
    if mzn_in_root_context(idx) then let { 
    constraint idx in index_set(x) 
    } in element_t(idx,x) 
    elseif (has_bounds(idx) /\ lb(idx) >= min(index_set(x)) /\ ub(idx) <= max(index_set(x))) then 
    element_t(idx,x) 
    else let { 
    constraint idx in index_set(x) 
    } in element_mt(idx,x) 
    endif; 

あなたの要素の制約が最初のif-thenブランチであると評価されていることがわかります次のとおりであるような定義は、builtins.mznで発見されました。より重要な問題は、要素制約がなぜ複雑になるかということです。その答えは不確定性と関係しているということです。

array[1..3] of int: aがあるとしたら、a[4]は何と評価されますか？ このようなことを違法にするのは簡単かもしれませんが、式a[i] > 5 \/ i > 10はどうでしょうか？これは、i = 11のために充足可能でなければならないよく考えられたモデルである可能性があります。 MiniZincでは、これらの不正な値は未定義と呼ばれ、falseに近いブール式までバブリングされます。

要素の制約を振り返ってみると、例のようにルートコンテキストでは、ドメインを強制して "安全"な要素の制約を使用することができます。同様に、インデックスの境界が配列の境界よりも小さい場合、安全な要素の制約を使用できますが、境界が大きければ、安全でない要素の制約を使用し、値が定義されたときにのみtrueが返されるようにします。

同様の方法を使用するか、後の段階の述語を再定義することをお勧めします。

フリッシュ、A. M.、&スタッキー、P. J.（2009）（これは代わりarray_var_set_elementを再定義することが可能です）MiniZincでundefinedness約

詳しい情報は、次の論文に見出すことができます。適切な治療 制約言語の不確定性。 CP、5732,367-382。

MiniZincはリレーショナルセマンティクスを使用します。