mzn2fzn 변환 중 int 도메인 집합을 전파하는 방법은 무엇입니까?

Question

나는 다음 MiniZinc 코드 샘플이 있습니다

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 코드 출력 : 여기에

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; 

을 통지 원래 y가 선언되었다 set of 1..100MiniZinc 모델이지만 mzn2fzn은 배열 x의 요소에 대한 경계를 y에 올바르게 전파하므로 FlatZinc 모델은 y을 set of 1..10으로 선언합니다.

지금, 나는 element_set.mzn의 내용을 사용자 정의 할 수 있도록 내 자신의 술어를 사용하는 경우 element_set이라고, 그래서 다음과 같이이로 변경됩니다 :

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; 

,691,363 : 결과 FlatZinc 파일이 y 여전히 set of 1..100 선언했다, 그래서 y에 배열 x의 요소에 대한 경계를 전파210

의 도메인을 전파하는 데 올바른 인코딩이 무엇인지 알고있는 사람이 있는지 알고 싶습니다. 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 술어의 패밀리는 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 정의에 전파됩니다. 다음과 같다 같이 정의는 builtins.mzn에서 발견된다 :

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; 

당신은 당신의 요소 제약이 첫 번째 경우 - 다음 지점에있는 것으로 평가되는 것을 볼 수 있습니다. 더 중요한 질문은 요소 제약이 왜 그렇게 복잡한가하는 것입니다. 답은 정의되지 않은 문제와 관련이 있다는 것입니다.

array[1..3] of int: a가 있다고 가정하면 a[4]은 무엇으로 평가됩니까? 그런 것을 불법으로 만들기는 쉬울 수도 있지만, a[i] > 5 \/ i > 10이라는 표현은 어떨까요? 이것은 i = 11에 대해 만족할만한 모델이어야합니다. MiniZinc에서 이러한 잘못된 값은 정의되지 않은 것으로 불리며 가장 가까운 부울 식으로 버블 링되어 false이됩니다.

이제 요소 제약 조건을 다시 살펴보면 예제에서와 같이 루트 컨텍스트에서 도메인을 적용하고 "안전"요소 제약 조건을 사용할 수 있음을 알 수 있습니다. 마찬가지로 인덱스의 경계가 배열 경계보다 작은 경우 "안전"요소 제약 조건을 사용할 수 있지만 범위가 더 큰 경우 "안전하지 않은"요소 제약 조건을 사용하고 값이 정의 될 때 true 만 반환되는지 확인하십시오 .

비슷한 접근법을 사용하거나 나중 단계 술어를 다시 정의 할 것을 제안합니다. 다음 논문에서 찾을 수있다 MiniZinc에서 undefinedness에 대한

자세한 내용은 (대신 array_var_set_element를 재정의하는 것이 가능) :

프리 슈, A. M., & 스 터키, P. J. (2009). 적절한 처리 제약 언어의 정의되지 않음. CP, 5732, 367-382]에 기재되어있다.

MiniZinc는 관계형 의미론을 사용합니다.