this repo has no description
dekker.one
1/***
2!Test
3expected:
4- !Result
5 solution: !Solution
6 sokPosns: [14, 13, 8, 7, 8, 9, 4, 5, 10, 1, 1, 1]
7 stime: 9
8***/
9
10% Regression test for bug #335.
11% Previous versions of CPX found this model to be unsatisfiable.
12% A slightly later version found a solution but it was not optimal
13% (stime = 11, rather than the optimal stime = 9.)
14
15int: w; % width of board
16int: n; % board positions 1, ..., w, w+1, ...., 2w, ...,
17constraint assert(n mod w == 0, "board must be rectangular");
18set of int: POS = 1..n;
19int: stps; % max steps in solution
20set of int: STEPS = 1..stps;
21
22int: nw; % number of walls
23set of int: WALLS = 1..nw;
24array[WALLS] of POS: walls; % wall positions
25int: nc; % number of crates + goals
26set of int: CRATES = 1..nc;
27set of POS: goals; % goal positions;
28array[CRATES] of POS: crates; % initial crate positions
29POS: pInit; % initial sokoban position
30
31set of int: MOVES = {-w,-1,1,w}; % possible moves
32
33include "alldifferent.mzn";
34
35array[STEPS] of var POS: sokPosn; % sokoban position
36array[STEPS] of var MOVES: move; % sokoban position
37array[STEPS,CRATES] of var POS: cratePosns;
38var STEPS: stime :: add_to_output; % time of solution
39
40
41%% initial positions
42constraint sokPosn[1] = pInit;
43constraint forall(c in CRATES)(cratePosns[1,c] = crates[c]);
44
45%% no overlap of crates, walls and sokoban
46constraint forall(s in STEPS)(
47 alldifferent(walls ++ [sokPosn[s]] ++ [cratePosns[s,c] | c in CRATES])
48 );
49
50%% at the end all crates are in a position
51constraint forall(c in CRATES)(
52 cratePosns[stime,c] in goals
53 );
54
55% legal move at each step
56constraint forall(s in 1..stps-1)(
57 sokPosn[s+1] - sokPosn[s] = move[s]
58 );
59
60% crate pushing
61constraint forall(s in 1..stps-1, c in CRATES)(
62 cratePosns[s+1,c] = cratePosns[s,c] + bool2int(sokPosn[s+1] == cratePosns[s,c]) * move[s]
63 );
64
65solve minimize stime;
66
67% output for test case comparison
68array[STEPS] of var POS: sokPosns :: add_to_output;
69constraint forall (s in 1..stime) (sokPosns[s] = sokPosn[s]);
70constraint forall (s in (stime+1)..stps) (sokPosns[s] = 1); % Just fill the rest with 1 for consistency
71
72w = 5;
73n = 15;
74stps = 12;
75
76nw = 0;
77walls = [];
78
79nc = 2;
80crates = [7,9];
81goals = {6,15};
82pInit = 14;