237 lines
13 KiB
MiniZinc
237 lines
13 KiB
MiniZinc
predicate fzn_all_different_int(array [int] of var int: x);
|
|
predicate count_eq(array [int] of var int: x, var int: y, var int: c);
|
|
predicate count_reif(array [int] of var int: x, var int: y, var int: c, var bool: b);
|
|
predicate fixed_fzn_cumulative(array [int] of var int: s, array [int] of int: d, array [int] of int: r, int: b);
|
|
predicate global_cardinality(array [int] of var int: x, array [int] of int: cover, array [int] of var int: counts);
|
|
predicate global_cardinality_closed(array [int] of var int: x, array [int] of int: cover, array [int] of var int: counts);
|
|
predicate global_cardinality_low_up(array [int] of var int: x, array [int] of int: cover, array [int] of int: lbound, array [int] of int: ubound);
|
|
predicate global_cardinality_low_up_closed(array [int] of var int: x, array [int] of int: cover, array [int] of int: lbound, array [int] of int: ubound);
|
|
predicate maximum_int(var int: m, array [int] of var int: x);
|
|
predicate minimum_int(var int: m, array [int] of var int: x);
|
|
predicate sliding_sum(int: low, int: up, int: seq, array [int] of var int: vs);
|
|
predicate sort(array [int] of var int: x, array [int] of var int: y);
|
|
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);
|
|
predicate var_fzn_cumulative(array [int] of var int: s, array [int] of int: d, array [int] of int: r, var int: b);
|
|
array [1..27] of var 0..2: bin_code :: output_array([1..27]);
|
|
array [1..81] of var 0..2: binary;
|
|
array [1..3] of var 0..2: t____00001;
|
|
array [1..3] of var 0..2: t____00002;
|
|
array [1..3] of var 0..2: t____00003;
|
|
array [1..3] of var 0..2: t____00004;
|
|
array [1..3] of var 0..2: t____00005;
|
|
array [1..3] of var 0..2: t____00006;
|
|
array [1..3] of var 0..2: t____00007;
|
|
array [1..3] of var 0..2: t____00008;
|
|
array [1..3] of var 0..2: t____00009;
|
|
array [1..3] of var 0..2: t____00010;
|
|
array [1..3] of var 0..2: t____00011;
|
|
array [1..3] of var 0..2: t____00012;
|
|
array [1..3] of var 0..2: t____00013;
|
|
array [1..3] of var 0..2: t____00014;
|
|
array [1..3] of var 0..2: t____00015;
|
|
array [1..3] of var 0..2: t____00016;
|
|
array [1..3] of var 0..2: t____00017;
|
|
array [1..3] of var 0..2: t____00018;
|
|
array [1..3] of var 0..2: t____00019;
|
|
array [1..3] of var 0..2: t____00020;
|
|
array [1..3] of var 0..2: t____00021;
|
|
array [1..3] of var 0..2: t____00022;
|
|
array [1..3] of var 0..2: t____00023;
|
|
array [1..3] of var 0..2: t____00024;
|
|
array [1..3] of var 0..2: t____00025;
|
|
array [1..3] of var 0..2: t____00026;
|
|
array [1..3] of var 0..2: t____00027;
|
|
array [1..27] of var 0..26: x :: output_array([1..27]);
|
|
constraint fzn_all_different_int(x);
|
|
constraint int_eq(binary[1], t____00001[1]);
|
|
constraint int_eq(binary[2], binary[4]);
|
|
constraint int_eq(binary[2], t____00001[2]);
|
|
constraint int_eq(binary[3], binary[5]);
|
|
constraint int_eq(binary[3], t____00001[3]);
|
|
constraint int_eq(binary[4], t____00002[1]);
|
|
constraint int_eq(binary[5], binary[7]);
|
|
constraint int_eq(binary[5], t____00002[2]);
|
|
constraint int_eq(binary[6], binary[8]);
|
|
constraint int_eq(binary[6], t____00002[3]);
|
|
constraint int_eq(binary[7], t____00003[1]);
|
|
constraint int_eq(binary[8], binary[10]);
|
|
constraint int_eq(binary[8], t____00003[2]);
|
|
constraint int_eq(binary[9], binary[11]);
|
|
constraint int_eq(binary[9], t____00003[3]);
|
|
constraint int_eq(binary[10], t____00004[1]);
|
|
constraint int_eq(binary[11], binary[13]);
|
|
constraint int_eq(binary[11], t____00004[2]);
|
|
constraint int_eq(binary[12], binary[14]);
|
|
constraint int_eq(binary[12], t____00004[3]);
|
|
constraint int_eq(binary[13], t____00005[1]);
|
|
constraint int_eq(binary[14], binary[16]);
|
|
constraint int_eq(binary[14], t____00005[2]);
|
|
constraint int_eq(binary[15], binary[17]);
|
|
constraint int_eq(binary[15], t____00005[3]);
|
|
constraint int_eq(binary[16], t____00006[1]);
|
|
constraint int_eq(binary[17], binary[19]);
|
|
constraint int_eq(binary[17], t____00006[2]);
|
|
constraint int_eq(binary[18], binary[20]);
|
|
constraint int_eq(binary[18], t____00006[3]);
|
|
constraint int_eq(binary[19], t____00007[1]);
|
|
constraint int_eq(binary[20], binary[22]);
|
|
constraint int_eq(binary[20], t____00007[2]);
|
|
constraint int_eq(binary[21], binary[23]);
|
|
constraint int_eq(binary[21], t____00007[3]);
|
|
constraint int_eq(binary[22], t____00008[1]);
|
|
constraint int_eq(binary[23], binary[25]);
|
|
constraint int_eq(binary[23], t____00008[2]);
|
|
constraint int_eq(binary[24], binary[26]);
|
|
constraint int_eq(binary[24], t____00008[3]);
|
|
constraint int_eq(binary[25], t____00009[1]);
|
|
constraint int_eq(binary[26], binary[28]);
|
|
constraint int_eq(binary[26], t____00009[2]);
|
|
constraint int_eq(binary[27], binary[29]);
|
|
constraint int_eq(binary[27], t____00009[3]);
|
|
constraint int_eq(binary[28], t____00010[1]);
|
|
constraint int_eq(binary[29], binary[31]);
|
|
constraint int_eq(binary[29], t____00010[2]);
|
|
constraint int_eq(binary[30], binary[32]);
|
|
constraint int_eq(binary[30], t____00010[3]);
|
|
constraint int_eq(binary[31], t____00011[1]);
|
|
constraint int_eq(binary[32], binary[34]);
|
|
constraint int_eq(binary[32], t____00011[2]);
|
|
constraint int_eq(binary[33], binary[35]);
|
|
constraint int_eq(binary[33], t____00011[3]);
|
|
constraint int_eq(binary[34], t____00012[1]);
|
|
constraint int_eq(binary[35], binary[37]);
|
|
constraint int_eq(binary[35], t____00012[2]);
|
|
constraint int_eq(binary[36], binary[38]);
|
|
constraint int_eq(binary[36], t____00012[3]);
|
|
constraint int_eq(binary[37], t____00013[1]);
|
|
constraint int_eq(binary[38], binary[40]);
|
|
constraint int_eq(binary[38], t____00013[2]);
|
|
constraint int_eq(binary[39], binary[41]);
|
|
constraint int_eq(binary[39], t____00013[3]);
|
|
constraint int_eq(binary[40], t____00014[1]);
|
|
constraint int_eq(binary[41], binary[43]);
|
|
constraint int_eq(binary[41], t____00014[2]);
|
|
constraint int_eq(binary[42], binary[44]);
|
|
constraint int_eq(binary[42], t____00014[3]);
|
|
constraint int_eq(binary[43], t____00015[1]);
|
|
constraint int_eq(binary[44], binary[46]);
|
|
constraint int_eq(binary[44], t____00015[2]);
|
|
constraint int_eq(binary[45], binary[47]);
|
|
constraint int_eq(binary[45], t____00015[3]);
|
|
constraint int_eq(binary[46], t____00016[1]);
|
|
constraint int_eq(binary[47], binary[49]);
|
|
constraint int_eq(binary[47], t____00016[2]);
|
|
constraint int_eq(binary[48], binary[50]);
|
|
constraint int_eq(binary[48], t____00016[3]);
|
|
constraint int_eq(binary[49], t____00017[1]);
|
|
constraint int_eq(binary[50], binary[52]);
|
|
constraint int_eq(binary[50], t____00017[2]);
|
|
constraint int_eq(binary[51], binary[53]);
|
|
constraint int_eq(binary[51], t____00017[3]);
|
|
constraint int_eq(binary[52], t____00018[1]);
|
|
constraint int_eq(binary[53], binary[55]);
|
|
constraint int_eq(binary[53], t____00018[2]);
|
|
constraint int_eq(binary[54], binary[56]);
|
|
constraint int_eq(binary[54], t____00018[3]);
|
|
constraint int_eq(binary[55], t____00019[1]);
|
|
constraint int_eq(binary[56], binary[58]);
|
|
constraint int_eq(binary[56], t____00019[2]);
|
|
constraint int_eq(binary[57], binary[59]);
|
|
constraint int_eq(binary[57], t____00019[3]);
|
|
constraint int_eq(binary[58], t____00020[1]);
|
|
constraint int_eq(binary[59], binary[61]);
|
|
constraint int_eq(binary[59], t____00020[2]);
|
|
constraint int_eq(binary[60], binary[62]);
|
|
constraint int_eq(binary[60], t____00020[3]);
|
|
constraint int_eq(binary[61], t____00021[1]);
|
|
constraint int_eq(binary[62], binary[64]);
|
|
constraint int_eq(binary[62], t____00021[2]);
|
|
constraint int_eq(binary[63], binary[65]);
|
|
constraint int_eq(binary[63], t____00021[3]);
|
|
constraint int_eq(binary[64], t____00022[1]);
|
|
constraint int_eq(binary[65], binary[67]);
|
|
constraint int_eq(binary[65], t____00022[2]);
|
|
constraint int_eq(binary[66], binary[68]);
|
|
constraint int_eq(binary[66], t____00022[3]);
|
|
constraint int_eq(binary[67], t____00023[1]);
|
|
constraint int_eq(binary[68], binary[70]);
|
|
constraint int_eq(binary[68], t____00023[2]);
|
|
constraint int_eq(binary[69], binary[71]);
|
|
constraint int_eq(binary[69], t____00023[3]);
|
|
constraint int_eq(binary[70], t____00024[1]);
|
|
constraint int_eq(binary[71], binary[73]);
|
|
constraint int_eq(binary[71], t____00024[2]);
|
|
constraint int_eq(binary[72], binary[74]);
|
|
constraint int_eq(binary[72], t____00024[3]);
|
|
constraint int_eq(binary[73], t____00025[1]);
|
|
constraint int_eq(binary[74], binary[76]);
|
|
constraint int_eq(binary[74], t____00025[2]);
|
|
constraint int_eq(binary[75], binary[77]);
|
|
constraint int_eq(binary[75], t____00025[3]);
|
|
constraint int_eq(binary[76], t____00026[1]);
|
|
constraint int_eq(binary[77], binary[79]);
|
|
constraint int_eq(binary[77], t____00026[2]);
|
|
constraint int_eq(binary[78], binary[80]);
|
|
constraint int_eq(binary[78], t____00026[3]);
|
|
constraint int_eq(binary[79], t____00027[1]);
|
|
constraint int_eq(binary[80], binary[1]);
|
|
constraint int_eq(binary[80], t____00027[2]);
|
|
constraint int_eq(binary[81], binary[2]);
|
|
constraint int_eq(binary[81], t____00027[3]);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00001[1], t____00001[2], t____00001[3], x[1]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00002[1], t____00002[2], t____00002[3], x[2]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00003[1], t____00003[2], t____00003[3], x[3]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00004[1], t____00004[2], t____00004[3], x[4]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00005[1], t____00005[2], t____00005[3], x[5]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00006[1], t____00006[2], t____00006[3], x[6]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00007[1], t____00007[2], t____00007[3], x[7]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00008[1], t____00008[2], t____00008[3], x[8]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00009[1], t____00009[2], t____00009[3], x[9]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00010[1], t____00010[2], t____00010[3], x[10]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00011[1], t____00011[2], t____00011[3], x[11]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00012[1], t____00012[2], t____00012[3], x[12]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00013[1], t____00013[2], t____00013[3], x[13]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00014[1], t____00014[2], t____00014[3], x[14]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00015[1], t____00015[2], t____00015[3], x[15]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00016[1], t____00016[2], t____00016[3], x[16]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00017[1], t____00017[2], t____00017[3], x[17]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00018[1], t____00018[2], t____00018[3], x[18]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00019[1], t____00019[2], t____00019[3], x[19]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00020[1], t____00020[2], t____00020[3], x[20]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00021[1], t____00021[2], t____00021[3], x[21]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00022[1], t____00022[2], t____00022[3], x[22]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00023[1], t____00023[2], t____00023[3], x[23]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00024[1], t____00024[2], t____00024[3], x[24]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00025[1], t____00025[2], t____00025[3], x[25]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00026[1], t____00026[2], t____00026[3], x[26]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00027[1], t____00027[2], t____00027[3], x[27]], 0);
|
|
constraint int_ne(bin_code[1], bin_code[2]);
|
|
constraint int_ne(bin_code[1], bin_code[27]);
|
|
constraint int_ne(bin_code[2], bin_code[3]);
|
|
constraint int_ne(bin_code[3], bin_code[4]);
|
|
constraint int_ne(bin_code[4], bin_code[5]);
|
|
constraint int_ne(bin_code[5], bin_code[6]);
|
|
constraint int_ne(bin_code[6], bin_code[7]);
|
|
constraint int_ne(bin_code[7], bin_code[8]);
|
|
constraint int_ne(bin_code[8], bin_code[9]);
|
|
constraint int_ne(bin_code[9], bin_code[10]);
|
|
constraint int_ne(bin_code[10], bin_code[11]);
|
|
constraint int_ne(bin_code[11], bin_code[12]);
|
|
constraint int_ne(bin_code[12], bin_code[13]);
|
|
constraint int_ne(bin_code[13], bin_code[14]);
|
|
constraint int_ne(bin_code[14], bin_code[15]);
|
|
constraint int_ne(bin_code[15], bin_code[16]);
|
|
constraint int_ne(bin_code[16], bin_code[17]);
|
|
constraint int_ne(bin_code[17], bin_code[18]);
|
|
constraint int_ne(bin_code[18], bin_code[19]);
|
|
constraint int_ne(bin_code[19], bin_code[20]);
|
|
constraint int_ne(bin_code[20], bin_code[21]);
|
|
constraint int_ne(bin_code[21], bin_code[22]);
|
|
constraint int_ne(bin_code[22], bin_code[23]);
|
|
constraint int_ne(bin_code[23], bin_code[24]);
|
|
constraint int_ne(bin_code[24], bin_code[25]);
|
|
constraint int_ne(bin_code[25], bin_code[26]);
|
|
constraint int_ne(bin_code[26], bin_code[27]);
|
|
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], bin_code[1], bin_code[2], bin_code[3], bin_code[4], bin_code[5], bin_code[6], bin_code[7], bin_code[8], bin_code[9], bin_code[10], bin_code[11], bin_code[12], bin_code[13], bin_code[14], bin_code[15], bin_code[16], bin_code[17], bin_code[18], bin_code[19], bin_code[20], bin_code[21], bin_code[22], bin_code[23], bin_code[24], bin_code[25], bin_code[26], bin_code[27]], first_fail, indomain_split, credit(5, bbs(1))) satisfy;
|