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

问题描述

我有兴趣计算问题的解决方案数量（不列举解决方案）。为此，我有使用CNF文件的工具。我想转换Minizinc文件（mzn或Flatzinc fzn格式）并将其转换为CNF。

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

我想要的是：我希望Picat可以加载Flatzinc文件并转储适当的CNF文件。如果原始问题有X解决方案，我希望相应的CNF也有X解决方案。

会发生什么：我尝试过的大多数Flatzinc文件都运行良好。但是有些似乎给出了不想要的结果。例如，the following mzn转换为this Flatzinc file。该文件只有211个解决方案，但是Picat的CNF file dumped有13万多个解决方案。许多SAT求解器可以显示CNF文件具有211种以上的解决方案（例如，cryptominisat，选项为--maxsol）。奇怪的是，当我要求Picat在不转换为CNF的情况下解决Flatzinc文件时，Picat确实只找到211个解决方案。问题似乎在翻译中。最后，即使使用Picat的CNF文件有很多解决方案，我也会收到错误% fzn_interpretation_error。

如果有人尝试过这种方法并成功了，或者有人知道如何将CP（约束编程）语言转换为CNF，那将不胜感激。谢谢大家。

解决方法

如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，则z的5种不同选择可以使谓词成立。通常，用户最可能只对输出变量不同的解决方案感兴趣。

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