parsing - 解决 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(非确定性)变体。

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