Dekker1/MiniZinc-Auto-Tabling-Models
Archived
1
0
Fork 0
Code

Add the models used in the CPAIOR 2017 paper

Browse Source
This commit is contained in:
Jip J. Dekker 2016-11-21 17:54:04 +01:00
parent 24368859ae
commit 1271ba14d0
86 changed files with 93518 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

120
black-hole/black-hole.mzn Normal file
View File

@ -0,0 +1,120 @@
%------------------------------------------------------------------------%
% Solving the Black Hole Patience game
%------------------------------------------------------------------------%
%
% The model of the problem is taken from "Search in the Patience Game
% 'Black Hole'", by Ian P. Gent, Chris Jefferson, Tom Kelsey, Inês
% Lynce, Ian Miguel, Peter Nightingale, Barbara M. Smith, and
% S. Armagan Tarim. It only implements the basic model. The instances
% are generated by the black hole patience model in the Gecode
% distribution.
%
% This model uses the following global constraints
% - inverse
% - table
%
% Main authors:
% Mikael Zayenz Lagerkvist <lagerkvist@gecode.org>
%
% Copyright:
% Mikael Zayenz Lagerkvist, 2009
%
% Permission is hereby granted, free of charge, to any person obtaining
% a copy of this software and associated documentation files (the
% "Software"), to deal in the Software without restriction, including
% without limitation the rights to use, copy, modify, merge, publish,
% distribute, sublicense, and/or sell copies of the Software, and to
% permit persons to whom the Software is furnished to do so, subject to
% the following conditions:
%
% The above copyright notice and this permission notice shall be
% included in all copies or substantial portions of the Software.
%
% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
%
%------------------------------------------------------------------------%
include "table.mzn";
include "inverse.mzn";
%------------------------------------------------------------------------%
% Parameters
%------------------------------------------------------------------------%
% Piles
array[1..17, 1..3] of int: layout;
% Data
%layout = array2d(1..17,1..3, [
%31, 30, 8,
%45, 50, 19,
%37, 12, 47,
%24, 9, 18,
%16, 40, 20,
%38, 36, 49,
%11, 33, 51,
%39, 10, 14,
%3, 27, 46,
%29, 2, 35,
%4, 32, 17,
%15, 13, 5,
%23, 34, 28,
%48, 21, 52,
%22, 6, 42,
%44, 41, 26,
%25, 43, 7
%]);
%------------------------------------------------------------------------%
% Variables
%------------------------------------------------------------------------%
% Card at position
array[1..52] of var 1..52: x;
% Position of card
array[1..52] of var 1..52: y;
%------------------------------------------------------------------------%
% Constraints
%------------------------------------------------------------------------%
% Ace of Spades is first card
constraint x[1] == 1;
% Consecutive cards match
predicate rank_apart(var 1..52: a, var 1..52: b) ::presolve
= abs( (a - b) mod 13 ) in {1,12};
constraint forall(i in 1..51) ( rank_apart(x[i], x[i+1]) );
% Link x and y
constraint inverse(x, y) :: domain;
% A card must be played before the one under it.
constraint
forall(i in 1..17, j in 1..2) (
y[layout[i,j]] < y[layout[i,j+1]]
);
%------------------------------------------------------------------------%
% Search
%------------------------------------------------------------------------%
solve :: int_search(x,
input_order,
indomain_min,
complete)
satisfy;
output [ "black-hole: ", show(x), "\n" ];

19
black-hole/instances/0.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
31, 30, 8,
45, 50, 19,
37, 12, 47,
24, 9, 18,
16, 40, 20,
38, 36, 49,
11, 33, 51,
39, 10, 14,
3, 27, 46,
29, 2, 35,
4, 32, 17,
15, 13, 5,
23, 34, 28,
48, 21, 52,
22, 6, 42,
44, 41, 26,
25, 43, 7
]);

19
black-hole/instances/1.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
20, 39, 6,
34, 31, 32,
15, 33, 38,
40, 4, 43,
16, 37, 7,
2, 18, 19,
8, 41, 47,
35, 25, 51,
28, 5, 21,
45, 24, 23,
9, 3, 46,
27, 52, 26,
14, 30, 44,
36, 12, 49,
10, 29, 42,
48, 50, 13,
17, 11, 22
]);

19
black-hole/instances/10.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
6, 22, 20,
33, 18, 31,
44, 4, 2,
51, 38, 23,
41, 14, 5,
34, 52, 39,
46, 19, 49,
10, 25, 15,
45, 43, 32,
26, 21, 11,
27, 47, 37,
28, 17, 50,
7, 3, 24,
30, 42, 16,
40, 35, 29,
36, 8, 48,
13, 12, 9
]);

19
black-hole/instances/11.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
10, 40, 12,
21, 3, 9,
47, 31, 20,
19, 45, 6,
7, 4, 35,
26, 30, 28,
25, 18, 32,
34, 46, 49,
15, 22, 42,
13, 41, 2,
11, 5, 44,
8, 43, 39,
36, 29, 17,
38, 33, 52,
24, 23, 37,
14, 51, 48,
27, 50, 16
]);

19
black-hole/instances/12.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
13, 28, 25,
21, 5, 43,
4, 9, 30,
40, 33, 51,
48, 52, 10,
37, 27, 12,
41, 6, 3,
42, 16, 35,
38, 18, 14,
45, 17, 49,
29, 24, 36,
31, 50, 39,
32, 8, 7,
46, 47, 20,
23, 34, 2,
15, 19, 26,
44, 22, 11
]);

19
black-hole/instances/13.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
43, 29, 24,
12, 18, 37,
28, 10, 42,
48, 33, 9,
15, 4, 44,
21, 22, 17,
25, 38, 5,
45, 23, 13,
51, 19, 7,
16, 49, 6,
50, 47, 31,
3, 40, 32,
2, 39, 30,
34, 11, 14,
35, 20, 46,
27, 52, 8,
26, 36, 41
]);

19
black-hole/instances/14.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
26, 17, 22,
19, 41, 46,
5, 12, 13,
31, 42, 3,
49, 30, 36,
38, 48, 52,
20, 34, 2,
9, 28, 24,
44, 11, 33,
50, 43, 16,
45, 4, 47,
29, 37, 51,
32, 8, 21,
35, 39, 14,
15, 7, 10,
27, 6, 18,
23, 40, 25
]);

19
black-hole/instances/15.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
28, 30, 11,
2, 48, 20,
29, 44, 9,
45, 47, 40,
24, 10, 19,
14, 15, 51,
5, 43, 46,
8, 18, 32,
37, 22, 36,
31, 50, 49,
7, 12, 52,
27, 4, 39,
33, 23, 38,
25, 41, 35,
42, 17, 3,
34, 13, 26,
21, 6, 16
]);

19
black-hole/instances/16.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
20, 26, 2,
10, 6, 45,
14, 15, 21,
27, 51, 41,
19, 48, 8,
44, 52, 33,
39, 47, 7,
17, 46, 37,
13, 11, 40,
32, 29, 9,
3, 12, 42,
28, 35, 50,
34, 30, 24,
43, 22, 16,
5, 49, 31,
25, 4, 36,
18, 38, 23
]);

19
black-hole/instances/17.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
46, 29, 48,
50, 31, 26,
25, 38, 13,
42, 4, 52,
40, 19, 45,
23, 44, 47,
16, 7, 21,
6, 30, 3,
34, 24, 41,
22, 5, 39,
12, 8, 17,
20, 43, 18,
11, 36, 27,
49, 51, 33,
14, 10, 37,
32, 28, 2,
35, 15, 9
]);

19
black-hole/instances/18.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
48, 27, 46,
49, 18, 40,
33, 26, 32,
36, 14, 6,
44, 31, 42,
5, 43, 15,
38, 10, 29,
21, 20, 22,
25, 34, 19,
52, 13, 37,
28, 39, 12,
23, 30, 2,
47, 7, 3,
8, 9, 16,
51, 50, 41,
24, 45, 35,
11, 4, 17
]);

19
black-hole/instances/19.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
49, 25, 9,
37, 6, 19,
21, 50, 44,
40, 35, 52,
10, 11, 41,
7, 4, 13,
15, 36, 2,
32, 18, 31,
30, 26, 39,
14, 24, 8,
48, 12, 46,
29, 28, 34,
43, 27, 16,
42, 38, 33,
23, 51, 22,
17, 3, 5,
20, 47, 45
]);

19
black-hole/instances/2.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
38, 25, 14,
8, 11, 13,
18, 52, 19,
30, 46, 16,
9, 41, 29,
22, 35, 27,
21, 15, 10,
50, 48, 7,
37, 51, 49,
23, 47, 43,
40, 3, 6,
28, 42, 20,
34, 12, 2,
36, 33, 45,
32, 39, 4,
26, 31, 5,
24, 17, 44
]);

19
black-hole/instances/20.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
13, 22, 5,
15, 37, 6,
14, 38, 49,
50, 23, 51,
27, 48, 10,
9, 8, 16,
26, 44, 43,
35, 34, 30,
11, 20, 40,
17, 31, 47,
29, 41, 28,
4, 18, 39,
12, 42, 25,
2, 52, 33,
36, 19, 32,
24, 7, 45,
21, 3, 46
]);

19
black-hole/instances/3.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
25, 47, 51,
23, 24, 41,
52, 10, 7,
36, 49, 35,
16, 21, 4,
12, 45, 9,
50, 28, 3,
20, 46, 43,
44, 22, 32,
34, 6, 31,
40, 27, 33,
15, 38, 14,
37, 39, 42,
26, 19, 5,
29, 2, 18,
13, 48, 11,
8, 17, 30
]);

19
black-hole/instances/4.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
39, 46, 5,
37, 38, 32,
49, 31, 48,
11, 6, 22,
2, 43, 13,
17, 26, 16,
4, 29, 8,
24, 20, 34,
42, 27, 52,
19, 35, 15,
41, 36, 40,
44, 7, 9,
33, 45, 51,
10, 23, 47,
3, 14, 21,
25, 30, 18,
50, 28, 12
]);

19
black-hole/instances/5.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
42, 38, 4,
45, 41, 21,
28, 15, 43,
30, 26, 25,
51, 7, 39,
22, 47, 8,
16, 46, 12,
29, 40, 18,
19, 5, 33,
13, 35, 20,
17, 36, 23,
34, 6, 27,
14, 24, 11,
52, 9, 49,
10, 2, 3,
44, 48, 31,
37, 50, 32
]);

19
black-hole/instances/6.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
40, 42, 24,
31, 39, 37,
48, 22, 36,
19, 29, 44,
51, 7, 45,
49, 38, 14,
25, 27, 16,
15, 12, 52,
20, 46, 8,
32, 18, 2,
30, 21, 13,
5, 9, 33,
11, 3, 17,
4, 50, 47,
10, 6, 23,
34, 35, 28,
43, 26, 41
]);

19
black-hole/instances/7.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
37, 36, 18,
50, 30, 25,
47, 21, 52,
9, 34, 28,
20, 19, 2,
14, 29, 6,
5, 13, 51,
23, 38, 45,
16, 27, 24,
46, 32, 44,
40, 17, 12,
33, 4, 42,
43, 10, 3,
26, 31, 35,
15, 48, 11,
8, 49, 7,
39, 22, 41
]);

19
black-hole/instances/8.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
43, 50, 35,
6, 34, 38,
7, 11, 40,
51, 36, 3,
42, 41, 31,
33, 18, 24,
49, 28, 2,
29, 13, 8,
30, 22, 37,
25, 9, 26,
14, 39, 19,
27, 44, 4,
17, 23, 47,
46, 52, 48,
10, 45, 15,
5, 16, 21,
20, 32, 12
]);

19
black-hole/instances/9.dzn Normal file
View File

@ -0,0 +1,19 @@
layout = array2d(1..17,1..3, [
31, 15, 22,
43, 35, 20,
24, 9, 48,
32, 25, 12,
8, 52, 27,
26, 44, 38,
29, 41, 36,
28, 23, 10,
50, 7, 2,
30, 40, 39,
4, 13, 33,
42, 45, 16,
21, 17, 46,
5, 18, 14,
34, 11, 37,
51, 3, 19,
6, 49, 47
]);

128
block-party/block-party.mzn Normal file
View File

