143 lines
8.8 KiB
MiniZinc
143 lines
8.8 KiB
MiniZinc
predicate fzn_all_different_int(array [int] of var int: x);
|
|
predicate count(array [int] of var int: x, var int: y, var int: c);
|
|
predicate global_cardinality(array [int] of var int: x, array [int] of int: cover, array [int] of var int: counts);
|
|
predicate table_bool(array [int] of var bool: x, array [int, int] of bool: t);
|
|
predicate table_int(array [int] of var int: x, array [int, int] of int: t);
|
|
array [1..32] of var 1..4096: sx____00001;
|
|
array [1..32] of var 1..4096: sy____00002;
|
|
array [1..32] of var 1..64: x :: output_array([1..32]);
|
|
array [1..32] of var 1..64: y :: output_array([1..32]);
|
|
constraint fzn_all_different_int([x[1], x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9], x[10], x[11], x[12], x[13], x[14], x[15], x[16], x[17], x[18], x[19], x[20], x[21], x[22], x[23], x[24], x[25], x[26], x[27], x[28], x[29], x[30], x[31], x[32], y[1], y[2], y[3], y[4], y[5], y[6], y[7], y[8], y[9], y[10], y[11], y[12], y[13], y[14], y[15], y[16], y[17], y[18], y[19], y[20], y[21], y[22], y[23], y[24], y[25], y[26], y[27], y[28], y[29], y[30], y[31], y[32]]) :: bounds;
|
|
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [sx____00001[1], sx____00001[2], sx____00001[3], sx____00001[4], sx____00001[5], sx____00001[6], sx____00001[7], sx____00001[8], sx____00001[9], sx____00001[10], sx____00001[11], sx____00001[12], sx____00001[13], sx____00001[14], sx____00001[15], sx____00001[16], sx____00001[17], sx____00001[18], sx____00001[19], sx____00001[20], sx____00001[21], sx____00001[22], sx____00001[23], sx____00001[24], sx____00001[25], sx____00001[26], sx____00001[27], sx____00001[28], sx____00001[29], sx____00001[30], sx____00001[31], sx____00001[32]], 44720);
|
|
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [sy____00002[1], sy____00002[2], sy____00002[3], sy____00002[4], sy____00002[5], sy____00002[6], sy____00002[7], sy____00002[8], sy____00002[9], sy____00002[10], sy____00002[11], sy____00002[12], sy____00002[13], sy____00002[14], sy____00002[15], sy____00002[16], sy____00002[17], sy____00002[18], sy____00002[19], sy____00002[20], sy____00002[21], sy____00002[22], sy____00002[23], sy____00002[24], sy____00002[25], sy____00002[26], sy____00002[27], sy____00002[28], sy____00002[29], sy____00002[30], sy____00002[31], sy____00002[32]], 44720);
|
|
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[1], x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9], x[10], x[11], x[12], x[13], x[14], x[15], x[16], x[17], x[18], x[19], x[20], x[21], x[22], x[23], x[24], x[25], x[26], x[27], x[28], x[29], x[30], x[31], x[32]], 1040);
|
|
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [y[1], y[2], y[3], y[4], y[5], y[6], y[7], y[8], y[9], y[10], y[11], y[12], y[13], y[14], y[15], y[16], y[17], y[18], y[19], y[20], y[21], y[22], y[23], y[24], y[25], y[26], y[27], y[28], y[29], y[30], y[31], y[32]], 1040);
|
|
constraint int_lt(x[1], x[2]);
|
|
constraint int_lt(x[1], y[1]);
|
|
constraint int_lt(x[2], x[3]);
|
|
constraint int_lt(x[3], x[4]);
|
|
constraint int_lt(x[4], x[5]);
|
|
constraint int_lt(x[5], x[6]);
|
|
constraint int_lt(x[6], x[7]);
|
|
constraint int_lt(x[7], x[8]);
|
|
constraint int_lt(x[8], x[9]);
|
|
constraint int_lt(x[9], x[10]);
|
|
constraint int_lt(x[10], x[11]);
|
|
constraint int_lt(x[11], x[12]);
|
|
constraint int_lt(x[12], x[13]);
|
|
constraint int_lt(x[13], x[14]);
|
|
constraint int_lt(x[14], x[15]);
|
|
constraint int_lt(x[15], x[16]);
|
|
constraint int_lt(x[16], x[17]);
|
|
constraint int_lt(x[17], x[18]);
|
|
constraint int_lt(x[18], x[19]);
|
|
constraint int_lt(x[19], x[20]);
|
|
constraint int_lt(x[20], x[21]);
|
|
constraint int_lt(x[21], x[22]);
|
|
constraint int_lt(x[22], x[23]);
|
|
constraint int_lt(x[23], x[24]);
|
|
constraint int_lt(x[24], x[25]);
|
|
constraint int_lt(x[25], x[26]);
|
|
constraint int_lt(x[26], x[27]);
|
|
constraint int_lt(x[27], x[28]);
|
|
constraint int_lt(x[28], x[29]);
|
|
constraint int_lt(x[29], x[30]);
|
|
constraint int_lt(x[30], x[31]);
|
|
constraint int_lt(x[31], x[32]);
|
|
constraint int_lt(y[1], y[2]);
|
|
constraint int_lt(y[2], y[3]);
|
|
constraint int_lt(y[3], y[4]);
|
|
constraint int_lt(y[4], y[5]);
|
|
constraint int_lt(y[5], y[6]);
|
|
constraint int_lt(y[6], y[7]);
|
|
constraint int_lt(y[7], y[8]);
|
|
constraint int_lt(y[8], y[9]);
|
|
constraint int_lt(y[9], y[10]);
|
|
constraint int_lt(y[10], y[11]);
|
|
constraint int_lt(y[11], y[12]);
|
|
constraint int_lt(y[12], y[13]);
|
|
constraint int_lt(y[13], y[14]);
|
|
constraint int_lt(y[14], y[15]);
|
|
constraint int_lt(y[15], y[16]);
|
|
constraint int_lt(y[16], y[17]);
|
|
constraint int_lt(y[17], y[18]);
|
|
constraint int_lt(y[18], y[19]);
|
|
constraint int_lt(y[19], y[20]);
|
|
constraint int_lt(y[20], y[21]);
|
|
constraint int_lt(y[21], y[22]);
|
|
constraint int_lt(y[22], y[23]);
|
|
constraint int_lt(y[23], y[24]);
|
|
constraint int_lt(y[24], y[25]);
|
|
constraint int_lt(y[25], y[26]);
|
|
constraint int_lt(y[26], y[27]);
|
|
constraint int_lt(y[27], y[28]);
|
|
constraint int_lt(y[28], y[29]);
|
|
constraint int_lt(y[29], y[30]);
|
|
constraint int_lt(y[30], y[31]);
|
|
constraint int_lt(y[31], y[32]);
|
|
constraint int_times(x[1], x[1], sx____00001[1]);
|
|
constraint int_times(x[2], x[2], sx____00001[2]);
|
|
constraint int_times(x[3], x[3], sx____00001[3]);
|
|
constraint int_times(x[4], x[4], sx____00001[4]);
|
|
constraint int_times(x[5], x[5], sx____00001[5]);
|
|
constraint int_times(x[6], x[6], sx____00001[6]);
|
|
constraint int_times(x[7], x[7], sx____00001[7]);
|
|
constraint int_times(x[8], x[8], sx____00001[8]);
|
|
constraint int_times(x[9], x[9], sx____00001[9]);
|
|
constraint int_times(x[10], x[10], sx____00001[10]);
|
|
constraint int_times(x[11], x[11], sx____00001[11]);
|
|
constraint int_times(x[12], x[12], sx____00001[12]);
|
|
constraint int_times(x[13], x[13], sx____00001[13]);
|
|
constraint int_times(x[14], x[14], sx____00001[14]);
|
|
constraint int_times(x[15], x[15], sx____00001[15]);
|
|
constraint int_times(x[16], x[16], sx____00001[16]);
|
|
constraint int_times(x[17], x[17], sx____00001[17]);
|
|
constraint int_times(x[18], x[18], sx____00001[18]);
|
|
constraint int_times(x[19], x[19], sx____00001[19]);
|
|
constraint int_times(x[20], x[20], sx____00001[20]);
|
|
constraint int_times(x[21], x[21], sx____00001[21]);
|
|
constraint int_times(x[22], x[22], sx____00001[22]);
|
|
constraint int_times(x[23], x[23], sx____00001[23]);
|
|
constraint int_times(x[24], x[24], sx____00001[24]);
|
|
constraint int_times(x[25], x[25], sx____00001[25]);
|
|
constraint int_times(x[26], x[26], sx____00001[26]);
|
|
constraint int_times(x[27], x[27], sx____00001[27]);
|
|
constraint int_times(x[28], x[28], sx____00001[28]);
|
|
constraint int_times(x[29], x[29], sx____00001[29]);
|
|
constraint int_times(x[30], x[30], sx____00001[30]);
|
|
constraint int_times(x[31], x[31], sx____00001[31]);
|
|
constraint int_times(x[32], x[32], sx____00001[32]);
|
|
constraint int_times(y[1], y[1], sy____00002[1]);
|
|
constraint int_times(y[2], y[2], sy____00002[2]);
|
|
constraint int_times(y[3], y[3], sy____00002[3]);
|
|
constraint int_times(y[4], y[4], sy____00002[4]);
|
|
constraint int_times(y[5], y[5], sy____00002[5]);
|
|
constraint int_times(y[6], y[6], sy____00002[6]);
|
|
constraint int_times(y[7], y[7], sy____00002[7]);
|
|
constraint int_times(y[8], y[8], sy____00002[8]);
|
|
constraint int_times(y[9], y[9], sy____00002[9]);
|
|
constraint int_times(y[10], y[10], sy____00002[10]);
|
|
constraint int_times(y[11], y[11], sy____00002[11]);
|
|
constraint int_times(y[12], y[12], sy____00002[12]);
|
|
constraint int_times(y[13], y[13], sy____00002[13]);
|
|
constraint int_times(y[14], y[14], sy____00002[14]);
|
|
constraint int_times(y[15], y[15], sy____00002[15]);
|
|
constraint int_times(y[16], y[16], sy____00002[16]);
|
|
constraint int_times(y[17], y[17], sy____00002[17]);
|
|
constraint int_times(y[18], y[18], sy____00002[18]);
|
|
constraint int_times(y[19], y[19], sy____00002[19]);
|
|
constraint int_times(y[20], y[20], sy____00002[20]);
|
|
constraint int_times(y[21], y[21], sy____00002[21]);
|
|
constraint int_times(y[22], y[22], sy____00002[22]);
|
|
constraint int_times(y[23], y[23], sy____00002[23]);
|
|
constraint int_times(y[24], y[24], sy____00002[24]);
|
|
constraint int_times(y[25], y[25], sy____00002[25]);
|
|
constraint int_times(y[26], y[26], sy____00002[26]);
|
|
constraint int_times(y[27], y[27], sy____00002[27]);
|
|
constraint int_times(y[28], y[28], sy____00002[28]);
|
|
constraint int_times(y[29], y[29], sy____00002[29]);
|
|
constraint int_times(y[30], y[30], sy____00002[30]);
|
|
constraint int_times(y[31], y[31], sy____00002[31]);
|
|
constraint int_times(y[32], y[32], sy____00002[32]);
|
|
solve :: int_search([x[1], x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9], x[10], x[11], x[12], x[13], x[14], x[15], x[16], x[17], x[18], x[19], x[20], x[21], x[22], x[23], x[24], x[25], x[26], x[27], x[28], x[29], x[30], x[31], x[32], y[1], y[2], y[3], y[4], y[5], y[6], y[7], y[8], y[9], y[10], y[11], y[12], y[13], y[14], y[15], y[16], y[17], y[18], y[19], y[20], y[21], y[22], y[23], y[24], y[25], y[26], y[27], y[28], y[29], y[30], y[31], y[32]], first_fail, indomain_min, complete) satisfy;
|