如何使用 Picat 从 Minizinc 文件创建 CNF 文件？

Question

我有兴趣计算一个问题的解决方案数量（不列举解决方案）。为此，我有使用CNF文件的工具。我想转换Minizinc文件（mzn 或 Flatzinc fzn 格式）并将其转换为 CNF。

我了解到Picat能够在加载约束后“转储”CNF 文件。此外，Picat 有一个聪明的模块来解释基本的 Flatzinc 文件。我修改了模块fzn_picat_sat.pi以“转储”CNF 文件。所以，我所做的是使用 mzn2fzn 将 Minizinc 文件转换为 Flatzinc，然后尝试使用我的（稍微）修改过的 fzn_picat_sat.pi版本将其转换为 CNF 。

我想要什么：我希望 Picat 加载 Flatzinc 文件并转储适当的 CNF 文件。如果原来的问题有X个解，我期望对应的CNF有X个解。

会发生什么：我尝试过的大多数 Flatzinc 文件都运行良好。但有些似乎会产生不需要的结果。例如，下面的 mzn转换为这个 Flatzinc 文件。该文件只有 211 个解决方案，但Picat转储的CNF 文件有超过 130k 个解决方案。许多 SAT 求解器可以显示 CNF 文件有超过 211 个解（例如带有选项的cryptominisat--maxsol）。奇怪的是，当我要求 Picat 解决 Flatzinc 文件而不转换为 CNF 时，Picat 确实只找到了 211 个解决方案。问题似乎出在翻译的某个地方。最后，即使 CNF 文件有很多使用 Picat 的解决方案，我也会收到错误% fzn_interpretation_error。

如果有人尝试过类似的方法并成功，或者有人知道如何从 CP（约束编程）语言转换为 CNF，那将不胜感激。谢谢大家。

Answer 1

正如 Axel Kemper 在评论中提到的，MiniZinc 可能会添加不应用于区分多个解决方案的其他变量。作为一个简单的示例，请考虑以下（人工）MiniZinc 模型

predicate separated(var int: x, var int: y) = 
    let {
      var int: z
    } in
     x < z /\ z < y;
     
var 1..10: x;
var 1..10: y;

constraint separated(x, y);

solve satisfy;

这里谓词separated添加了另一个变量，该变量仅用作 x 和 y 之间存在某个数字的见证（谓词相当于abs(x-y)>0）。

该模型有 36 个解 ( 1,3, 1,4, ..., 8,10)。然而，如果考虑解决方案3,8，则 z 有 5 种不同的选择可以使谓词为真。一般来说，用户很可能只对输出变量不同的解决方案感兴趣。

将上述 MiniZinc 转换为 CNF 时，谓词内部 z 变量将无法与“真实”问题变量 x 和 y 区分开来。为了计算解决方案，您需要区分与模型中输出变量的域相对应的文字，并指示 SAT 求解器仅在这些文字不同时才考虑两个不同的解决方案（不确定这是否是一个功能）可用）。