How to avoid integer overflow in MiniZinc?

Question

I am trying to solve a code-game from codingame website using MiniZinc for Python. All I have to do is to find the number of the possible combination in a morse code, given a vocabulary (a set of possible words that, converted and concatenated, should precisely be equal to the input morse code). I have been able to sort out a solution pretty fast, but the problem is that whatever solver I use, I get an integer overflow. I tried to use OptiMathSAT but I could not manage to apply it.

Here, you can find my code (you will not find the count of the possible combination, but I think it would be straigth-forward):

MORSE_CODE_DICT = { 'A':'12', 'B':'2111', 
                    'C':'2121', 'D':'211', 'E':'1', 
                    'F':'1121', 'G':'221', 'H':'1111', 
                    'I':'11', 'J':'1222', 'K':'212', 
                    'L':'1211', 'M':'22', 'N':'21', 
                    'O':'222', 'P':'1221', 'Q':'2212', 
                    'R':'121', 'S':'111', 'T':'2', 
                    'U':'112', 'V':'1112', 'W':'122', 
                    'X':'2112', 'Y':'2122', 'Z':'2211'}


# Input vocabulary converter to number
def converter(vocabulary):
    for i in range(len(vocabulary)):
        var = ""
        for j in vocabulary[i]:
            var = var+MORSE_CODE_DICT[j]
        vocabulary[i]=int(var)
    return vocabulary

# Create a MiniZinc model

gecode = Solver.lookup("or-tools")
model=Model()
model.add_string("""
include "globals.mzn";

int: n;
int: lmax;
array[1..n] of int: c;
int: morse;
array [1..lmax] of var 1..n: frase; 
var int: r;
array [1..n] of var int: len;
array [1..lmax] of var int: sa;

constraint forall(i in 1..n)(len[i]=string_length(mzn_version_to_string(c[i]))-4);
constraint sa[1]=c[frase[1]]; 
constraint forall(i in 2..lmax)(sa[i]=c[frase[i]]*pow(10,sum(j in 2..i)(len[frase[j-1]]))); 
constraint lmax>0 /\ lmax<100000;
constraint n>0 /\ n<100000;
constraint forall(i in len)(i>0 /\ i<20);
constraint r>=0 /\ r<pow(2,10);
constraint sum(sa) = morse;
""")

# Transform Model into a instance

inst = Instance(gecode, model)
inst["n"] = 6

vocabulary = ["HELL","HELLO","OWORLD","WORLD","TEST"]
vocabulary= np.array(converter(vocabulary))
vocabulary = np.append(vocabulary, 0)
print(vocabulary)
inst["c"] = vocabulary

morse = 11111121112112221222221211211211
inst["morse"] = morse

print(len(str(morse)));
inst["lmax"] = len(str(morse))

result = inst.solve()

How would you solve this problem? Could you give me some advice about a possible solution or different approach to the problem? I have already tried using strings rather than ints, but MiniZinc does not support them very well.

Thank you in advance to everyone.

Answer 1

Most FlatZinc solvers don't support large integers and give overlflow errors, for example when detecting operations with integers larger than 2**32. The exact limit is solver dependent.

One problem in your model is that you have a lot of domains defined as var int which yield very large domains for the solver to work with. If you try to reduce these domains as much as possible, it might work.

In the MiniZinc model, I commented some of the constraints and gave all the var int some (but probably wrong) domains which gave a solution using the OR-tools solver:

include "globals.mzn";

int: n;
int: lmax;
array[1..n] of int: c;
int: morse;

array [1..lmax] of var 1..n: frase; 
var 0..pow(2,10): r; % hakank
array [1..n] of var 0..20: len; % hakank
array [1..lmax] of var 0..100000000: sa; % hakank

% constraint forall(i in 1..n)(len[i]=string_length(mzn_version_to_string(c[i]))-4);
constraint sa[1]=c[frase[1]]; 
% constraint forall(i in 2..lmax)(sa[i]=c[frase[i]]*pow(10,sum(j in 2..i)(len[frase[j-1]]))); 
constraint lmax>0 /\ lmax<100000;
% constraint n>0 /\ n<100000;
% constraint forall(i in len)(i>0 /\ i<20);
% constraint r>=0 /\ r<pow(2,10);
constraint sum(sa) = morse;

solve satisfy;

Here is one solution which - as mentioned above - don't look correct. But you can now work with the constraints and the domains.

Solution(frase=[5, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 
         r=0, 
         len=[0, 0, 0, 0, 0, 0], 
         sa=[211112, 0, 0, 0, 0, 0, 0, 0, 0, 0, 47272535, 100000000, 100000000, 100000000, 100000000, 100000000, 100000000, 100000000, 100000000, 100000000, 100000000, 100000000, 100000000, 100000000, 100000000, 100000000, 100000000, 100000000, 100000000, 100000000, 100000000, 100000000],    
         _checker='')