如何避免MiniZinc中的整数溢出？

Question

我试图解决一个代码游戏，从codingame网站使用MiniZinc的Python。我所要做的就是在一个莫尔斯代码中找到可能组合的数目，给出一个词汇表(一组可能的单词，经过转换和连接，应该精确地等于输入的莫尔斯代码)。我已经能够很快地找到一个解决方案，但问题是，无论我使用哪一个求解器，我都会得到一个整数溢出。我试着使用OptiMathSAT，但是我无法应用它。

在这里，您可以找到我的代码(您将找不到可能的组合的计数，但我认为它将是倾斜的)：

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()

你将如何解决这个问题？你能给我一些关于这个问题可能的解决方案或不同方法的建议吗？我已经尝试过使用字符串而不是int，但是MiniZinc并不很好地支持它们。

提前谢谢大家。

Answer 1

大多数FlatZinc求解器不支持大整数，并给出重叠流错误，例如，当检测大于2**32的整数操作时。精确的极限取决于求解者。

模型中的一个问题是，有许多域被定义为var int，这为求解者提供了非常大的处理域。如果您试图尽可能地减少这些域，它可能会工作。

在MiniZinc模型中，我注释了一些约束，并为所有var int提供了一些(但可能是错误的)域，这些域提供了一个使用OR工具求解器的解决方案：

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;

这里有一个解决方案--正如上面提到的--看起来不正确。但是现在您可以使用约束和域。

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='')