카디널리티 제약

Question

MiniZinc 제약 해결사 사용하여 매우 쉽게 cardinality constraints을 표현할 수 내장 sum() 기능 : 카디널리티 제약 조건이 충족

% This predicate is true, iff 2 of the array 
% elements are true 
predicate exactly_two_sum(array[int] of var bool: x) = 
    (sum(x) == 2); 

경우에만, 수 경우 배열의 진정한 요소 부울 변수의 값은 지정된대로입니다. 부울은 합계를 계산하기 위해 정수 값 0 및 1에 자동으로 매핑됩니다.

% This predicate is true, iff 2 of the array 
% elements are true 
predicate exactly_two_parallel(array[int] of var bool: x) = 
    let 
    { 
     int: lb = min(index_set(x)); 
     int: ub = max(index_set(x)); 
     int: len = length(x); 
    } 
    in 
    if len < 2 then 
     false 
    else if len == 2 then 
     x[lb] /\ x[ub] 
    else 
     (
     let 
     { 
      % counter is modelled as a set of slices 
      % with 2 outputs each 
      % Encoding: 
      % 0 0 : 0 x true 
      % 0 1 : 1 x true 
      % 1 0 : 2 x true 
      % 1 1 : more than 2 x true 
      array[lb+1..ub] of var bool: t0; 
      array[lb+1..ub] of var bool: t1; 
     } 
     in 
     % first two slices are hard-coded 
     (t1[lb+1] == (x[lb] /\ x[lb+1])) /\ 
     (t0[lb+1] == not t1[lb+1]) /\ 
     % remaining slices are regular 
     forall(i in lb+2..ub) 
     (
      (t0[i] == (t0[i-1] != x[i]) \/ (t0[i-1] /\ t1[i-1])) /\ 
      (t1[i] == t1[i-1] \/ (t0[i-1] /\ x[i])) 
     ) /\ 
     % output of final slice must be 1 0 to fulfil predicate 
     (t1[ub] /\ not t0[ub]) 
    ) 
    endif endif; 

질문 :

% This predicate is true, iff 2 of the array 
% elements are true 
predicate exactly_two_serial(array[int] of var bool: x) = 
    let 
    { 
     int: lb = min(index_set(x)); 
     int: ub = max(index_set(x)); 
     int: len = length(x); 
    } 
    in 
    if len < 2 then 
     false 
    else if len == 2 then 
     x[lb] /\ x[ub] 
    else 
     (
     let 
     { 
      % 1-of-3 counter is modelled as a set of slices 
      % with 3 outputs each 
      array[lb+1..ub-1] of var bool: t0; 
      array[lb+1..ub-1] of var bool: t1; 
      array[lb+1..ub-1] of var bool: t2; 
     } 
     in 
     % first two slices are hard-coded 
     (t0[lb+1] == not(x[lb] \/ x[lb+1])) /\ 
     (t1[lb+1] == (x[lb] != x[lb+1])) /\ 
     (t2[lb+1] == (x[lb] /\ x[lb+1])) /\ 
     % remaining slices are regular 
     forall(i in lb+2..ub-1) 
     (
      (t0[i] == t0[i-1] /\ not x[i]) /\ 
      (t1[i] == (t0[i-1] /\ x[i]) \/ (t1[i-1] /\ not x[i])) /\ 
      (t2[i] == (t1[i-1] /\ x[i]) \/ (t2[i-1] /\ not x[i])) 
     ) /\ 
     % output 2 of final slice must be true to fulfil predicate 
     ((t1[ub-1] /\ x[ub]) \/ (t2[ub-1] /\ not x[ub])) 
    ) 
    endif endif; 

이 구현은 조각 사이의 적은 라인/변수로 병렬 인코딩을 사용하고 있습니다 : 카운터 조각 세트로

나는 내 자신의 카디널리티 제약 조건을 구현 :

h ome-grown 카디널리티 술어? 아니면 솔루션 속도면에서 의문의 여지없이 MiniZinc 구현이 sum()입니까?

업데이트 : Gecode로 해석 백엔드를 사용하고
.

Answer 1

선형 합계는 일반적으로 제약 조건 해결사에서 구현하기에 가장 중요한 제약 조건 중 하나입니다. 따라서 간단한 합계를 사용하는 초기 버전이 훨씬 좋습니다. 특히 부울 합계를 구현하는 Gecode의 전파자는 최대한 효율적으로 최적화되었습니다.

일반적으로 일반적으로 사용 가능한 제한 조건을 사용하는 것이 좋습니다. 특히, 일반적으로 좋은 아이디어 인 global constraint으로 매핑하는 것이 좋습니다. 관련 예제는 정수 배열에서 여러 다른 숫자의 발생을 계산하려는 경우입니다.이 경우 global cardinality constraint은 매우 유용합니다.

완전성을 위해 : 게으른 절 생성 솔버 (예 : Chuffed)를 사용할 때, (새로운) 분해가 때로는 놀랍게 유용 할 수 있습니다. 그러나 그것은 훨씬 더 진보 된 주제입니다.