标签: picat

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

该picat解算器（诉2.6#2）指出，示例性的模型knights.mzn包含在minizinc存储库，并在此复制和粘贴：

% RUNS ON mzn20_fd
% RUNS ON mzn-fzn_fd
% RUNS ON mzn20_mip
% knights.mzn
% Ralph Becket
% vim: ft=zinc ts=4 sw=4 et
% Tue Aug 26 14:24:28 EST 2008
%
% Find a closed knight's tour of a chessboard (every square is visited exactly
% once, the tour forms a loop).

include "globals.mzn";

    % n is the length of side of the chessboard.
    %
int: n = 6;

    % The ith square …