如何使用Picat从Minizinc文件创建CNF文件？

Question

我感兴趣的是计算一个问题的解决方案的数量(不是枚举解决方案)。为此，我有使用CNF文件的工具。我想转换Minizinc文件(mzn或Flatzinc格式)，并将其转换为CNF。

我了解到Picat能够在加载约束后“转储”CNF文件。此外，Picat有一个聪明的模块，可以解释基本的Flatzinc文件。我修改了模块fzn_picat_sat.pi以“转储”CNF文件。所以，我所做的就是使用mzn2fzn将迷你文件转换为Flatzin型文件，然后尝试使用我的(稍微) fzn_picat_sat.pi的modified version将其转换为CNF。

我想要的:我希望Picat能加载Flatzinc文件并转储一个合适的CNF文件。如果原始问题有X个解，我希望相应的CNF也有X个解。

结果:我尝试过的大多数Flatzin型文件都工作得很好。但有些人似乎给出了不想要的结果。例如，the following mzn translate to this Flatzinc file。该文件只有211个解决方案，但Picat的CNF file dumped有超过130k的解决方案。许多SAT求解器可以显示CNF文件有超过211个解决方案(例如，带有选项--maxsol的cryptominisat )。奇怪的是，当我要求Picat在不转换为CNF的情况下解决Flatzinc文件时，Picat确实只找到了211个解决方案。问题似乎出在翻译中的某个地方。最后，即使CNF文件有大量使用Picat的解决方案，我也会收到一个错误% fzn_interpretation_error。

如果有人尝试过这样的东西并获得成功，或者有人知道如何从CP (约束编程)语言转换成CNF，那将是非常感谢的。谢谢大家。

Answer 1

正如Axel Kemper在评论中提到的，MiniZinc可能会添加不应用于区分多个解决方案的其他变量。作为一个简单的例子，考虑下面的(人工) MiniZinc模型

predicate separated(var int: x, var int: y) = 
    let {
      var int: z
    } in
     x < z /\ z < y;
     
var 1..10: x;
var 1..10: y;

constraint separated(x, y);

solve satisfy;

这里，谓词separated添加了另一个变量，该变量只是用来证明x和y之间存在某个数字(该谓词等同于abs(x-y)>0)。

该模型有36个解决方案(1,3，1,4，...，8,10)。但是，如果您考虑解决方案3,8，那么有5种不同的z选择可以使谓词为真。通常，用户很可能只对输出变量不同的解决方案感兴趣。

在将上述MiniZinc转换为CNF时，谓词内部z变量将不会与“真实”问题变量x和y区分开来。为了计算解决方案，您需要区分与模型中输出变量的域相对应的文字，并指示SAT求解器仅在这些文字不同的情况下考虑两个不同的解决方案(不确定这是否是可用的功能)。