this repo has no description
dekker.one
1% blocksworld_model.mzn
2% vim: ft=zinc ts=4 sw=4 et tw=0
3%
4% A state-based blocks-world model.
5
6include "globals.mzn";
7
8 % Instance parameter: the number of steps to consider in the plan.
9 %
10int: n_steps;
11
12set of int: steps = 1..n_steps;
13
14 % The last step.
15 %
16int: end = n_steps;
17
18 % Instance parameter: the number of blocks in the problem.
19 %
20int: n_blocks;
21
22set of int: blocks = 1..n_blocks;
23
24 % Block 0 denotes the table, which has enough space for all the blocks.
25 %
26int: Table = 0;
27
28set of int: table_or_blocks = {Table} union blocks;
29
30 % Instance parameter: the starting locations of blocks in the problem.
31 %
32array [blocks] of table_or_blocks: initial_loc;
33
34 % Instance parameter: the finishing locations of blocks in the problem.
35 %
36array [blocks] of table_or_blocks: final_loc;
37
38 % If a block has a negative location then it's on the table.
39 % Block a has its own "free" spot on the table at location -a.
40 %
41set of int: locs = -n_blocks..n_blocks;
42
43 % Decision variables: block locations at each step.
44 %
45array [steps, blocks] of var locs: on;
46
47 % Constrain the starting state.
48 %
49constraint
50 forall (b in blocks) (
51 if initial_loc[b] = Table then
52 on[1, b] = -b
53 else
54 on[1, b] = initial_loc[b]
55 endif
56 );
57
58 % Constrain the goal state.
59 %
60constraint
61 forall (b in blocks) (
62 if final_loc[b] = Table then
63 on[end, b] = -b
64 else
65 on[end, b] = final_loc[b]
66 endif
67 );
68
69 % Ensure each block cannot be put in the wrong place on the table
70 % (this simplifies the model and allows us to use alldifferent below)
71 % or on itself.
72 %
73constraint
74 forall (b in blocks, s in steps) (
75 on[s, b] in {c | c in blocks where c != b} union {-b}
76 );
77
78 % No two blocks can occupy the same location at the same time.
79 %
80constraint
81 forall (s in steps) (alldifferent (b in blocks) (on[s, b]));
82
83 % A clear block is one that has no other block on top of it.
84 % The table is always clear.
85 %
86predicate clear(steps: s, var locs: l) =
87 l < 0 \/ forall (b in blocks) (on[s, b] != l);
88
89 % If a block moves then it must (a) be clear and (b) its destination
90 % must be clear.
91 %
92constraint
93 forall (s in steps, b in blocks where s < n_steps) (
94 on[s, b] != on[s + 1, b]
95 ->
96 ( clear(s, b)
97 /\ clear(s, on[s + 1, b])
98 )
99 );
100
101solve :: int_search(
102 [on[s, b] | s in steps, b in blocks],
103 first_fail,
104 indomain_split,
105 complete
106 )
107 satisfy;
108
109output
110 [ "[Negative locations denote the table.]\n"
111 ] ++
112 [ if b = 1 then
113 "Step " ++ show(s) ++ ":\n"
114 else
115 ""
116 endif ++
117 " block " ++ show(b) ++ " on " ++ show(on[s, b]) ++ "\n"
118 | s in 1..n_steps, b in 1..n_blocks
119 ];
120