5

I'm interested in counting the number of solutions a problem have (not enumerating the solutions). For that, I have tools that uses CNF files. I want to convert Minizinc files (mzn or Flatzinc fzn format) and convert it to CNF.

I learned Picat has the ability to "dump" a CNF file after loading the constraints. Moreover, Picat has a clever Module that interprets basic Flatzinc files. I modified the module fzn_picat_sat.pi to "dump" the CNF file. So, what I do is that I convert a Minizinc file to Flatzinc using mzn2fzn, then I try to convert it to CNF using my (slightly) modified version of fzn_picat_sat.pi.

What I want : I expect Picat to load the Flatzinc files and dump an appropriate CNF file. If the original problems has X solutions, I expect the corresponding CNF to have X solutions.

What happens : Most Flatzinc files I tried worked just fine. But some seem to give unwanted results. For example, the following mzn translate to this Flatzinc file. That file has only 211 solutions, but the CNF file dumped by Picat has over 130k solutions. Many SAT solvers can show that the CNF file has over 211 solutions (for example cryptominisat with the option --maxsol). Weirdly, when I ask Picat to solve the Flatzinc file without translating to CNF, Picat does find only 211 solutions. The problem seems to be somewhere in the translation. Finally, even if the CNF file has the good number of solutions using Picat, I do receive an error % fzn_interpretation_error.

If anyone tried something like that and succeeded, or if anyone knows how to translate from a CP (constraint programming) language to CNF, that would be much appreciated. Thanks everyone.

4

1 回答 1

3

正如 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 求解器仅在这些文字不同时才考虑两个不同的解决方案（不确定这是否是可用）。

于 2020-08-19T05:38:23.480 回答