to be n puzzle4x4-1
puzzle:
mind be1 or not
to1 be2 that is
to2 question whether 'tis
the1 nobler in the2
0: mind be1 or not to1 be2 that is to2 question whether 'tis the1 nobler in the2
0: to1 be1 or not mind be2 that is to2 question whether 'tis the1 nobler in the2
0: to1 be1 or not to2 be2 that is mind question whether 'tis the1 nobler in the2
0: to1 be1 or not to2 be2 that is the1 question whether 'tis mind nobler in the2
0: to1 be1 or not to2 be2 that is the1 question whether 'tis nobler mind in the2
0: to1 be1 or not to2 be2 that is the1 question whether 'tis nobler in mind the2
1: to1 be1 or not to2 be2 that is the1 question whether 'tis nobler in the2 mind
1: to1 be1 or not to2 be2 that is the1 question whether 'tis nobler in the2 mind
1: to1 be1 or not to2 be2 that is the1 question whether 'tis nobler in the2 mind
1: to1 be1 or not to2 be2 that is the1 question whether 'tis nobler in the2 mind
1: to1 be1 or not to2 be2 that is the1 question whether 'tis nobler in the2 mind
1: to1 be1 or not to2 be2 that is the1 question whether 'tis nobler in the2 mind
1: to1 be1 or not to2 be2 that is the1 question whether 'tis nobler in the2 mind
1: to1 be1 or not to2 be2 that is the1 question whether 'tis nobler in the2 mind
1: to1 be1 or not to2 be2 that is the1 question whether 'tis nobler in the2 mind
moves:
- to1
to1 to2
to2 the1
the1 nobler
nobler in
in the2
the2 mind
be1 -
be1 -
be1 -
be1 -
be1 -
be1 -
be1 -
be1 -
MiniZinc model
include "globals.mzn";
int: n;
int: t = n*n;
array[1..t] of 1..t: puzzle;
array[0..16] of string: s = array1d(0..16, ["- ",
"to1 ",
"be1 ",
"or ",
"not ",
"to2 ",
"be2 ",
"that ",
"is ",
"the1 ",
"question",
"whether ",
"'tis ",
"nobler ",
"in ",
"the2 ",
"mind "
]);
int: num_sols;
int: num_connections = sum([1 | i1 in 1..n, j1 in 1..n, i2 in 1..n, j2 in 1..n
where (abs(j1-j2) = 1 /\ i1 = i2) \/ (abs(i1-i2) = 1 /\ j1 mod n = j2 mod n)]);
predicate table_int_reif(array[int] of var int: x, array[int, int] of int: t, var bool: b) =
assert (index_set_2of2(t) == index_set(x),
"The second dimension of the table must equal the number of variables "
++ "in the first argument",
let { int: l = min(index_set(x)),
int: u = max(index_set(x)),
int: lt = min(index_set_1of2(t)),
int: ut = max(index_set_1of2(t)),
var lt..ut: i,
array[l..u, lt..ut] of int: t_transposed =
array2d(l..u, lt..ut, [ t[i,j] | j in l..u, i in lt..ut ]) }
in
b <-> forall(j in l..u) (
t_transposed[j,i] = x[j]
)
);
array[1..num_connections, 1..2] of int: valid_connections =
array2d(1..num_connections, 1..2,
[
if k = 1 then
(i1-1)*n+j1
else
(i2-1)*n+j2
endif
| i1 in 1..n, j1 in 1..n, i2 in 1..n, j2 in 1..n, k in 1..2
where (abs(j1-j2) = 1 /\ i1 = i2) \/ (abs(i1-i2) = 1 /\ j1 mod n = j2 mod n)
])
;
array[1..num_sols, 1..2] of var 0..t: moves;
array[1..num_sols, 1..t] of var 1..t: x;
array[1..num_sols] of var 0..1: operations;
array[1..t, 1..t] of 0..1: valid_moves;
array[1..num_sols] of var 0..1: check;
var 1..num_sols: check_ix;
array[1..num_sols] of var 0..t: changes;
predicate same(array[int] of var int: x, array[int] of var int: y) =
let {
int: n = card(index_set(x))
}
in
forall(i in 1..n) (
y[i] = x[i]
)
;
solve minimize check_ix;
constraint
% initializations
check[1] = 0
/\
moves[1, 1] = 0
/\
changes[1] = 0
/\
% identify the empty block in the puzzle configuration
exists(j in 1..t) (
x[1, j] = t
/\
moves[1, 2] = j
)
/\ % initialize first row in x with the puzzle
forall(j in 1..t) (
x[1,j] = puzzle[j]
)
/\ % last row should be 1..t (this is the goal)
forall(j in 1..t) (
x[num_sols, j] = j
)
/\ % select the operations
forall(i in 2..num_sols) (
all_different([x[i, j] | j in 1..t]) :: domain
/\
% at most 2 changes of each move
changes[i] = sum(j in 1..t) (bool2int(x[i,j] != x[i-1,j]))
/\
(changes[i] = 2 \/ changes[i] = 0)
/\
( % is this row a solution (i.e. 1..t)? Then we're done.
check[i] = 1
<->
same([j | j in 1..t], [x[i,j] | j in 1..t ])
)
/\ % select operations
(
( % either the row is same as last line
same([x[i-1,j] | j in 1..t], [x[i,j] | j in 1..t ])
/\
operations[i] = 0
/\
moves[i,1] = 2 % dummy move
/\
moves[i,2] = 0
)
\/
( % or we move a piece
moves[i-1, 2] = moves[i, 1]
/\
x[i-1,moves[i,1]] = t % find the blank
/\
table([moves[i,1], moves[i,2]], valid_connections)
/\
x[i, moves[i,2]] = t
/\
operations[i] = 1
/\
moves[i,1] > 0
/\
moves[i,2] > 0
)
)
)
/\ % check_ix is the first index where we have a solution
exists(i in 2..num_sols) (
check_ix = i
/\
check[i] = 1
/\ % no other solutions before check_ix = i
forall(j in 2..i-1) ( check[j] = 0)
)
;
output
["\npuzzle:"] ++
[
if i mod (ceil(sqrt(int2float(t)))) = 1 then "\n" else " " endif ++
show(s[puzzle[i]])
| i in 1..t
] ++ ["\n"] ++
[
if j = 1 then "\n" ++ show(check[i]) ++ ": " else " " endif ++
show(s[fix(x[i,j])])
| i in 1..num_sols, j in 1..t
] ++
["\nmoves:"]
++
[
if j = 1 then "\n" else " " endif ++
show(s[fix(moves[i,j])])
| i in 1..num_sols, j in 1..2
] ++ ["\n"];
% problem
num_sols = 15;
n = 4;
puzzle = [16, 2, 3, 4,
1, 6, 7, 8,
5,10,11,12,
9,13,14,15];
valid_moves = array2d(1..t, 1..t, [
% 1,2,3,4,5,6,7,8,9,0,1,2,3,4,5,6
0,1,0,0,1,0,0,0,0,0,0,0,0,0,0,0, % 1
1,0,1,0,0,1,0,0,0,0,0,0,0,0,0,0, % 2
0,1,0,1,0,0,1,0,0,0,0,0,0,0,0,0, % 3
0,0,1,0,0,0,0,1,0,0,0,0,0,0,0,0, % 4
1,0,0,0,0,1,0,0,1,0,0,0,0,0,0,0, % 5
0,1,0,0,1,1,0,0,0,1,0,0,0,0,0,0, % 6
0,0,1,0,0,1,0,1,0,0,1,0,0,0,0,0, % 7
0,0,0,1,0,0,1,0,0,0,0,1,0,0,0,0, % 8
0,0,0,0,1,0,0,0,0,1,0,0,1,0,0,0, % 9
0,0,0,0,0,1,0,0,1,0,1,0,0,1,0,0, % 10
0,0,0,0,0,0,1,0,0,1,0,1,0,0,1,0, % 11
0,0,0,0,0,0,0,1,0,0,1,0,0,0,0,1, % 12
0,0,0,0,0,0,0,0,1,0,0,0,0,1,0,0, % 13
0,0,0,0,0,0,0,0,0,1,0,0,1,0,1,0, % 14
0,0,0,0,0,0,0,0,0,0,1,0,0,1,0,1, % 15
0,0,0,0,0,0,0,0,0,0,0,1,0,0,1,0 % 16
]);
Back to Constrained-based constraint poetry
Created by Hakan Kjellerstrand hakank@gmail.com