解决 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, which is described in http://hakank.org/minizinc/crossword3/。

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

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

请注意，MiniZinc 和 Picat - 以及大多数其他 CP 系统 - 支持使用 DFA（确定性有限自动机）创建约束的全局约束 "regular"。参见例如 Nonogram 求解器：http://hakank.org/minizinc/nonogram_create_automaton2.mzn and the decomposition of the global contiguity constraint: http://hakank.org/minizinc/contiguity_regular.mzn

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

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

解决 MiniZinc 中的字符串约束

Solving string constraints in MiniZinc

parsing

minizinc