@ -0,0 +1,128 @@
/*
* author: Jean-Noël Monette
*/
include "globals.mzn";
%cubes
set of int: cubes=1..8;
int: ud=0;
int: lr=8;
int: fb=16;
set of int: pos=1..24;
set of int: symbols=0..4*4*4-1;
array[cubes] of var cubes: cube_at;
array[pos] of var symbols: symbol_at;
%Each cube is placed once.
constraint alldifferent(cube_at);
%Party constraints on the 6 faces
constraint party([symbol_at[i] | i in 1..4]);
constraint party([symbol_at[i + 4] | i in 1..4]);
constraint party([symbol_at[(i - 1) * 2 + 1 + lr] | i in 1..4]);
constraint party([symbol_at[i * 2 + lr] | i in 1..4]);
constraint party([symbol_at[if i < 3 then i else i+2 endif + fb] | i in 1..4]);
constraint party([symbol_at[if i < 3 then i else i+2 endif + 2 + fb] | i in 1..4]);
%Linking cubes and symbols
constraint forall(i in {1,4,6,7})(
link_cube_and_symbols([cube_at[i],symbol_at[i+ud],symbol_at[i+lr],symbol_at[i+fb]]));
constraint forall(i in {2,3,5,8})(
link_cube_and_symbols([cube_at[i],symbol_at[i+ud],symbol_at[i+fb],symbol_at[i+lr]]));
%Sym break
constraint cube_at[1] = 1;
constraint cube_at[2] < cube_at[3];
constraint cube_at[2] < cube_at[5];
%better to search on symbol_at first rather than cube_at
solve :: int_search(symbol_at, first_fail, indomain_min, complete) satisfy;
%introduced because of limitation in output.
array[pos] of var 0..3: color_at = [color(symbol_at[i]) |i in pos];
array[pos] of var 0..3: shape_at = [shape(symbol_at[i]) |i in pos];
array[pos] of var 0..3: fill_at = [fill(symbol_at[i]) |i in pos];
%names (for output)
array[1..4] of string: colorname = ["blue","red","yellow","black"];
array[1..4] of string: fillname = ["half","plain","empty","grid"];
array[1..4] of string: shapename = ["triangle","circle","square","heart"];
output [show(cube_at), "\n", show(symbol_at), "\n"] ++
["pos " ++ show(i) ++ ": cube " ++ show(cube_at[i]) ++ "\n"
++ "u/d:\t"++fillname[fix(fill_at[i+ud])+1]++"\t"++colorname[fix(color_at[i+ud])+1]++"\t"++shapename[fix(shape_at[i+ud])+1]++"\n"
++ "f/b:\t"++fillname[fix(fill_at[i+fb])+1]++"\t"++colorname[fix(color_at[i+fb])+1]++"\t"++shapename[fix(shape_at[i+fb])+1]++"\n"
++ "l/r:\t"++fillname[fix(fill_at[i+lr])+1]++"\t"++colorname[fix(color_at[i+lr])+1]++"\t"++shapename[fix(shape_at[i+lr])+1]++"\n"
| i in 1..8];%fill
predicate diff_or_equal(array[1..4] of var 0..3: x)
=
forall(i in 1..4,j in i+1..4)(x[i]!=x[j])
\/
forall(i in 1..4,j in i+1..4)(x[i]=x[j]);
% A party is alldiff or allequal for each of the three characteristics.
predicate party(array[1..4] of var 0..63: symbols)
= (
diff_or_equal([color(symbols[i]) | i in 1..4])
/\ diff_or_equal([shape(symbols[i]) | i in 1..4])
/\ diff_or_equal([fill(symbols[i]) | i in 1..4])
);
%Linking cube IDs with the three symbols appearing in relevant positions
predicate link_cube_and_symbols(array[1..4] of var int: cs) ::presolve
= let{
var 1..24: pos;
var int: cube = cs[1];
} in forall(i in 1..3)(data[cube,pp[pos,i]]=cs[i+1]);
%How to implement linking functions with the advantages of CSE.
function array[1..3] of var 0..3: fcs(var 0..63:symbol) :: promise_total =
let { var 0..3: color; var 0..3:shape;var 0..3: fill;
constraint symbol = 4*4*fill+4*color+shape; }
in [fill,color,shape];
function var 0..3: color_help(array[1..3] of var 0..3: fcs) :: promise_total = fcs[2];
function var 0..3: color(var int:symbol) ::promise_total = color_help(fcs(symbol));
function var 0..3: fill_help(array[1..3] of var 0..3: fcs) :: promise_total = fcs[1];
function var 0..3: fill(var int:symbol) ::promise_total = fill_help(fcs(symbol));
function var 0..3: shape_help(array[1..3] of var 0..3: fcs) :: promise_total = fcs[3];
function var 0..3: shape(var int:symbol) ::promise_total = shape_help(fcs(symbol));
%For parameters
function 0..3: shape(int: symbol) = symbol mod 4;
function 0..3: color(int: symbol) = symbol mod 16 div 4;
function 0..3: fill(int:symbol) = symbol div 16;
array[1..8,1..24] of int: data;
%Which symbol positions on a cube are next to each other on the same corner.
%Made by hand, I do not think there is any hope for finding a simple formula that could be used in precomputation :-)
%Actually it might be divided by three and have a disjunction in link_cube_and_symbols
array[1..24,1..3] of int: pp = [|21,12,7
|23,17,11
|24,4,18
|22,8,3
|1,6,16
|2,14,20
|4,18,24
|3,22,8
|7,21,12
|5,10,15
|6,16,1
|8,3,22
|16,1,6
|15,5,10
|13,9,19
|14,20,2
|18,24,4
|20,2,14
|19,13,9
|17,11,23
|12,7,21
|11,23,17
|9,19,13
|10,15,5
|];

13
block-party/instances/1176.dzn Normal file
View File

@ -0,0 +1,13 @@
data =[| 52, 29, 10, 60, 23, 24, 7, 31, 48, 47, 1, 26, 37, 22, 61, 5, 58, 27, 25, 28, 2, 40, 21, 14 |
45, 22, 36, 9, 51, 53, 44, 5, 30, 49, 46, 57, 43, 23, 60, 29, 18, 34, 27, 14, 61, 59, 41, 1 |
53, 13, 5, 20, 63, 24, 60, 59, 31, 51, 56, 49, 22, 12, 28, 47, 40, 52, 27, 39, 26, 43, 54, 57 |
13, 41, 39, 8, 33, 35, 46, 55, 0, 24, 62, 61, 54, 34, 20, 50, 51, 6, 63, 52, 1, 18, 21, 11 |
37, 18, 33, 9, 30, 56, 50, 8, 4, 42, 23, 13, 43, 45, 21, 0, 12, 41, 20, 63, 28, 38, 36, 7 |
49, 34, 0, 56, 47, 57, 26, 54, 35, 32, 3, 29, 10, 39, 19, 58, 59, 9, 2, 17, 36, 8, 15, 16 |
58, 19, 53, 3, 62, 12, 55, 32, 42, 48, 6, 15, 16, 50, 30, 35, 33, 17, 4, 25, 11, 2, 38, 44 |
14, 48, 42, 3, 55, 25, 4, 11, 38, 37, 44, 19, 46, 31, 16, 15, 32, 7, 6, 45, 17, 10, 40, 62 |]
;
% cubes: [4, 3, 7, 6, 2, 5, 1, 8]
% symbols: [46, 22, 2, 58, 18, 23, 28, 25, 1, 27, 53, 49, 41, 36, 29, 14, 61, 31, 32, 57, 46, 12, 22, 15]
% rotations: [9, 15, 4, 13, 20, 22, 18, 11]

13
block-party/instances/1266.dzn Normal file
View File

@ -0,0 +1,13 @@
data =[| 14, 2, 29, 16, 33, 3, 63, 47, 6, 26, 19, 34, 31, 44, 23, 9, 38, 49, 27, 7, 32, 37, 52, 17 |
14, 47, 57, 53, 59, 37, 48, 41, 27, 12, 7, 52, 20, 44, 17, 21, 13, 43, 1, 10, 6, 23, 39, 9 |
2, 27, 18, 10, 35, 53, 7, 33, 58, 57, 50, 30, 36, 31, 14, 4, 44, 12, 63, 49, 23, 52, 15, 19 |
25, 34, 3, 40, 2, 33, 16, 43, 18, 31, 45, 21, 48, 10, 53, 24, 28, 59, 41, 4, 13, 57, 35, 63 |
38, 18, 36, 26, 41, 60, 43, 22, 48, 28, 42, 46, 9, 20, 50, 56, 3, 37, 24, 17, 39, 8, 62, 45 |
46, 0, 1, 16, 15, 25, 4, 19, 30, 34, 36, 13, 61, 51, 60, 40, 8, 26, 39, 11, 54, 5, 55, 62 |
46, 29, 6, 30, 25, 59, 62, 35, 60, 28, 38, 11, 32, 5, 56, 42, 0, 54, 51, 22, 55, 1, 61, 58 |
42, 32, 54, 21, 11, 49, 24, 15, 29, 58, 8, 51, 0, 55, 22, 50, 5, 45, 40, 12, 47, 61, 20, 56 |]
;
% cubes: [8, 3, 2, 7, 1, 6, 5, 4]
% symbols: [49, 33, 17, 1, 31, 16, 26, 21, 50, 52, 12, 35, 27, 26, 37, 13, 42, 18, 59, 6, 6, 62, 45, 16]
% rotations: [11, 12, 14, 4, 15, 7, 7, 21]

13
block-party/instances/2254.dzn Normal file
View File

@ -0,0 +1,13 @@
data =[| 63, 11, 0, 62, 39, 55, 15, 60, 19, 29, 45, 46, 9, 44, 21, 41, 7, 56, 26, 18, 34, 38, 52, 23 |
31, 6, 10, 38, 51, 57, 42, 44, 16, 48, 11, 4, 15, 63, 35, 2, 49, 25, 8, 47, 54, 39, 21, 9 |
23, 62, 49, 9, 25, 44, 55, 63, 11, 60, 36, 39, 33, 10, 21, 19, 56, 17, 6, 34, 32, 61, 59, 7 |
49, 25, 57, 6, 42, 13, 41, 5, 36, 16, 28, 7, 50, 27, 2, 20, 10, 38, 35, 26, 0, 55, 43, 32 |
47, 43, 12, 19, 54, 52, 28, 46, 42, 24, 20, 45, 0, 23, 48, 29, 3, 58, 18, 50, 16, 37, 2, 56 |
30, 8, 50, 4, 40, 32, 46, 59, 48, 1, 5, 17, 27, 37, 28, 34, 12, 18, 45, 20, 35, 14, 53, 22 |
43, 51, 54, 59, 17, 24, 37, 61, 60, 58, 14, 40, 29, 8, 36, 1, 31, 13, 62, 22, 3, 30, 33, 53 |
57, 33, 31, 3, 61, 5, 15, 22, 12, 58, 1, 4, 14, 53, 30, 26, 40, 51, 41, 24, 52, 13, 27, 47 |]
;
% cubes: [4, 7, 6, 8, 5, 2, 3, 1]
% symbols: [28, 62, 45, 15, 47, 51, 11, 23, 43, 60, 48, 52, 29, 48, 6, 56, 10, 29, 27, 4, 52, 35, 33, 62]
% rotations: [22, 19, 19, 9, 5, 10, 23, 3]

13
block-party/instances/3237.dzn Normal file
View File

@ -0,0 +1,13 @@
data =[| 10, 56, 12, 7, 39, 22, 33, 59, 21, 6, 30, 55, 27, 3, 41, 44, 57, 4, 28, 26, 60, 49, 15, 2 |
33, 22, 38, 51, 57, 10, 1, 48, 18, 0, 21, 23, 14, 8, 27, 30, 26, 34, 11, 52, 12, 40, 63, 45 |
34, 38, 12, 57, 54, 6, 61, 43, 58, 53, 20, 7, 25, 60, 33, 0, 40, 9, 37, 19, 15, 8, 30, 51 |
24, 46, 15, 16, 58, 0, 7, 53, 42, 54, 21, 5, 38, 13, 45, 55, 29, 22, 56, 50, 11, 59, 34, 17 |
39, 46, 52, 48, 41, 6, 51, 49, 32, 60, 20, 53, 2, 1, 40, 45, 13, 26, 29, 27, 50, 56, 63, 4 |
39, 5, 52, 61, 41, 19, 24, 20, 48, 23, 36, 63, 11, 13, 42, 46, 49, 54, 62, 37, 47, 31, 35, 8 |
61, 44, 43, 42, 29, 16, 37, 4, 25, 62, 32, 9, 5, 36, 10, 24, 3, 31, 14, 28, 47, 35, 17, 18 |
19, 23, 16, 14, 32, 50, 44, 18, 25, 55, 43, 1, 28, 2, 9, 58, 35, 62, 3, 59, 36, 31, 47, 17 |]
;
% cubes: [4, 8, 5, 7, 2, 6, 3, 1]
% symbols: [42, 58, 26, 10, 22, 54, 38, 6, 56, 50, 48, 29, 52, 8, 60, 39, 38, 19, 4, 62, 8, 61, 19, 41]
% rotations: [23, 13, 17, 14, 6, 17, 6, 24]

