我有兴趣计算一个问题的解决方案数量（不列举解决方案）。为此，我有使用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 的解决方案，我也会收到错误 …