在 minizinc 中搜索排序数组的最小交换次数

Question

我正在学习约束规划课程，教授给我分配了这份工作： 让我们考虑一个由数字 v = [v_1, ... , v_n] 组成的 n 元素向量，其中 v_i ∈ N。对于 i，j ∈ {1, ... , n} swap(i, j) 移动具有交换值 v[i] 和 v[j] 的效果。问题是要找到 对向量进行排序的最小长度计划。

int: n = 5;

array[1..n] of int: A = [2, 3, 4, 5, 1];

array[1..n, 1..n] of var int: A_prime;
array[1..n, 1..2] of var 1..n: swaps;
array[1..n, 1..n, 1..n] of var 0..1: lt;
array[1..n] of var int: sums;

var int: steps;

predicate swap(array[1..n, 1..n] of var int: A_prime, var int: i, var int: j, int: k) = 
  let {var int: temp = A_prime[k-1, i]}
  in A_prime[k, i] = A_prime[k-1, j]
  /\ A_prime[k, j] = temp
;


constraint steps > 0 /\ steps <= n;

constraint forall(i in 1..n)
(
  A_prime[1, i] = A[i]
);

constraint forall(i, j in 1..n where i < j)
(
  if A[i] <= A[j] then
    lt[1, i, j] = 1
  else
    lt[1, i, j] = 0
  endif
);

constraint forall(i in 1..n)
(
  forall(j, k in 1..n where j >= k)
  (
    lt[i, j, k] = 0
  )  
);

constraint forall(i in 1..steps)
(
  swaps[i, 1] < swaps[i, 2]
);

constraint forall(i, j in 1..steps where i < j)
(
  (swaps[i, 1] != swaps[j, 1] /\ swaps[i, 2] == swaps[j, 2]) \/
  (swaps[i, 1] == swaps[j, 1] /\ swaps[i, 2] != swaps[j, 2]) \/
  (swaps[i, 1] != swaps[j, 1] /\ swaps[i, 2] != swaps[j, 2])
);

constraint forall(i in 2..steps)
(
  swap(A_prime, swaps[i-1, 1], swaps[i-1, 2], i)
);

constraint forall(i in 2..steps)
(
  forall(j in 1..n where j != swaps[i-1, 1] /\ j != swaps[i-1, 2])
  (
    A_prime[i, j] = A_prime[i-1, j]
  )
);

constraint forall(i in 2..steps)
(
  forall(j, k in 1..n where j < k)
  (
    if A_prime[i, j] <= A_prime[i, k] then
      lt[i, j, k] = 1
    else
      lt[i, j, k] = 0
    endif
  )
);

constraint forall(i in 1..steps-1)
(
  lt[i, swaps[i, 1], swaps[i, 2]] == 0
);

constraint forall(i in 1..steps)
(
  sums[i] = sum(j, k in 1..n where j < k)(lt[i, j, k])
);

constraint forall(i, j in 1..steps where i < j)
(
  sums[i] < sums[j]
);

constraint sums[steps] == ceil((n*(n-1))/2);

constraint forall(i in steps+1..n, j in 1..n)
(
  A_prime[i, j] = 1
);

constraint forall(i in steps+1..n)
(
  sums[i] = 0
);

constraint forall(i in steps+1..n)
(
  swaps[i, 1] = 1 /\ swaps[i, 2] = 1 
);

solve minimize steps;

这是我想出的解决方案。让我分解一下：首先，我为 n 元素向量生成所有可能的交换，然后仅过滤那些排列 v[i] 和 v[j] 的交换。每次交换后，我将结果数组存储在 A_prime 矩阵中，位于与进行交换的步骤相对应的行中。为了确定唯一有用的交换，我计算 lt 矩阵，这是一个上三角 3D 矩阵，其中如果 A_prime[k, i] 小于或等于 A_prime[k, j]，则 lt[i, j] 等于 0，并且 1否则。如果最终 lt 矩阵中的元素总和等于 (n*(n-1))/2，我认为数组是有序的。

问题是这个解决方案很慢；即使数组只有 5 个元素，它也会遇到困难。我尝试为未使用的变量（例如 lt 矩阵的下三角部分）分配默认值，以减少解的数量，但这似乎并不有效。

您有什么提示可以让这段代码执行得更快吗？预先感谢！

Answer 1

我无法告诉你的模型到底发生了什么。但以下替代解决方案可能会给您带来启发。

正如您所注意到的，运行时间随着

n

值的增长而爆炸。

int: n = 5;
set of int: elements = 1..n;
set of int: steps = 1..n;

%  array elements can be arbitrary integers
%  not necessarily distinct
array[elements] of int: A = [2, 3, 4, 5, 1];

%  evaluate set of occurring numbers
%  to delimit the choices for the solver
set of int: Domain = array2set(A);

%  array of 1..n permutations
array[steps, elements] of var Domain: AP;

%  number of steps to minimize
%  may be zero if A is sorted beforehand
var 0..n: Steps;

%  first permutation is the original array A
%  copy A to avoid case distinctions
constraint forall(e in elements) ( AP[1, e] == A[e] );
 
%  adjacent permutations have a pairwise distance of one swap
%  for each step, a pair of indices must exist which describes the swap
constraint forall(s in steps where (s > 1))
( exists([
     %  count matching elements; all positions have to match
     n == (
            %  count swapped positions separately
            (AP[s - 1, i] == AP[s, j]) + 
            (AP[s - 1, j] == AP[s, i]) +
            %  add the non-swapped positions
            sum([AP[s - 1, e] == AP[s, e] 
                 | e in elements where (e != i) /\ (e != j)])
          )
     | i, j in elements where j > i
   ])
);

%  after Steps, the resulting permutation must be sorted
constraint forall([ AP[1 + Steps, e] >= AP[1 + Steps, e - 1] 
                   | e in elements where e > 1 ] );

solve minimize Steps;

结果输出：

AP = 
[| 2, 3, 4, 5, 1
 | 5, 3, 4, 2, 1
 | 5, 4, 3, 2, 1
 | 5, 2, 3, 4, 1
 | 1, 2, 3, 4, 5
 |];
Steps = 4;
_objective = 4;