为什么 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=====

除基于Yices（v.2.2.1）的fzn2smt 之外，其他所有MiniZinc 求解器都告诉我该模型是可满足的。

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

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 variables are not supported"。

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

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

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

include "nosets.mzn";

为什么 picat 说模型不可满足？

Why picat says that the model is unsatisfiable?

minizinc

picat