13
block-party/instances/3345.dzn Normal file
View File

@ -0,0 +1,13 @@
data =[| 56, 29, 24, 47, 38, 15, 50, 10, 63, 30, 40, 41, 39, 62, 2, 33, 34, 36, 54, 5, 25, 7, 55, 48 |
27, 39, 35, 46, 8, 7, 21, 54, 18, 15, 25, 1, 29, 40, 38, 63, 32, 41, 62, 16, 53, 60, 17, 52 |
20, 25, 43, 54, 10, 50, 57, 16, 39, 7, 63, 38, 31, 36, 42, 47, 5, 33, 2, 0, 48, 56, 11, 1 |
21, 17, 41, 11, 58, 46, 9, 47, 51, 29, 60, 33, 26, 37, 1, 31, 23, 4, 10, 6, 12, 8, 28, 45 |
28, 19, 42, 4, 43, 26, 57, 14, 2, 34, 13, 27, 59, 61, 36, 11, 23, 50, 5, 24, 45, 40, 32, 30 |
4, 35, 12, 59, 61, 27, 24, 26, 3, 20, 34, 18, 13, 6, 48, 51, 58, 44, 53, 57, 45, 37, 22, 49 |
52, 8, 56, 9, 13, 22, 16, 43, 23, 6, 18, 19, 55, 62, 49, 35, 3, 42, 14, 12, 37, 53, 44, 0 |
49, 51, 30, 15, 20, 31, 14, 52, 61, 9, 44, 0, 55, 46, 32, 21, 28, 17, 60, 58, 59, 22, 19, 3 |]
;
% cubes: [5, 3, 6, 1, 7, 8, 4, 2]
% symbols: [2, 38, 26, 62, 43, 51, 31, 7, 5, 48, 37, 5, 53, 46, 21, 27, 59, 57, 12, 29, 56, 58, 46, 63]
% rotations: [23, 21, 12, 16, 12, 6, 13, 11]

13
block-party/instances/412.dzn Normal file
View File

@ -0,0 +1,13 @@
data =[| 29, 9, 38, 49, 7, 32, 34, 52, 25, 2, 43, 42, 4, 17, 31, 56, 58, 62, 21, 28, 37, 50, 60, 51 |
47, 10, 39, 28, 31, 17, 61, 23, 29, 13, 1, 50, 49, 9, 37, 2, 16, 20, 26, 33, 4, 34, 46, 44 |
5, 57, 4, 56, 47, 7, 36, 42, 18, 61, 26, 30, 0, 55, 16, 53, 33, 54, 45, 60, 12, 25, 31, 50 |
15, 14, 59, 39, 54, 27, 35, 52, 49, 10, 5, 48, 20, 6, 19, 16, 24, 61, 37, 3, 44, 36, 11, 17 |
62, 0, 2, 18, 45, 33, 41, 52, 48, 5, 40, 21, 14, 46, 27, 26, 56, 59, 28, 12, 55, 11, 53, 42 |
43, 12, 58, 9, 18, 57, 60, 46, 45, 32, 39, 53, 6, 1, 11, 41, 29, 54, 14, 62, 63, 8, 47, 22 |
55, 24, 34, 51, 22, 32, 23, 20, 63, 1, 35, 0, 7, 40, 36, 59, 3, 8, 19, 38, 15, 10, 30, 13 |
30, 3, 22, 51, 23, 15, 27, 41, 19, 13, 44, 63, 35, 8, 58, 6, 25, 21, 38, 40, 48, 57, 24, 43 |]
;
% cubes: [8, 5, 2, 6, 1, 3, 4, 7]
% symbols: [44, 45, 46, 47, 51, 0, 17, 34, 24, 27, 1, 29, 62, 18, 39, 20, 25, 5, 16, 39, 49, 45, 61, 10]
% rotations: [22, 10, 2, 2, 3, 15, 3, 8]

13
block-party/instances/4629.dzn Normal file
View File

@ -0,0 +1,13 @@
data =[| 15, 39, 57, 20, 61, 36, 41, 22, 47, 43, 29, 6, 14, 17, 18, 40, 54, 34, 42, 3, 24, 13, 10, 30 |
15, 45, 20, 19, 47, 57, 7, 46, 59, 14, 56, 17, 11, 34, 37, 62, 55, 54, 61, 16, 9, 31, 51, 2 |
45, 17, 18, 26, 29, 11, 57, 46, 23, 22, 49, 24, 20, 53, 35, 28, 19, 38, 4, 3, 0, 52, 8, 9 |
52, 51, 14, 2, 3, 45, 44, 16, 43, 39, 37, 21, 58, 0, 28, 36, 38, 7, 33, 1, 32, 63, 61, 6 |
60, 36, 24, 15, 48, 23, 47, 9, 0, 10, 32, 28, 41, 46, 2, 33, 35, 25, 12, 55, 4, 44, 40, 29 |
7, 63, 34, 16, 25, 44, 21, 39, 6, 5, 33, 30, 22, 26, 55, 41, 32, 31, 11, 18, 48, 42, 50, 27 |
38, 63, 52, 31, 56, 49, 10, 59, 48, 19, 37, 1, 62, 8, 58, 43, 25, 5, 60, 12, 27, 50, 53, 13 |
35, 4, 60, 13, 49, 8, 59, 21, 56, 62, 30, 1, 5, 23, 54, 40, 58, 50, 42, 53, 27, 26, 51, 12 |]
;
% cubes: [1, 2, 8, 3, 6, 7, 5, 4]
% symbols: [41, 19, 62, 4, 11, 49, 28, 38, 24, 2, 49, 20, 6, 43, 47, 61, 6, 54, 54, 23, 22, 38, 4, 37]
% rotations: [9, 7, 24, 19, 19, 11, 21, 20]

13
block-party/instances/7059.dzn Normal file
View File

@ -0,0 +1,13 @@
data =[| 56, 42, 49, 5, 34, 14, 40, 45, 62, 18, 12, 51, 50, 39, 26, 25, 28, 10, 11, 63, 32, 61, 19, 58 |
17, 51, 3, 7, 25, 46, 29, 41, 57, 48, 53, 20, 56, 15, 22, 12, 60, 38, 33, 34, 27, 14, 55, 40 |
61, 18, 23, 44, 32, 6, 52, 51, 29, 2, 22, 56, 0, 14, 19, 46, 9, 60, 40, 17, 3, 48, 50, 37 |
47, 49, 28, 63, 27, 21, 1, 25, 45, 55, 3, 42, 54, 61, 53, 34, 48, 43, 6, 39, 29, 52, 4, 33 |
50, 13, 38, 7, 15, 36, 21, 10, 42, 12, 23, 16, 55, 27, 45, 60, 35, 53, 44, 26, 46, 22, 0, 52 |
36, 1, 15, 58, 37, 35, 7, 0, 21, 4, 33, 8, 19, 44, 62, 16, 17, 32, 26, 59, 30, 31, 24, 39 |
47, 31, 38, 35, 43, 8, 62, 16, 36, 1, 41, 23, 59, 57, 49, 30, 2, 5, 24, 11, 13, 20, 9, 54 |
57, 18, 20, 5, 28, 4, 13, 63, 30, 43, 2, 24, 8, 10, 59, 37, 41, 11, 9, 6, 47, 58, 31, 54 |]
;
% cubes: [6, 7, 8, 1, 4, 5, 3, 2]
% symbols: [39, 49, 10, 28, 54, 22, 6, 38, 58, 1, 18, 12, 6, 10, 46, 7, 32, 43, 6, 19, 45, 38, 61, 40]
% rotations: [3, 14, 16, 20, 15, 4, 11, 17]

13
block-party/instances/7324.dzn Normal file
View File

@ -0,0 +1,13 @@
data =[| 30, 7, 63, 61, 57, 62, 12, 5, 55, 16, 49, 42, 54, 18, 13, 29, 41, 15, 6, 3, 25, 22, 0, 11 |
29, 59, 53, 45, 57, 43, 8, 36, 22, 3, 35, 50, 41, 9, 27, 37, 10, 61, 26, 60, 42, 16, 48, 39 |
6, 46, 22, 24, 14, 0, 29, 39, 33, 10, 32, 35, 53, 30, 9, 58, 8, 7, 62, 5, 28, 11, 20, 1 |
27, 60, 2, 56, 32, 47, 63, 26, 18, 23, 21, 5, 49, 43, 44, 3, 39, 13, 11, 40, 19, 51, 48, 20 |
60, 61, 37, 19, 47, 27, 24, 28, 0, 25, 43, 36, 53, 45, 33, 31, 10, 63, 35, 12, 51, 58, 23, 52 |
48, 15, 33, 4, 8, 57, 56, 6, 49, 7, 28, 38, 47, 14, 30, 51, 12, 41, 34, 59, 20, 37, 50, 17 |
59, 32, 62, 31, 42, 16, 58, 4, 54, 40, 36, 17, 45, 19, 44, 14, 1, 2, 38, 34, 46, 55, 21, 52 |
40, 54, 21, 13, 17, 1, 23, 44, 2, 46, 38, 24, 50, 26, 31, 18, 15, 4, 25, 56, 55, 34, 52, 9 |]
;
% cubes: [1, 5, 3, 8, 4, 7, 2, 6]
% symbols: [29, 35, 58, 4, 21, 16, 27, 30, 30, 0, 0, 9, 39, 14, 57, 7, 62, 53, 6, 13, 48, 59, 3, 8]
% rotations: [13, 19, 13, 17, 22, 11, 14, 14]

13
block-party/instances/7326.dzn Normal file
View File

@ -0,0 +1,13 @@
data =[| 16, 63, 9, 37, 29, 30, 31, 55, 25, 23, 60, 53, 26, 46, 13, 50, 15, 47, 28, 6, 49, 11, 48, 38 |
44, 47, 27, 12, 41, 40, 50, 54, 43, 37, 2, 9, 51, 20, 26, 11, 17, 63, 23, 45, 34, 31, 62, 29 |
51, 14, 11, 49, 61, 34, 24, 17, 47, 46, 38, 1, 2, 31, 32, 19, 39, 54, 37, 48, 40, 35, 10, 44 |
48, 42, 15, 14, 5, 12, 50, 58, 56, 34, 3, 53, 20, 17, 40, 2, 30, 1, 45, 24, 62, 36, 63, 61 |
58, 55, 49, 42, 62, 33, 5, 25, 20, 13, 44, 28, 59, 43, 21, 45, 52, 30, 29, 38, 23, 14, 1, 35 |
60, 16, 58, 36, 57, 27, 43, 12, 46, 9, 54, 3, 0, 22, 41, 8, 7, 10, 53, 21, 4, 32, 61, 18 |
3, 18, 32, 10, 52, 22, 8, 39, 4, 28, 42, 60, 57, 5, 56, 0, 55, 6, 24, 59, 33, 19, 7, 51 |
0, 52, 22, 4, 56, 19, 27, 33, 13, 16, 57, 36, 41, 15, 7, 8, 21, 25, 39, 35, 18, 6, 26, 59 |]
;
% cubes: [1, 2, 4, 8, 3, 7, 5, 6]
% symbols: [28, 45, 62, 15, 31, 51, 43, 7, 26, 20, 50, 35, 14, 10, 38, 61, 25, 47, 53, 52, 48, 6, 55, 54]
% rotations: [19, 18, 1, 16, 16, 3, 16, 20]

13
block-party/instances/7444.dzn Normal file
View File

