Adding at most k and at least k constraints to a word puzzle

205 Views Asked by At

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:

  1. 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.
  2. What about if I want an at least k constraint?
0

There are 0 best solutions below