I'm toying around with Minizinc trying to learn to be more proficient with it. I'm trying to place letters into the 3x3 grid with the middle cell unassignable, so that the words intersect like in a word puzzle. To keep it neat, say we can use only 4 words, say axe, ace, ero, evo. A possible solution is:
a x e
c . r
e v o
My corresponding Minizinc model is:
include "globals.mzn";
int: num_words1 = 26;
array[1..num_words1, 1..1] of int: words1 = array2d(1..num_words1, 1..1,
[
a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z,
]);
int: num_words3 = 4;
array[1..num_words3, 1..3] of int: words3 = array2d(1..num_words3, 1..3,
[
a,c,e,
a,x,e,
e,r,o,
e,v,o,
]);
int: a = 1; int: b = 2; int: c = 3; int: d = 4; int: e = 5; int: f = 6;
int: g = 7; int: h = 8; int: i = 9; int: j = 10; int: k = 11; int: l = 12;
int: m = 13; int: n = 14; int: o = 15; int: p = 16; int: q = 17; int: r = 18;
int: s = 19; int: t = 20; int: u = 21; int: v = 22; int: w = 23; int: x = 24;
int: y = 25; int: z = 26;
int: num_letters = 26;
array[1..num_letters] of string: letters =
["a","b","c","d","e","f","g","h","i","j","k","l","m",
"n","o","p","q","r","s","t","u","v","w","x","y","z"
];
% number of letters to assign
int: N = 8;
% decision variables with a dummy for natural indexing
array[0..N] of var 1..num_letters: L;
constraint L[0] = 1;
solve :: int_search(L, first_fail, indomain_min, complete) satisfy;
constraint
forall(I,J in 1..num_segments where I < J) (
% 1-letter words must be able to be the same across and down
if sum(K in 1..max_length) ( bool2int(segments[I,K] > 0 ) ) = 1 /\
segments[I,1] = segments[J,1]
then
true
else
not(forall(K in 1..max_length) (
L[segments[I,K]] = L[segments[J,K]]
))
endif
);
constraint
table([L[1],L[2],L[3]], words3) /\
table([L[4]], words1) /\
table([L[5]], words1) /\
table([L[6],L[7],L[8]], words3) /\
table([L[1],L[4],L[6]], words3) /\
table([L[2]], words1) /\
table([L[7]], words1) /\
table([L[3],L[5],L[8]], words3);
int: max_length = 3;
int: num_segments = 8;
array[1..num_segments, 1..max_length] of int: segments = array2d(1..num_segments, 1..max_length,
[
% across
1,2,3,
4,0,0,
5,0,0,
6,7,8,
% down
1,4,6,
2,0,0,
7,0,0,
3,5,8,
]);
Now, I have a real problem that uses a similar setup into which I'm trying to incorporate "at most k" and "at least k" type of constraints. To handle "at most k", I figured I can just add:
int: group_0_len = 4;
array[1..group_0_len] of var 0..1: group_0;
constraint sum(group_0) <= 4;
constraint (L[1] = a /\ L[2] = c /\ L[3] = e) -> group_0[1] = 1;
constraint (L[6] = a /\ L[7] = c /\ L[8] = e) -> group_0[1] = 1;
constraint (L[1] = a /\ L[4] = c /\ L[6] = e) -> group_0[1] = 1;
constraint (L[3] = a /\ L[5] = c /\ L[8] = e) -> group_0[1] = 1;
constraint (L[1] = a /\ L[2] = x /\ L[3] = e) -> group_0[2] = 1;
constraint (L[6] = a /\ L[7] = x /\ L[8] = e) -> group_0[2] = 1;
constraint (L[1] = a /\ L[4] = x /\ L[6] = e) -> group_0[2] = 1;
constraint (L[3] = a /\ L[5] = x /\ L[8] = e) -> group_0[2] = 1;
constraint (L[1] = e /\ L[2] = r /\ L[3] = o) -> group_0[3] = 1;
constraint (L[6] = e /\ L[7] = r /\ L[8] = o) -> group_0[3] = 1;
constraint (L[1] = e /\ L[4] = r /\ L[6] = o) -> group_0[3] = 1;
constraint (L[3] = e /\ L[5] = r /\ L[8] = o) -> group_0[3] = 1;
constraint (L[1] = e /\ L[2] = v /\ L[3] = o) -> group_0[4] = 1;
constraint (L[6] = e /\ L[7] = v /\ L[8] = o) -> group_0[4] = 1;
constraint (L[1] = e /\ L[4] = v /\ L[6] = o) -> group_0[4] = 1;
constraint (L[3] = e /\ L[5] = v /\ L[8] = o) -> group_0[4] = 1;
and modify the search line to be
solve :: int_search(L++group_0, first_fail, indomain_min, complete) satisfy;
In this case, if k = 4 the instance is SAT, but if the sum is required to be less than 4, the instance is UNSAT since the group just happens to correspond to the whole group of 4 words.
I have two questions:
- Is there a more direct or cleaner way of setting up an at most k constraint in this case? Of course, I want to model this in a way that that would be most useful for the solver and lead to good propagation and quick runtimes.
- What about if I want an at least k constraint?