@ -0,0 +1,13 @@
data =[| 6, 36, 47, 53, 3, 41, 1, 13, 34, 18, 60, 23, 63, 5, 37, 52, 50, 57, 19, 22, 46, 17, 24, 11 |
27, 34, 36, 30, 55, 58, 52, 32, 5, 57, 60, 33, 41, 42, 35, 8, 40, 9, 37, 2, 50, 39, 24, 28 |
24, 6, 2, 28, 47, 37, 12, 44, 58, 36, 43, 32, 38, 61, 48, 49, 57, 40, 3, 23, 42, 50, 62, 1 |
7, 59, 0, 45, 60, 22, 10, 25, 15, 38, 42, 54, 14, 51, 43, 2, 12, 4, 23, 48, 41, 21, 30, 6 |
1, 63, 21, 18, 8, 48, 29, 56, 15, 35, 12, 43, 58, 19, 10, 33, 49, 14, 9, 4, 53, 39, 13, 47 |
18, 53, 38, 46, 27, 34, 20, 16, 56, 32, 51, 55, 22, 19, 40, 28, 54, 62, 7, 9, 59, 5, 26, 31 |
54, 21, 20, 45, 33, 7, 35, 49, 56, 16, 17, 10, 0, 8, 14, 63, 25, 26, 44, 31, 29, 61, 11, 13 |
44, 20, 30, 27, 4, 11, 59, 25, 16, 39, 51, 15, 45, 3, 52, 46, 26, 31, 55, 61, 17, 62, 0, 29 |]
;
% cubes: [7, 8, 5, 3, 4, 1, 6, 2]
% symbols: [13, 4, 10, 3, 43, 46, 32, 37, 45, 52, 35, 38, 38, 23, 40, 5, 26, 39, 8, 58, 60, 1, 27, 41]
% rotations: [3, 10, 14, 19, 14, 1, 24, 19]

13
block-party/instances/7661.dzn Normal file
View File

@ -0,0 +1,13 @@
data =[| 62, 40, 20, 61, 42, 52, 5, 25, 37, 14, 11, 46, 36, 0, 29, 41, 32, 44, 55, 19, 39, 45, 34, 60 |
20, 38, 14, 5, 61, 45, 18, 39, 34, 50, 1, 44, 35, 31, 27, 17, 47, 15, 0, 37, 63, 22, 55, 26 |
27, 51, 36, 47, 21, 6, 10, 17, 43, 34, 16, 52, 12, 44, 11, 46, 42, 57, 40, 32, 2, 59, 50, 25 |
6, 24, 8, 31, 40, 39, 59, 16, 41, 33, 45, 15, 48, 56, 20, 38, 60, 29, 14, 55, 1, 35, 51, 22 |
3, 63, 25, 60, 26, 57, 58, 6, 12, 21, 47, 4, 1, 33, 30, 56, 23, 54, 31, 19, 18, 52, 13, 37 |
7, 16, 4, 5, 59, 2, 12, 3, 28, 11, 58, 22, 36, 15, 13, 43, 56, 42, 21, 29, 9, 49, 53, 26 |
13, 3, 18, 17, 50, 43, 10, 57, 9, 46, 2, 61, 28, 53, 32, 24, 49, 30, 23, 62, 48, 7, 54, 8 |
10, 27, 23, 38, 28, 41, 30, 51, 35, 0, 48, 62, 7, 49, 19, 4, 58, 9, 24, 54, 33, 53, 63, 8 |]
;
% cubes: [5, 8, 6, 3, 1, 7, 2, 4]
% symbols: [60, 19, 5, 42, 32, 46, 39, 41, 54, 0, 26, 16, 34, 32, 14, 48, 37, 28, 42, 50, 11, 50, 22, 14]
% rotations: [7, 14, 7, 20, 20, 24, 12, 23]

13
block-party/instances/7750.dzn Normal file
View File

@ -0,0 +1,13 @@
data =[| 30, 23, 35, 29, 62, 37, 52, 40, 10, 18, 43, 17, 41, 7, 48, 54, 46, 16, 56, 33, 27, 0, 15, 59 |
37, 53, 47, 32, 57, 16, 48, 30, 62, 58, 10, 55, 7, 14, 13, 36, 34, 60, 43, 49, 19, 29, 1, 56 |
61, 53, 10, 11, 50, 41, 51, 4, 5, 28, 20, 18, 33, 40, 6, 16, 12, 56, 3, 8, 49, 14, 22, 15 |
25, 29, 19, 4, 63, 30, 50, 47, 2, 53, 38, 51, 62, 60, 55, 39, 34, 12, 3, 15, 61, 24, 46, 42 |
13, 50, 46, 38, 24, 8, 52, 31, 6, 41, 33, 3, 54, 59, 21, 28, 40, 37, 25, 36, 17, 9, 44, 42 |
14, 60, 9, 58, 20, 1, 43, 38, 31, 57, 61, 6, 22, 11, 36, 63, 39, 24, 42, 34, 21, 49, 26, 45 |
35, 47, 45, 11, 22, 7, 13, 28, 51, 0, 20, 27, 19, 63, 5, 44, 52, 25, 8, 31, 23, 2, 26, 32 |
4, 32, 12, 57, 54, 23, 18, 2, 21, 5, 0, 44, 17, 9, 45, 55, 58, 1, 35, 39, 59, 26, 48, 27 |]
;
% cubes: [6, 5, 7, 3, 8, 1, 2, 4]
% symbols: [14, 24, 35, 53, 55, 48, 57, 62, 1, 21, 44, 40, 23, 62, 58, 3, 63, 41, 7, 8, 4, 18, 13, 2]
% rotations: [5, 10, 5, 6, 13, 14, 10, 15]

13
block-party/instances/8848.dzn Normal file
View File

@ -0,0 +1,13 @@
data =[| 32, 4, 28, 47, 2, 54, 21, 0, 6, 40, 17, 42, 26, 50, 23, 44, 46, 55, 19, 63, 12, 41, 29, 20 |
7, 44, 29, 3, 9, 35, 36, 30, 27, 37, 10, 39, 19, 11, 51, 0, 34, 18, 28, 32, 46, 1, 21, 8 |
52, 47, 48, 33, 58, 4, 8, 3, 5, 16, 13, 36, 38, 42, 49, 18, 29, 41, 7, 21, 53, 6, 62, 24 |
17, 54, 34, 24, 1, 26, 9, 7, 47, 57, 39, 50, 43, 22, 13, 15, 45, 27, 41, 30, 48, 35, 23, 20 |
5, 23, 48, 50, 13, 10, 45, 16, 40, 2, 18, 9, 58, 11, 32, 43, 28, 51, 22, 3, 0, 57, 20, 59 |
31, 43, 60, 52, 24, 25, 37, 49, 35, 51, 15, 62, 1, 63, 54, 6, 8, 27, 58, 39, 14, 61, 33, 56 |
5, 17, 25, 12, 57, 63, 62, 46, 31, 33, 45, 60, 30, 19, 53, 34, 4, 56, 61, 40, 38, 59, 55, 14 |
12, 38, 10, 56, 61, 44, 22, 60, 49, 26, 52, 36, 2, 16, 53, 15, 31, 42, 37, 55, 11, 25, 59, 14 |]
;
% cubes: [1, 8, 3, 6, 5, 2, 7, 4]
% symbols: [47, 36, 42, 33, 3, 34, 17, 48, 55, 11, 47, 8, 11, 10, 19, 9, 20, 22, 21, 15, 23, 21, 40, 50]
% rotations: [7, 21, 16, 2, 18, 20, 6, 1]

159
block-party/instances/block-party-generate.mzn Normal file
View File

@ -0,0 +1,159 @@
/*
* author: Jean-Noël Monette
*/
include "globals.mzn";
set of int: cubes=1..8;
set of int: pos=1..24;
set of int: symbols=0..4*4*4-1;
set of int: places=1..8*24;
set of int: faces= 1..6;
array[faces] of set of pos: face = [{1,2,3,4},{5,6,7,8},{9,10,11,12},{13,14,15,16},{17,18,19,20},{21,22,23,24}];
set of int: chars = 0..3;
array[cubes,pos] of var symbols: data;
constraint global_cardinality_closed(array1d(data),symbols,[3|i in symbols])::domain;
constraint forall(c in 7..8)(all_different([data[c,i]|i in pos])::domain);
%redundant constraint for the previous ones
array[cubes,symbols] of var 0..1: cnt;
constraint forall(c in 1..8)(global_cardinality_closed([data[c,i]|i in pos],symbols,[cnt[c,i]|i in symbols])::domain);
constraint forall(s in symbols)(sum(c in cubes)(cnt[c,s])=3);
constraint forall(c in cubes, f in faces)(
global_cardinality_low_up_closed([color(data[c,p])|p in face[f]],chars,[0|i in chars],[3|i in chars])::domain
/\
global_cardinality_low_up_closed([fill(data[c,p])|p in face[f]],chars,[0|i in chars],[3|i in chars])::domain
/\
global_cardinality_low_up_closed([shape(data[c,p])|p in face[f]],chars,[0|i in chars],[3|i in chars])::domain
);
%I believe this set of constraints is redundant with the previous one
constraint forall(c in cubes, f in faces)(
nvalue([color(data[c,p])|p in face[f]]) >= 2
/\
nvalue([fill(data[c,p])|p in face[f]]) >= 2
/\
nvalue([shape(data[c,p])|p in face[f]]) >= 2
);
solve
::seq_search([
int_search(cube_at,input_order,indomain_random,complete),
int_search(symbol_at,input_order,indomain_random,complete),
int_search(rotation,input_order,indomain_random,complete),
int_search(array1d(data),input_order,indomain_random,complete),
])
satisfy;
output ["data =",show2d(data),";\n","% cubes: ",show(cube_at),"\n% symbols: ",show(symbol_at),"\n% rotations: ",show(rotation)];
%How to implement linking functions with the advantages of CSE.
function array[1..3] of var 0..3: fcs(var 0..63:symbol) :: promise_total =
let { var 0..3: color; var 0..3:shape;var 0..3: fill;
constraint symbol = 4*4*fill+4*color+shape; }
in [fill,color,shape];
function var 0..3: color_help(array[1..3] of var 0..3: fcs) :: promise_total = fcs[2];
function var 0..3: color(var int:symbol) ::promise_total = color_help(fcs(symbol));
function var 0..3: fill_help(array[1..3] of var 0..3: fcs) :: promise_total = fcs[1];
function var 0..3: fill(var int:symbol) ::promise_total = fill_help(fcs(symbol));
function var 0..3: shape_help(array[1..3] of var 0..3: fcs) :: promise_total = fcs[3];
function var 0..3: shape(var int:symbol) ::promise_total = shape_help(fcs(symbol));
int: ud=0;
int: lr=8;
int: fb=16;
array[cubes] of var cubes: cube_at;
array[pos] of var symbols: symbol_at;
array[cubes] of var 1..24: rotation;
%Each cube is placed once.
constraint alldifferent(cube_at);
%Party constraints on the 6 faces
constraint party([symbol_at[i] | i in 1..4]);
constraint party([symbol_at[i + 4] | i in 1..4]);
constraint party([symbol_at[(i - 1) * 2 + 1 + lr] | i in 1..4]);
constraint party([symbol_at[i * 2 + lr] | i in 1..4]);
constraint party([symbol_at[if i < 3 then i else i+2 endif + fb] | i in 1..4]);
constraint party([symbol_at[if i < 3 then i else i+2 endif + 2 + fb] | i in 1..4]);
%Linking cubes and symbols
constraint forall(i in {1,4,6,7})(
link_cube_and_symbols(cube_at[i],[symbol_at[i+ud],symbol_at[i+lr],symbol_at[i+fb]],rotation[i],data));
constraint forall(i in {2,3,5,8})(
link_cube_and_symbols(cube_at[i],[symbol_at[i+ud],symbol_at[i+fb],symbol_at[i+lr]],rotation[i],data));
%Note: this presolve does not change much
predicate diff_or_equal(array[1..4] of var 0..3: x) =
forall(i in 1..4,j in i+1..4)(x[i]!=x[j])
\/
forall(i in 1..4,j in i+1..4)(x[i]=x[j]);
% A party is alldiff or allequal for each of the three characteristics.
% Note: I never tried to (manually) presolve this one but it might be worth trying it as well...
predicate party(array[1..4] of var 0..63: symbols) = (
diff_or_equal([color(symbols[i]) | i in 1..4])
/\ diff_or_equal([shape(symbols[i]) | i in 1..4])
/\ diff_or_equal([fill(symbols[i]) | i in 1..4]) );
%Linking cube IDs with the three symbols appearing in relevant positions
predicate link_cube_and_symbols(var int: cube, array[1..3] of var int: symbols,var 1..24: pos,array[cubes,pos] of var symbols:data) =
forall(i in 1..3)(data[cube,pp[pos,i]]=symbols[i]);
%Which symbol positions on a cube are next to each other on the same corner.
%Made by hand, I do not think there is any hope for finding a simple formula that could be used in precomputation :-)
%Actually it might be divided by three and have a disjunction in link_cube_and_symbols
array[1..24,1..3] of int: pp = [|21,12,7
|23,17,11
|24,4,18
|22,8,3
|1,6,16
|2,14,20
|4,18,24
|3,22,8
|7,21,12
|5,10,15
|6,16,1
|8,3,22
|16,1,6
|15,5,10
|13,9,19
|14,20,2
|18,24,4
|20,2,14
|19,13,9
|17,11,23
|12,7,21
|11,23,17
|9,19,13
|10,15,5
|];

