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