为什么picat说这个模型是不可满足的？

Question

picat解决程序(v. 2.6#2)指出，包含在minizinc存储库中的示例模型knights.mzn，在此复制和粘贴：

% 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 (v. 2.2.1)的fzn2smt (v.2.2.1)外，其他每一个求解器都告诉我，该模型是可满足的。

Q:，这是软件中的一个bug，还是一个不受支持的公式的样本？

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应该提供更好的错误消息，例如“不支持set变量”。

注意，许多FlatZinc求解器不支持set变量。例如，Chuffed在模型上抛出了一条很好的消息：

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

本机不支持set变量的解决程序可以包含标准库中的nosets文件。此文件将确保将所有set变量转换为多个布尔变量。理想情况下，该文件将包含在求解器MiniZinc redefinitions.mzn文件中，但始终可以通过添加以下行从模型中直接包含该文件：

include "nosets.mzn";