289
handball/handball7.mzn Normal file
View File

@ -0,0 +1,289 @@
% Elitserien handboll -- generic model, needs specific:
% - sets of teams for N and S divisions
% - which teams to form complementary divisions
% - derby sets
% - venue unavailabilities
%
% Jeff Larson <jeffreyl@kth.se>
% Mats Carlsson <matsc@sics.se>
% * 14-team league
% * Form 2 divisions which hold a single round-robin tournament
% 1. Each 7-team division must hold a SRRT to start the season.
% 2. This must be followed by two SRRTs between the entire league, the
% second SRRT being a mirror of the first.
% 3. There must be a minimum number of breaks in the schedule
% (home-home pair or away-away pair).
% 4. Each team has one bye during the season (to occur during the
% divisional RRT).
% 5. At no point during the season can the number of home and away
% games played by a team differ by more than 1.
% 6. Any pair of teams must have consecutive meetings occur at different
% venues. (AVR)
include "globals.mzn";
%% version codes
bool: dopresolve = true;
%% HAP patterns
int: A = 1; % away
int: B = 2; % bye
int: H = 3; % home
int: divsize = 7;
set of int: north_team = 1..7;
set of int: south_team = 8..14;
set of int: team = 1..14;
set of int: first_tour = 1..7;
set of int: second_tour = 8..20;
set of int: third_tour = 21..33;
set of int: period = 1..20;
set of int: allperiod = 1..33;
set of int: breakable = {0,9,11,13,15,17,19};
array[period,team] of var A..H: hap;
array[period,team] of var team: contestant;
array[team] of var breakable: break;
var int: cost;
array[team] of var team: rowof; % rowof[i]=j means TEAMi gets row j of template
array[team] of var team: teamof;% the inverse of rowof
%% venue unavailability
array[team,allperiod] of 0..1: nohome;
%% division assignment
set of int: group1;
set of int: group2;
%% derby constraints
array[int] of set of int: derby_set; % unused
array[int] of period: derby_period; % unused
%% complementary schedules
array[int] of set of int: cpairs; % unused
%% cost table
array[int,int] of int: costtable; % unused
%% search heuristic
array[team] of team: heur; % unused
%% DFA states
int: INIT = 1;
int: B_1 = 2;
int: A_1 = 3;
int: H_1 = 4;
int: A_2 = 5;
int: H_2 = 6;
int: AB_2 = 7;
int: HB_2 = 8;
int: A_3 = 9;
int: H_3 = 10;
int: AB_3 = 11;
int: HB_3 = 12;
int: A_4 = 13;
int: H_4 = 14;
int: AB_4 = 15;
int: HB_4 = 16;
int: A_5 = 17;
int: H_5 = 18;
int: AB_5 = 19;
int: HB_5 = 20;
int: A_6 = 21;
int: H_6 = 22;
int: AB_6 = 23;
int: HB_6 = 24;
int: AB_7 = 25;
int: HB_7 = 26;
int: AB_8 = 27;
int: HB_8 = 28;
int: AB_9 = 29;
int: HB_9 = 30;
int: AB_20 = 31;
int: HB_20 = 32;
array[int,int] of int: transition =
[| A_1, B_1, H_1 % INIT, start state
| AB_2, 0, HB_2 % B_1
| 0, AB_2, H_2 % A_1
| A_2, HB_2, 0 % H_1
| 0, AB_3, H_3 % A_2
| A_3, HB_3, 0 % H_2
| 0, 0, HB_3 % AB_2
| AB_3, 0, 0 % HB_2
| 0, AB_4, H_4 % A_3
| A_4, HB_4, 0 % H_3
| 0, 0, HB_4 % AB_3
| AB_4, 0, 0 % HB_3
| 0, AB_5, H_5 % A_4
| A_5, HB_5, 0 % H_4
| 0, 0, HB_5 % AB_4
| AB_5, 0, 0 % HB_4
| 0, AB_6, H_6 % A_5
| A_6, HB_6, 0 % H_5
| 0, 0, HB_6 % AB_5
| AB_6, 0, 0 % HB_5
| 0, AB_7, 0 % A_6
| 0, HB_7, 0 % H_6
| 0, 0, HB_7 % AB_6
| AB_7, 0, 0 % HB_6
| 0, 0, HB_8 % AB_7
| AB_8, 0, 0 % HB_7
| 0, 0, HB_9 % AB_8, accept state
| AB_9, 0, 0 % HB_8, accept state
|AB_20, 0, HB_8 % AB_9
| AB_8, 0, HB_20 % HB_9
| 0, 0, HB_20 % AB_20, accept state
|AB_20, 0, 0 % HB_20, accept state
|];
% cost function
predicate part_cost(var breakable: bt, var team: r, var team: t, var 0..max(allperiod): part) ::presolve = (
if dopresolve then
bt in breakable /\
let {array[period] of var A..H: lhap} in (
channel_break_hap(bt, lhap, r) /\
part = sum(p in period where nohome[t,p]=1)(bool2int(lhap[p] =H)) +
sum(p in third_tour where nohome[t,p]=1)(bool2int(lhap[min(third_tour)+max(period)-p]=A))
)
else
part = sum(p in period where nohome[t,p]=1)(bool2int(hap[p,r] =H)) +
sum(p in third_tour where nohome[t,p]=1)(bool2int(hap[min(third_tour)+max(period)-p,r]=A))
endif
);
constraint
if not dopresolve then
cost = sum(t in team, p in period where nohome[t,p]=1)(bool2int(hap[p,rowof[t]]=H))
+ sum(t in team, p in third_tour where nohome[t,p]=1)(bool2int(hap[min(third_tour)+max(period)-p,rowof[t]]=A))
else
let {array[team] of var 0..max(allperiod): rowcost} in (
forall(t in team)(part_cost(break[t], t, teamof[t], rowcost[t])) /\
cost = sum(t in team)(rowcost[t])
)
endif;
% division assignment
constraint
let {var bool: NS} in (
forall(t in group1)(NS <-> rowof[t] in north_team) /\
forall(t in group2)(NS <-> rowof[t] in south_team)
);
constraint
inverse(rowof,teamof) :: domain;
%% STRUCTURAL CONSTAINTS
% first round robin tournament (domains)
constraint
forall(p in first_tour, t in north_team)(
contestant[p,t] in north_team
) /\
forall(p in first_tour, t in south_team)(
contestant[p,t] in south_team
);
% channel break <---> hap (2)
predicate channel_break_hap(var breakable: bt, array[period] of var A..H: hapt, var team: t) ::presolve(model) =
bt in breakable /\
(t in north_team -> hapt[(t mod divsize)+1] = A) /\
(t in south_team -> hapt[(t mod divsize)+1] = H) /\
hapt[((t-1) mod divsize)+1] = B /\
forall(p in breakable diff {0})(
bt = p <-> hapt[p]=hapt[p+1]
) /\
regular([hapt[p] | p in period],
HB_20, % last state
H, % last symbol
transition,
INIT, % start state
{AB_8,HB_8,AB_20,HB_20} % accept states
);
constraint
forall(t in team)(
channel_break_hap(break[t], [hap[p,t] | p in period], t)
);
% RRT (5)
constraint
forall(p in period)(
inverse([contestant[p,t] | t in team],[contestant[p,t] | t in team]) :: domain
);
% RRT (6)
constraint
forall(t in team)(
alldifferent([contestant[p,t] | p in first_tour]) :: domain /\
alldifferent([contestant[p,t] | p in second_tour]) :: domain
);
% either we at home and contestant away (7)
% or we away and contestant at home
% or bye (we = contestant)
constraint
forall(p in period, t in team)(
let {var team: ctw = contestant[p,t]} in (
hap[p,ctw] + hap[p,t] = A+H
)
);
% AVR rule (1) (8)
constraint
forall(t in team)(
alldifferent([3*contestant[p,t]+hap[p,t] | p in period]) :: domain
);
%% IMPLIED CONSTRAINTS
% channel contestant <---> hap (3)
constraint
forall(t in team, p in period)(
contestant[p,t]=t <-> hap[p,t]=B
);
% exactly two occurrences of every break period (12)
constraint
global_cardinality_closed(break, [i | i in breakable], [2 | i in breakable]) :: domain;
%% SYMMETRY-BREAKING CONSTAINTS
% 1st row and 1st column complementary for each division (18)
constraint
forall(t in north_team)(
hap[t,1] + hap[1,t] = A+H /\
hap[t,1+divsize] + hap[1,t+divsize] = A+H
);
%% SOLVING AND OUTPUTTING
solve :: seq_search(
[int_search([hap[p,t] | p in period, t in team], input_order, indomain_min, complete),
int_search(rowof, input_order, indomain_min, complete),
int_search([contestant[p,t] | t in team, p in period], input_order, indomain_min, complete)
]
) minimize(cost);
output [show(cost)];

311
handball/handball9.mzn Normal file
View File

