解决 MiniZinc 中的字符串约束

Question

我尝试在 MiniZinc 中使用字符串连接运算符定义约束，求解变量a和b：

include "disjunctive.mzn";

var string:a;
var string:b;
constraint("var1/var2" = (a ++ "/" ++ b));

solve satisfy;
output ["\nx=", show(a)];

尽管如此，这似乎是一个语法错误：

MiniZinc: type error: type error in operator application for `++'. No matching operator found with left-hand side type `string' and right-hand side type `var string'

是否仍然可以用字符串或数组作为变量来解决 MiniZinc 中的约束？

Answer 1

直接对字符串进行约束在约束编程社区中非常罕见。虽然我还没有看到任何支持字符串变量的通用 CP 系统，但这方面已有一些研究。（非通用 CP 系统见下文。）

在MiniZinc中，最好将字符串转换为整数（例如a=1、b=2等），然后将所有操作模拟为整数操作。

一个简单的例子是填字游戏生成器：http://hakank.org/minizinc/crossword3/crossword3.mzn，http : //hakank.org/minizinc/crossword3/中对此进行了描述。

一个重要的字符串操作是两个字符串的连接，但由于 MiniZinc 仅支持静态（固定长度）数组，因此必须通过定义足够大的“目标数组”来处理。

关于Picat，cp/sat 模块也不支持字符串，因此必须应用相同的整数转换。但由于 Picat 是一种逻辑编程语言（例如 Prolog），因此可以使用传统的逻辑编程方法。

请注意，MiniZinc 和 Picat - 以及大多数其他 CP 系统 - 支持全局约束“常规”，它使用 DFA（确定性有限自动机）来创建约束。例如，参见 Nonogram 求解器：http://hakank.org/minizinc/nonogram_create_automaton2.mzn和全局连续性约束的分解：http://hakank.org/minizinc/contiguity_regular.mzn

MiniZinc 还支持正则约束的 NFA（非确定性）变体。

也就是说，有些系统使用一种支持字符串变量的约束求解方法，尽管据我所知，它们往往只支持字符串变量，而不支持整数、集合等的一般指令。例如，参见 Hampi (http:// people. csail.mit.edu/akiezun/hampi/）。注意：自从我检查这些专用系统以来已经有很长一段时间了。