minizinc - 为什么picat说模型不满足？

Question

picat求解器 (v. 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 (r, c) on the path is given by p[i] = (r - 1) * n + c.
    %
int: nn = n * n;
set of int: sq = 1..nn;
array [sq] of var sq: p;

set of int: row = 1..n;
set of int: col = 1..n;

    % Break some symmetry by specifying the first and last moves.
    %
constraint p[1]  = 1;
constraint p[2]  = n + 3;
constraint p[nn] = 2 * n + 2;

    % All points along the path must be unique.
    %
constraint alldifferent(p);

array [sq] of set of sq: neighbours =
    [   { n * (R - 1) + C
        |
            i in 1..8,
            R in {R0 + [-1, -2, -2, -1,  1,  2,  2,  1][i]},
            C in {C0 + [-2, -1,  1,  2,  2,  1, -1, -2][i]}
            where R in row /\ C in col
        }
    |   R0 in row, C0 in col
    ];

constraint forall (i in sq where i > 1) (p[i] in neighbours[p[i - 1]]);

solve
    :: int_search(
        p,
        input_order,
        indomain_min,
        complete
    )
    satisfy;
% It has been observed that Warnsdorf's heuristic of choosing the next
% square as the one with the fewest remaining neighbours leads almost 
% directly to a solution.  How might we express this in MiniZinc?

output ["p = " ++ show(p) ++ ";\n"];

% Invert the path to show the tour.
% 
% array [sq] of var sq: q;
% 
% constraint forall (i in sq) (q[p[i]] = i);
% 
% output  [   show(q[i]) ++ if i mod n = 0 then "\n" else " " endif
%         |   i in sq
%         ] ++
%         [   "\n"
%         ];

不满意:

~$ mzn2fzn knights.mzn
~$ picat tools/picat/fzn_picat_cp.pi knights.fzn
% solving(knights.fzn)
% loading knights.fzn
=====UNSATISFIABLE=====

~$ mzn2fzn knights.mzn
~$ picat tools/picat/fzn_picat_sat.pi knights.fzn
% solving(knights.fzn)
% loading knights.fzn
=====UNSATISFIABLE=====

每隔 MiniZinc求解器，除了 fzn2smt基于 Yices (v. 2.2.1)，告诉我模型是可满足的。

问:这是软件中的错误还是不受支持的公式样本？

Answer 1

Picat 在这个模型上失败的原因是它 - 或者更确切地说是生成的 FlatZinc 模型 - 包含“var set”变量(见下文)，而这些变量在 Picat 中不受支持。

var set of 1..36: X_INTRODUCED_36_ ::var_is_introduced :: is_defined_var;
var set of 1..36: X_INTRODUCED_38_ ::var_is_introduced :: is_defined_var;
var set of 1..36: X_INTRODUCED_39_ ::var_is_introduced :: is_defined_var;

理想情况下，Picat 应该给出更好的错误信息，例如“不支持设置变量”。

请注意，许多 FlatZinc 求解器不支持设置变量。例如，Chuffed 在模型上抛出这个好消息:

Error: LazyGeoff: set variables not supported in line no. 72

本身不支持设置变量的求解器可以包括 nosets标准库中的文件。该文件将确保所有设置的变量都被转换为多个 bool 变量。理想情况下，此文件将包含在求解器 MiniZinc redefinitions.mzn 中文件，但您始终可以通过添加以下行直接从模型中包含此文件:

include "nosets.mzn";