@ -0,0 +1,311 @@
% Elitserien handboll -- generic model, needs specific:
% - sets of teams for N and S divisions
% - which teams to form complementary divisions
% - derby sets
% - venue unavailabilities
%
% Jeff Larson <jeffreyl@kth.se>
% Mats Carlsson <matsc@sics.se>
% * 18-team league
% * Form 2 divisions which hold a single round-robin tournament
% 1. Each 9-team division must hold a SRRT to start the season.
% 2. This must be followed by two SRRTs between the entire league, the
% second SRRT being a mirror of the first.
% 3. There must be a minimum number of breaks in the schedule
% (home-home pair or away-away pair).
% 4. Each team has one bye during the season (to occur during the
% divisional RRT).
% 5. At no point during the season can the number of home and away
% games played by a team differ by more than 1.
% 6. Any pair of teams must have consecutive meetings occur at different
% venues. (AVR)
include "globals.mzn";
%% version codes
bool: dopresolve;
%% HAP patterns
int: A = 1; % away
int: B = 2; % bye
int: H = 3; % home
int: divsize = 9;
set of int: north_team = 1..9;
set of int: south_team = 10..18;
set of int: team = 1..18;
set of int: first_tour = 1..9;
set of int: second_tour = 10..26;
set of int: third_tour = 27..43;
set of int: period = 1..26;
set of int: allperiod = 1..43;
set of int: breakable = {0,11,13,15,17,19,21,23,25};
array[period,team] of var A..H: hap;
array[period,team] of var team: contestant;
array[team] of var breakable: break;
var int: cost;
array[team] of var team: rowof; % rowof[i]=j means TEAMi gets row j of template
array[team] of var team: teamof;% the inverse of rowof
%% venue unavailability
array[team,allperiod] of 0..1: nohome;
%% division assignment
set of int: group1;
set of int: group2;
%% derby constraints
array[int] of set of int: derby_set; % unused
array[int] of period: derby_period; % unused
%% complementary schedules
array[int] of set of int: cpairs; % unused
%% cost table
array[int,int] of int: costtable; % unused
%% search heuristic
array[team] of team: heur; % unused
%% DFA states
int: INIT = 1;
int: B_1 = 2;
int: A_1 = 3;
int: H_1 = 4;
int: A_2 = 5;
int: H_2 = 6;
int: AB_2 = 7;
int: HB_2 = 8;
int: A_3 = 9;
int: H_3 = 10;
int: AB_3 = 11;
int: HB_3 = 12;
int: A_4 = 13;
int: H_4 = 14;
int: AB_4 = 15;
int: HB_4 = 16;
int: A_5 = 17;
int: H_5 = 18;
int: AB_5 = 19;
int: HB_5 = 20;
int: A_6 = 21;
int: H_6 = 22;
int: AB_6 = 23;
int: HB_6 = 24;
int: A_7 = 25;
int: H_7 = 26;
int: AB_7 = 27;
int: HB_7 = 28;
int: A_8 = 29;
int: H_8 = 30;
int: AB_8 = 31;
int: HB_8 = 32;
int: AB_9 = 33;
int: HB_9 = 34;
int: AB_10 = 35;
int: HB_10 = 36;
int: AB_11 = 37;
int: HB_11 = 38;
int: AB_20 = 39;
int: HB_20 = 40;
array[int,int] of int: transition =
[| A_1, B_1, H_1 % INIT, start state
| AB_2, 0, HB_2 % B_1
| 0, AB_2, H_2 % A_1
| A_2, HB_2, 0 % H_1
| 0, AB_3, H_3 % A_2
| A_3, HB_3, 0 % H_2
| 0, 0, HB_3 % AB_2
| AB_3, 0, 0 % HB_2
| 0, AB_4, H_4 % A_3
| A_4, HB_4, 0 % H_3
| 0, 0, HB_4 % AB_3
| AB_4, 0, 0 % HB_3
| 0, AB_5, H_5 % A_4
| A_5, HB_5, 0 % H_4
| 0, 0, HB_5 % AB_4
| AB_5, 0, 0 % HB_4
| 0, AB_6, H_6 % A_5
| A_6, HB_6, 0 % H_5
| 0, 0, HB_6 % AB_5
| AB_6, 0, 0 % HB_5
| 0, AB_7, H_7 % A_6
| A_7, HB_7, 0 % H_6
| 0, 0, HB_7 % AB_6
| AB_7, 0, 0 % HB_6
| 0, AB_8, H_8 % A_7
| A_8, HB_8, 0 % H_7
| 0, 0, HB_8 % AB_7
| AB_8, 0, 0 % HB_7
| 0, AB_9, 0 % A_8
| 0, HB_9, 0 % H_8
| 0, 0, HB_9 % AB_8
| AB_9, 0, 0 % HB_8
| 0, 0, HB_10 % AB_9
|AB_10, 0, 0 % HB_9
| 0, 0, HB_11 % AB_10, accept state
| AB_11, 0, 0 % HB_10, accept state
|AB_20, 0, HB_10 % AB_11
|AB_10, 0, HB_20 % HB_11
| 0, 0, HB_20 % AB_20, accept state
|AB_20, 0, 0 % HB_20, accept state
|];
% cost function
predicate part_cost(var breakable: bt, var team: r, var team: t, var 0..max(allperiod): part) ::presolve = (
if dopresolve then
bt in breakable /\
let {array[period] of var A..H: lhap} in (
channel_break_hap(bt, lhap, r) /\
part = sum(p in period where nohome[t,p]=1)(bool2int(lhap[p] =H)) +
sum(p in third_tour where nohome[t,p]=1)(bool2int(lhap[min(third_tour)+max(period)-p]=A))
)
else
part = sum(p in period where nohome[t,p]=1)(bool2int(hap[p,r] =H)) +
sum(p in third_tour where nohome[t,p]=1)(bool2int(hap[min(third_tour)+max(period)-p,r]=A))
endif
);
constraint
if not dopresolve then
cost = sum(t in team, p in period where nohome[t,p]=1)(bool2int(hap[p,rowof[t]]=H))
+ sum(t in team, p in third_tour where nohome[t,p]=1)(bool2int(hap[min(third_tour)+max(period)-p,rowof[t]]=A))
else
let {array[team] of var 0..max(allperiod): rowcost} in (
forall(t in team)(part_cost(break[t], t, teamof[t], rowcost[t])) /\
cost = sum(t in team)(rowcost[t])
)
endif;
% division assignment
constraint
let {var bool: NS} in (
forall(t in group1)(NS <-> rowof[t] in north_team) /\
forall(t in group2)(NS <-> rowof[t] in south_team)
);
constraint
inverse(rowof,teamof) :: domain;
%% STRUCTURAL CONSTAINTS
% first round robin tournament (domains)
constraint
forall(p in first_tour, t in north_team)(
contestant[p,t] in north_team
) /\
forall(p in first_tour, t in south_team)(
contestant[p,t] in south_team
);
% channel break <---> hap (2)
predicate channel_break_hap(var breakable: bt, array[period] of var A..H: hapt, var team: t) ::presolve(model) =
bt in breakable /\
(t in north_team -> hapt[(t mod divsize)+1] = A) /\
(t in south_team -> hapt[(t mod divsize)+1] = H) /\
hapt[((t-1) mod divsize)+1] = B /\
forall(p in breakable diff {0})(
bt = p <-> hapt[p]=hapt[p+1]
) /\
regular([hapt[p] | p in period],
HB_20, % last state
H, % last symbol
transition,
INIT, % start state
{AB_10,HB_10,AB_20,HB_20} % accept states
);
constraint
forall(t in team)(
channel_break_hap(break[t], [hap[p,t] | p in period], t)
);
% RRT (5)
constraint
forall(p in period)(
inverse([contestant[p,t] | t in team],[contestant[p,t] | t in team]) :: domain
);
% RRT (6)
constraint
forall(t in team)(
alldifferent([contestant[p,t] | p in first_tour]) :: domain /\
alldifferent([contestant[p,t] | p in second_tour]) :: domain
);
% either we at home and contestant away (7)
% or we away and contestant at home
% or bye (we = contestant)
constraint
forall(p in period, t in team)(
let {var team: ctw = contestant[p,t]} in (
hap[p,ctw] + hap[p,t] = A+H
)
);
% AVR rule (1) (8)
constraint
forall(t in team)(
alldifferent([3*contestant[p,t]+hap[p,t] | p in period]) :: domain
);
%% IMPLIED CONSTRAINTS
% channel contestant <---> hap (3)
constraint
forall(t in team, p in period)(
contestant[p,t]=t <-> hap[p,t]=B
);
% exactly two occurrences of every break period (12)
constraint
global_cardinality_closed(break, [i | i in breakable], [2 | i in breakable]) :: domain;
%% SYMMETRY-BREAKING CONSTAINTS
% 1st row and 1st column complementary for each division (18)
constraint
forall(t in north_team)(
hap[t,1] + hap[1,t] = A+H /\
hap[t,1+divsize] + hap[1,t+divsize] = A+H
);
%% SOLVING AND OUTPUTTING
solve :: seq_search(
[int_search([hap[p,t] | p in period, t in team], input_order, indomain_min, complete),
int_search(rowof, input_order, indomain_min, complete),
int_search([contestant[p,t] | t in team, p in period], input_order, indomain_min, complete)
]
) minimize(cost);
output [show(cost)];

1401
handball/instances7/1.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/10.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/11.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/12.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/13.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/14.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/15.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/16.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/17.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/18.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/19.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/2.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/20.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/3.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/4.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/5.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/6.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/7.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/8.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1401
handball/instances7/9.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/1.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/10.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/11.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/12.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/13.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/14.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/15.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/16.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/17.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/18.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/19.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/2.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/20.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/3.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/4.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/5.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/6.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/7.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/8.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

2949
handball/instances9/9.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

167
jp-encoding/instances/data100.dzn Normal file
View File

@ -0,0 +1,167 @@
len = 164;
stream = [
227,
129,
157,
227,
129,
147,
227,
129,
167,
230,
180,
155,
228,
184,
173,
227,
129,
174,
227,
129,
149,
227,
129,
179,
227,
130,
140,
230,
150,
185,
227,
129,
175,
228,
184,
128,
233,
128,
154,
227,
130,
138,
227,
129,
167,
227,
129,
175,
227,
129,
170,
227,
129,
132,
227,
128,
130,
10,
227,
129,
130,
227,
130,
139,
230,
151,
165,
227,
129,
174,
230,
154,
174,
230,
150,
185,
227,
129,
174,
228,
186,
139,
227,
129,
167,
227,
129,
130,
227,
130,
139,
227,
128,
130,
228,
184,
128,
228,
186,
186,
227,
129,
174,
228,
184,
139,
228,
186,
186,
227,
129,
140,
227,
128,
129,
231,
190,
133,
231,
148,
159,
233,
150,
128,
227,
129,
174,
228,
184,
139,
227,
129,
167,
233,
155,
168,
227,
130,
132,
227,
129,
191,
227,
130,
146,
229,
190,
133,
227,
129,
163,
227,
129,
166,
227,
129,
132,
227,
129,
159,
227,
128,
130,
10
];

1018
jp-encoding/instances/data1000.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

1773
jp-encoding/instances/data1700.dzn Normal file
View File

File diff suppressed because it is too large Load Diff

602
jp-encoding/instances/data400.dzn Normal file
View File

@ -0,0 +1,602 @@
len = 599;
stream = [
202,
204,
195,
202,
191,
188,
164,
164,
205,
253,
205,
179,
164,
199,
164,
226,
164,
202,
164,
164,
161,
163,
10,
144,
86,
146,
122,
130,
204,
147,
241,
138,
75,
130,
169,
130,
231,
142,
241,
130,
240,
143,
111,
130,
181,
130,
196,
130,
162,
130,
189,
130,
231,
129,
65,
147,
175,
139,
137,
144,
182,
130,
204,
136,
234,
144,
108,
130,
170,
143,
231,
146,
107,
130,
201,
129,
65,
130,
162,
130,
173,
130,
231,
136,
208,
146,
163,
130,
193,
130,
196,
130,
224,
129,
65,
130,
187,
130,
177,
130,
169,
130,
231,
148,
242,
130,
209,
141,
126,
130,
232,
130,
233,
142,
150,
130,
205,
143,
111,
151,
136,
130,
220,
130,
162,
129,
66,
10,
188,
229,
195,
238,
164,
228,
161,
188,
164,
164,
161,
163,
164,
200,
211,
242,
164,
183,
164,
191,
164,
171,
164,
233,
164,
199,
164,
162,
164,
235,
161,
163,
190,
174,
187,
200,
164,
203,
201,
233,
164,
214,
164,
181,
164,
195,
164,
198,
181,
162,
164,
195,
164,
198,
205,
232,
164,
191,
187,
254,
161,
162,
164,
170,
164,
228,
164,
184,
164,
172,
194,
231,
164,
173,
164,
202,
180,
227,
164,
242,
164,
183,
164,
198,
198,
243,
179,
172,
164,
176,
164,
233,
164,
164,
164,
171,
164,
233,
200,
244,
164,
211,
185,
223,
164,
234,
164,
198,
185,
248,
164,
242,
200,
180,
164,
171,
164,
185,
197,
219,
164,
172,
164,
162,
164,
235,
164,
171,
164,
200,
177,
190,
164,
195,
164,
191,
164,
171,
164,
233,
161,
162,
164,
179,
164,
206,
188,
161,
164,
207,
200,
180,
164,
171,
164,
181,
164,
186,
164,
203,
200,
244,
164,
243,
164,
199,
184,
171,
164,
187,
164,
222,
164,
185,
164,
200,
197,
250,
164,
168,
164,
191,
161,
163,
10,
191,
198,
190,
249,
164,
234,
164,
206,
204,
181,
197,
180,
203,
164,
164,
199,
190,
174,
182,
161,
164,
206,
187,
254,
164,
171,
164,
233,
194,
187,
164,
208,
164,
171,
164,
234,
164,
183,
164,
198,
164,
164,
164,
235,
161,
163,
10,
229,
136,
165,
230,
174,
181,
230,
183,
177,
227,
129,
132,
231,
144,
134,
231,
148,
177,
227,
129,
167,
227,
130,
130,
227,
129,
170,
227,
129,
132,
227,
128,
130,
10,
230,
151,
167,
232,
168,
152,
227,
129,
171,
227,
130,
136,
227,
130,
139,
227,
129,
168,
227,
128,
129,
228,
187,
143,
229,
131,
143,
227,
130,
132,
228,
187,
143,
229,
133,
183,
227,
130,
146,
230,
137,
147,
231,
160,
149,
227,
129,
132,
227,
129,
166,
227,
128,
129,
227,
129,
157,
227,
129,
174,
228,
184,
185,
227,
129,
140,
227,
129,
164,
227,
129,
132,
227,
129,
159,
227,
130,
138,
227,
128,
129,
233,
135,
145,
233,
138,
128,
227,
129,
174,
231,
174,
148,
227,
129,
140,
227,
129,
164,
227,
129,
132,
227,
129,
159,
227,
130,
138,
227,
129,
151,
227,
129,
159,
230,
156,
168,
227,
130,
146,
227,
128,
129,
232,
183,
175,
227,
129,
176,
227,
129,
159,
227,
129,
171,
227,
129,
164,
227,
129,
191,
233,
135,
141,
227,
129,
173,
227,
129,
166,
227,
128,
129,
232,
150,
170,
227,
129,
174,
230,
150,
153,
227,
129,
171,
229,
163,
178,
227,
129,
163,
227,
129,
166,
227,
129,
132,
227,
129,
159,
227,
129,
168,
228,
186,
145,
227,
129,
134,
228,
186,
139,
227,
129,
167,
227,
129,
130,
227,
130,
139,
227,
128,
130,
10
];

