カーディナリティ制約は

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

通常、線形和は、制約ソルバーでよく実装するための最も重要な制約の1つです。そのため、単純な和を使った初期バージョンのほうがはるかに優れています。特に、ブール和を実装するGecodeのプロパゲータは、可能な限り効率的になるように大きく最適化されています。

一般的に、利用可能な制約を使用することをお勧めします。特に、よく実行されているものがglobal constraintにマップされていれば、それは良い考えです。関連する例は、整数配列のいくつかの異なる数字の出現を数えたい場合です。この場合、global cardinality constraintは非常に便利です。

完全性：遅延句生成ソルバー（たとえばChuffed）を使用する場合、（新規）分解が驚くほど便利な場合があります。しかしそれははるかに高度なトピックです。