827
jp-encoding/instances/data800.dzn Normal file
View File

@ -0,0 +1,827 @@
len = 824;
stream = [
130,
187,
130,
177,
130,
197,
129,
65,
147,
250,
130,
204,
150,
218,
130,
170,
140,
169,
130,
166,
130,
200,
130,
173,
130,
200,
130,
233,
130,
198,
129,
65,
146,
78,
130,
197,
130,
224,
139,
67,
150,
161,
130,
240,
136,
171,
130,
233,
130,
170,
130,
193,
130,
196,
129,
65,
130,
177,
130,
204,
150,
229,
130,
204,
139,
223,
143,
138,
130,
214,
130,
205,
145,
171,
130,
212,
130,
221,
130,
240,
130,
181,
130,
200,
130,
162,
142,
150,
130,
201,
130,
200,
130,
193,
130,
196,
130,
181,
130,
220,
130,
193,
130,
189,
130,
204,
130,
197,
130,
160,
130,
233,
129,
66,
10,
84,
104,
101,
32,
113,
117,
105,
99,
107,
32,
98,
114,
111,
119,
110,
32,
102,
111,
120,
32,
106,
117,
109,
112,
115,
32,
111,
118,
101,
114,
32,
116,
104,
101,
32,
108,
97,
122,
121,
32,
100,
111,
103,
10,
130,
187,
130,
234,
130,
170,
129,
65,
130,
177,
130,
204,
146,
106,
130,
204,
130,
217,
130,
169,
130,
201,
130,
205,
146,
78,
130,
224,
130,
162,
130,
200,
130,
162,
129,
66,
10,
178,
191,
184,
206,
164,
171,
164,
200,
177,
190,
164,
166,
164,
200,
161,
162,
164,
179,
164,
206,
198,
243,
187,
176,
199,
175,
161,
162,
181,
254,
197,
212,
164,
203,
164,
207,
161,
162,
195,
207,
191,
204,
164,
200,
164,
171,
196,
212,
201,
247,
164,
200,
164,
171,
178,
208,
187,
246,
164,
200,
164,
171,
241,
192,
241,
188,
164,
200,
164,
171,
177,
190,
164,
166,
186,
210,
164,
172,
164,
196,
164,
197,
164,
164,
164,
198,
181,
175,
164,
195,
164,
191,
161,
163,
10,
151,
133,
144,
182,
150,
229,
130,
170,
129,
65,
142,
233,
144,
157,
145,
229,
152,
72,
130,
201,
130,
160,
130,
233,
136,
200,
143,
227,
130,
205,
129,
65,
130,
177,
130,
204,
146,
106,
130,
204,
130,
217,
130,
169,
130,
201,
130,
224,
129,
65,
137,
74,
130,
226,
130,
221,
130,
240,
130,
183,
130,
233,
142,
115,
143,
151,
138,
125,
130,
226,
157,
134,
137,
71,
150,
88,
142,
113,
130,
170,
129,
65,
130,
224,
130,
164,
147,
241,
142,
79,
144,
108,
130,
205,
130,
160,
130,
232,
130,
187,
130,
164,
130,
200,
130,
224,
130,
204,
130,
197,
130,
160,
130,
233,
129,
66,
10,
227,
129,
157,
227,
130,
140,
227,
129,
140,
227,
128,
129,
227,
129,
147,
227,
129,
174,
231,
148,
183,
227,
129,
174,
227,
129,
187,
227,
129,
139,
227,
129,
171,
227,
129,
175,
232,
170,
176,
227,
130,
130,
227,
129,
132,
227,
129,
170,
227,
129,
132,
227,
128,
130,
10,
144,
101,
143,
247,
130,
232,
130,
204,
150,
179,
147,
83,
150,
67,
130,
197,
143,
172,
139,
159,
130,
204,
142,
158,
130,
169,
130,
231,
145,
185,
130,
206,
130,
169,
130,
232,
130,
181,
130,
196,
130,
162,
130,
233,
129,
66,
10,
229,
136,
165,
230,
174,
181,
230,
183,
177,
227,
129,
132,
231,
144,
134,
231,
148,
177,
227,
129,
167,
227,
130,
130,
227,
129,
170,
227,
129,
132,
227,
128,
130,
10,
142,
227,
146,
142,
130,
226,
129,
91,
130,
162,
129,
66,
130,
198,
154,
146,
130,
181,
130,
189,
130,
169,
130,
231,
130,
197,
130,
160,
130,
233,
129,
66,
143,
172,
142,
103,
130,
201,
149,
137,
130,
212,
130,
179,
130,
193,
130,
196,
139,
65,
130,
193,
130,
196,
151,
136,
130,
189,
142,
158,
129,
65,
130,
168,
130,
226,
130,
182,
130,
170,
145,
229,
130,
171,
130,
200,
138,
225,
130,
240,
130,
181,
130,
196,
147,
241,
138,
75,
130,
174,
130,
231,
130,
162,
130,
169,
130,
231,
148,
242,
130,
209,
141,
126,
130,
232,
130,
196,
141,
152,
130,
240,
148,
178,
130,
169,
130,
183,
147,
122,
130,
170,
130,
160,
130,
233,
130,
169,
130,
198,
137,
93,
130,
193,
130,
189,
130,
169,
130,
231,
129,
65,
130,
177,
130,
204,
142,
159,
130,
205,
148,
178,
130,
169,
130,
179,
130,
184,
130,
201,
148,
242,
130,
241,
130,
197,
140,
169,
130,
185,
130,
220,
130,
183,
130,
198,
147,
154,
130,
166,
130,
189,
129,
66,
10,
137,
189,
140,
204,
130,
169,
130,
198,
137,
93,
130,
164,
130,
198,
129,
65,
130,
177,
130,
204,
147,
241,
142,
79,
148,
78,
129,
65,
139,
158,
147,
115,
130,
201,
130,
205,
129,
65,
146,
110,
144,
107,
130,
198,
130,
169,
146,
210,
149,
151,
130,
198,
130,
169,
137,
206,
142,
150,
130,
198,
130,
169,
233,
95,
233,
91,
130,
198,
130,
169,
137,
93,
130,
164,
141,
208,
130,
170,
130,
194,
130,
195,
130,
162,
130,
196,
139,
78,
130,
193,
130,
189,
129,
66,
10
];

543
jp-encoding/jp-encoding.mzn Normal file
View File

@ -0,0 +1,543 @@
%
% jp-encoding.mzn
%
%
% There are several popular character encodings in Japan.
% (EUC-JP, SJIS, UTF-8)
%
% If they are mixed into one text file (by accident or something),
% text information will be lost.
% So we can define a problem "recovering original encodings" for byte stream.
%
% In this problem, byte stream (as variable 'stream') is given as input
% and encodings are assigned as output (as variable 'encoding').
%
include "table.mzn";
% *_score tables have -log(probability of appearance) * 10 for each encoding.
array[1..256] of int: sjis_score = [
135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 57, 135, 135, 135, 135, 135,
135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135,
74, 135, 128, 119, 135, 100, 135, 135, 96, 96, 112, 104, 106, 92, 106, 107,
97, 92, 99, 95, 98, 106, 107, 103, 97, 101, 105, 135, 135, 111, 135, 119,
65, 46, 45, 64, 75, 74, 79, 78, 71, 74, 79, 76, 71, 79, 59, 64,
81, 78, 70, 67, 80, 81, 70, 82, 69, 81, 75, 72, 62, 60, 73, 70,
76, 79, 75, 66, 77, 75, 78, 73, 77, 43, 43, 79, 54, 68, 68, 61,
73, 67, 80, 66, 69, 53, 51, 72, 73, 68, 74, 71, 77, 80, 77, 135,
77, 28, 11, 51, 75, 73, 69, 69, 51, 47, 49, 49, 44, 49, 41, 47,
44, 48, 48, 47, 50, 46, 45, 48, 63, 76, 75, 79, 74, 68, 63, 73,
50, 67, 40, 80, 45, 79, 56, 71, 59, 42, 45, 55, 67, 49, 68, 58,
69, 53, 65, 54, 69, 45, 57, 50, 64, 60, 65, 54, 67, 44, 49, 58,
66, 47, 58, 74, 43, 47, 43, 59, 43, 45, 62, 62, 40, 45, 60, 72,
71, 69, 72, 68, 61, 80, 62, 68, 72, 68, 70, 75, 51, 66, 67, 61,
47, 56, 59, 61, 62, 53, 53, 47, 51, 43, 49, 60, 74, 60, 83, 74,
47, 47, 76, 71, 78, 82, 77, 83, 80, 81, 70, 67, 67, 135, 135, 135
];
array[1..256] of int: eucjp_score = [
135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 57, 135, 135, 135, 135, 135,
135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135,
74, 135, 128, 119, 135, 100, 135, 135, 96, 96, 112, 104, 106, 92, 106, 107,
97, 92, 99, 95, 98, 106, 107, 103, 97, 101, 105, 135, 135, 111, 135, 119,
135, 112, 114, 100, 108, 102, 135, 113, 121, 110, 124, 135, 111, 106, 111, 111,
100, 135, 114, 109, 112, 124, 135, 135, 124, 119, 128, 128, 121, 128, 135, 135,
135, 94, 128, 102, 104, 95, 113, 97, 108, 90, 124, 124, 99, 101, 95, 90,
105, 135, 93, 99, 94, 108, 128, 113, 135, 124, 117, 135, 135, 135, 135, 135,
135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135,
135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135,
135, 28, 41, 44, 11, 50, 45, 72, 55, 64, 57, 42, 45, 54, 65, 46,
49, 49, 51, 48, 50, 48, 54, 41, 45, 45, 52, 44, 48, 45, 49, 39,
43, 50, 51, 43, 49, 53, 40, 43, 41, 50, 34, 36, 48, 45, 38, 43,
53, 66, 62, 66, 61, 62, 49, 50, 59, 62, 62, 63, 63, 68, 50, 63,
63, 58, 46, 55, 57, 59, 58, 52, 50, 46, 49, 43, 48, 58, 63, 58,
73, 67, 46, 46, 70, 68, 58, 66, 71, 73, 72, 74, 66, 61, 58, 135
];
array[1..256] of int: utf8_score = [
139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 61, 139, 139, 139, 139, 139,
139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139,
78, 139, 132, 123, 139, 104, 139, 139, 100, 100, 116, 108, 110, 96, 110, 111,
101, 96, 103, 99, 102, 110, 111, 107, 101, 105, 109, 139, 139, 115, 139, 139,
139, 116, 118, 104, 112, 107, 139, 117, 125, 114, 128, 139, 115, 110, 115, 115,
104, 139, 118, 113, 116, 128, 139, 139, 128, 123, 132, 132, 125, 132, 139, 139,
139, 98, 132, 107, 108, 99, 117, 101, 112, 95, 128, 128, 103, 105, 99, 94,
109, 139, 97, 103, 98, 112, 132, 117, 139, 128, 121, 139, 139, 139, 139, 139,
36, 17, 27, 51, 42, 55, 47, 54, 41, 40, 49, 38, 42, 47, 64, 48,
53, 52, 49, 45, 56, 51, 56, 46, 58, 50, 58, 52, 57, 51, 65, 46,
51, 53, 63, 48, 54, 54, 44, 48, 45, 54, 45, 46, 61, 53, 42, 47,
53, 61, 63, 57, 61, 63, 62, 62, 48, 59, 45, 53, 39, 57, 49, 57,
139, 139, 139, 132, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 118, 139,
139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139,
139, 139, 68, 14, 42, 36, 40, 44, 44, 47, 139, 139, 139, 139, 139, 40,
139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139
];
%
% labels for encoding
%
int: e_ascii = 0;
int: e_euc_jp = 1;
int: e_sjis = 2;
int: e_utf8 = 3;
int: e_unknown = 4;
%
% labels for byte_status
%
int: b_ascii = 0;
int: b_euc1 = 1;
int: b_euc2 = 2;
int: b_sjis1_1 = 3;
int: b_sjis2_1 = 4;
int: b_sjis2_2 = 5;
int: b_utf8_2_1 = 6;
int: b_utf8_2_2 = 7;
int: b_utf8_3_1 = 8;
int: b_utf8_3_2 = 9;
int: b_utf8_3_3 = 10;
int: b_utf8_4_1 = 11;
int: b_utf8_4_2 = 12;
int: b_utf8_4_3 = 13;
int: b_utf8_4_4 = 14;
int: b_unknown = 15;
%
% test data
%
% int: len = 12;
% array[1..len] of int: stream = [ 227, 129, 138, 227, 129, 175, 227, 130, 136, 227, 129, 134 ];
int: len;
set of int: rng = 1..len;
array[rng] of int: stream;
% int: len = 3 ;
% array[rng] of int: stream = [ 65, 66, 67 ];
%------------------------------------------------------------------------------%
% Variables
array[rng] of var 0..b_unknown: byte_status;
array[rng] of var 0..e_unknown: encoding;
array[rng] of var 0..1: char_start;
set of int: scoreType = 0..max(i in 1..256)(eucjp_score[i] + sjis_score[i] + utf8_score[i]) + 1000;
int: maxObj = len * (max(i in 1..256)(eucjp_score[i] + sjis_score[i] + utf8_score[i]) + 1000);
var 0..maxObj: objective;
constraint objective = sum (i in rng) (
score_of(encoding[i],stream[i])
);
predicate score_computation(var 0..e_unknown:encoding_i, var 0..255:stream_i, var scoreType: score_i) ::presolve(model) =
score_i = (bool2int(encoding_i == e_euc_jp) * eucjp_score[stream_i+1]
+ bool2int(encoding_i == e_sjis) * sjis_score[stream_i+1]
+ bool2int(encoding_i == e_utf8) * utf8_score[stream_i+1]
+ bool2int(encoding_i == e_unknown) * 1000);
function var scoreType: score_of(var int: encoding_i, int: stream_i) =
let{
var scoreType: score_i;
constraint score_computation(encoding_i,stream_i, score_i);
} in score_i;
%------------------------------------------------------------------------------%
% Constraints
constraint forall (i in rng) (
if i >= 2 then link_statuses(byte_status[i],byte_status[i-1]) else true endif
/\
link_vars(encoding[i],byte_status[i],char_start[i])
/\
init(byte_status[i],i)
/\
stream_to_status(i,stream,byte_status[i])
);
predicate link_vars(var int: encoding_i, var int: byte_status_i, var int: char_start_i) ::presolve =
(forall([
%
% byte_status -> encoding
%
encoding_i = e_ascii <-> byte_status_i = b_ascii
,
encoding_i = e_euc_jp ->
byte_status_i = b_euc1 \/ byte_status_i = b_euc2
,
(encoding_i = e_sjis ->
byte_status_i = b_sjis1_1
\/ byte_status_i = b_sjis2_1
\/ byte_status_i = b_sjis2_2)
,
encoding_i = e_utf8 ->
byte_status_i = b_utf8_2_1
\/ byte_status_i = b_utf8_2_2
\/ byte_status_i = b_utf8_3_1
\/ byte_status_i = b_utf8_3_2
\/ byte_status_i = b_utf8_3_3
\/ byte_status_i = b_utf8_4_1
\/ byte_status_i = b_utf8_4_2
\/ byte_status_i = b_utf8_4_3
\/ byte_status_i = b_utf8_4_4
,
byte_status_i = b_unknown <-> encoding_i = e_unknown
,
%
% byte_status -> char_start
%
byte_status_i = b_ascii -> char_start_i = 1
,
byte_status_i = b_utf8_2_1 -> char_start_i = 1
,
byte_status_i = b_utf8_2_2 -> char_start_i = 0
,
byte_status_i = b_utf8_3_1 -> char_start_i = 1
,
byte_status_i in {b_utf8_3_2, b_utf8_3_3} -> char_start_i = 0
,
byte_status_i = b_utf8_4_1 -> char_start_i = 1
,
byte_status_i in {b_utf8_4_2, b_utf8_4_3, b_utf8_4_4} -> char_start_i = 0
,
byte_status_i = b_euc1 -> char_start_i = 1
,
byte_status_i = b_euc2 -> char_start_i = 0
,
byte_status_i = b_sjis1_1 -> char_start_i = 1
,
byte_status_i = b_sjis2_1 -> char_start_i = 1
,
byte_status_i = b_sjis2_2 -> char_start_i = 0
,
%
% unknown
%
byte_status_i = b_unknown -> char_start_i = 1
]));
predicate stream_to_status(int:i, array[int] of int: stream, var int: byte_status_i) =
( forall([
%
% ASCII
%
if (stream[i] < 128) then true else
byte_status_i != b_ascii endif
,
%
% UTF-8
%
% C2-DF, 80-BF
if (i >= len) then
byte_status_i != b_utf8_2_1
else
if ((194 <= stream[i] /\ stream[i] <= 223)
/\ (128 <= stream[i+1] /\ stream[i+1] <= 191))
then true else
byte_status_i != b_utf8_2_1
endif
endif
,
% E0-EF, 80-BF, 80-BF
if (i >= len - 1) then
byte_status_i != b_utf8_3_1
else
if ((224 <= stream[i] /\ stream[i] <= 239)
/\ (128 <= stream[i+1] /\ stream[i+1] <= 191)
/\ (128 <= stream[i+2] /\ stream[i+2] <= 191))
then true else
byte_status_i != b_utf8_3_1
endif
endif
,
% F0-F7, 80-BF, 80-BF, 80-BF
if (i >= len - 2) then
byte_status_i != b_utf8_4_1
else
if (240 <= stream[i] /\ stream[i] <= 247
/\ 128 <= stream[i+1] /\ stream[i+1] <= 191
/\ 128 <= stream[i+2] /\ stream[i+2] <= 191
/\ 128 <= stream[i+3] /\ stream[i+3] <= 191)
then true else
byte_status_i != b_utf8_4_1
endif
endif
,
%
% EUC-JP (CP51932)
% (A1-A8, AD, B0-F4, F9-FC), (A1-FE)
%
if (i >= len) then
byte_status_i !=b_euc1
else
if ((161 <= stream[i] /\ stream[i] <= 168)
\/ (173 = stream[i])
\/ (176 <= stream[i] /\ stream[i] <= 244)
\/ (249 <= stream[i] /\ stream[i] <= 252))
/\ (161 <= stream[i+1] /\ stream[i+1] <= 254)
then true else
byte_status_i != b_euc1
endif
endif
,
%
% SJIS
%
% (A1-DF)
if (161 <= stream[i] /\ stream[i] <= 223)
then true else
byte_status_i != b_sjis1_1
endif
,
% (81-9F, E0-FC), (40-7E, 80-FC)
if (i >= len) then
byte_status_i != b_sjis2_1
else
if ((129 <= stream[i] /\ stream[i] <= 159)
\/ (224 <= stream[i] /\ stream[i] <= 252))
/\ ((64 <= stream[i+1] /\ stream[i+1] <= 126)
\/ (128 <= stream[i+1] /\ stream[i+1] <= 252))
then true else
byte_status_i != b_sjis2_1
endif
endif
])
);
predicate stream_to_status_old(int:i, array[int] of int: stream, var int: byte_status_i) =
( forall([
%
% ASCII
%
if (stream[i] < 128) then true else
byte_status_i != b_ascii endif
,
%
% UTF-8
%
% C2-DF, 80-BF
if (i >= len) then
byte_status_i != b_utf8_2_1
else
byte_status_i = b_utf8_2_1 ->
((194 <= stream[i] /\ stream[i] <= 223)
/\ (128 <= stream[i+1] /\ stream[i+1] <= 191))
endif
,
% E0-EF, 80-BF, 80-BF
if (i >= len - 1) then
byte_status_i != b_utf8_3_1
else
byte_status_i = b_utf8_3_1 ->
((224 <= stream[i] /\ stream[i] <= 239)
/\ (128 <= stream[i+1] /\ stream[i+1] <= 191)
/\ (128 <= stream[i+2] /\ stream[i+2] <= 191))
endif
,
% F0-F7, 80-BF, 80-BF, 80-BF
if (i >= len - 2) then
byte_status_i != b_utf8_4_1
else
byte_status_i = b_utf8_4_1 ->
(240 <= stream[i] /\ stream[i] <= 247
/\ 128 <= stream[i+1] /\ stream[i+1] <= 191
/\ 128 <= stream[i+2] /\ stream[i+2] <= 191
/\ 128 <= stream[i+3] /\ stream[i+3] <= 191)
endif
,
%
% EUC-JP (CP51932)
% (A1-A8, AD, B0-F4, F9-FC), (A1-FE)
%
if (i >= len) then
byte_status_i !=b_euc1
else
byte_status_i = b_euc1 ->
((161 <= stream[i] /\ stream[i] <= 168)
\/ (173 = stream[i])
\/ (176 <= stream[i] /\ stream[i] <= 244)
\/ (249 <= stream[i] /\ stream[i] <= 252))
/\ (161 <= stream[i+1] /\ stream[i+1] <= 254)
endif
,
%
% SJIS
%
% (A1-DF)
byte_status_i = b_sjis1_1 ->
(161 <= stream[i] /\ stream[i] <= 223)
,
% (81-9F, E0-FC), (40-7E, 80-FC)
if (i >= len) then
byte_status_i != b_sjis2_1
else
byte_status_i = b_sjis2_1 ->
((129 <= stream[i] /\ stream[i] <= 159)
\/ (224 <= stream[i] /\ stream[i] <= 252))
/\ ((64 <= stream[i+1] /\ stream[i+1] <= 126)
\/ (128 <= stream[i+1] /\ stream[i+1] <= 252))
endif
])
);
predicate link_statuses(var int: byte_status_i, var int: byte_status_im1) ::presolve =
( forall([
%
% UTF-8
%
% C2-DF, 80-BF
byte_status_i == b_utf8_2_2 <-> byte_status_im1 == b_utf8_2_1
,
% E0-EF, 80-BF, 80-BF
byte_status_i == b_utf8_3_2 <-> byte_status_im1 == b_utf8_3_1
,
byte_status_i == b_utf8_3_3 <-> byte_status_im1 == b_utf8_3_2
,
% F0-F7, 80-BF, 80-BF, 80-BF
byte_status_i == b_utf8_4_2 <-> byte_status_im1 == b_utf8_4_1
,
byte_status_i == b_utf8_4_3 <-> byte_status_im1 == b_utf8_4_2
,
byte_status_i == b_utf8_4_4 <-> byte_status_im1 == b_utf8_4_3
,
%
% EUC-JP (CP51932)
% (A1-A8, AD, B0-F4, F9-FC), (A1-FE)
%
byte_status_i == b_euc2 <-> byte_status_im1 = b_euc1
,
%
% SJIS
%
% (A1-DF)
% (81-9F, E0-FC), (40-7E, 80-FC)
byte_status_i == b_sjis2_2 <-> byte_status_im1 == b_sjis2_1
])
);
predicate init(var int: byte_status_i, int: i) =
( forall([
%
% UTF-8
%
% C2-DF, 80-BF
if (i < 2) then
byte_status_i != b_utf8_2_2
else
true
endif
,
% E0-EF, 80-BF, 80-BF
if (i < 2) then
byte_status_i != b_utf8_3_2
else
true
endif
,
if (i < 3) then
byte_status_i != b_utf8_3_3
else
true
endif
,
% F0-F7, 80-BF, 80-BF, 80-BF
if (i < 2) then
byte_status_i != b_utf8_4_2
else
true
endif
,
if (i < 3) then
byte_status_i != b_utf8_4_3
else
true
endif
,
if (i < 4) then
byte_status_i != b_utf8_4_4
else
true
endif
,
%
% EUC-JP (CP51932)
% (A1-A8, AD, B0-F4, F9-FC), (A1-FE)
%
if (i < 2) then
byte_status_i != b_euc2
else
true
endif
,
%
% SJIS
%
% (A1-DF)
% (81-9F, E0-FC), (40-7E, 80-FC)
if (i < 2) then
byte_status_i != b_sjis2_2
else
true
endif
])
);
%------------------------------------------------------------------------------%
% Search and Solve
solve
:: seq_search([
int_search(byte_status, first_fail, indomain_split, complete),
int_search(char_start, input_order, indomain_max, complete),
int_search(encoding, first_fail, indomain_split, complete)
])
minimize objective;
%------------------------------------------------------------------------------%
% Output
output [
"encoding = ", show(encoding), ";\n",
"byte_status = ", show(byte_status), ";\n",
"char_start = ", show(char_start), ";\n",
"constraint objective = ", show(objective), ";\n"
]