How to use Picat to create CNF files from Minizinc files?

Question

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.

Answer 1

As mentioned in the comments by Axel Kemper, MiniZinc may add additional variables that should not be used to differentiate multiple solutions. As a simple example, consider the following (artificial) MiniZinc model

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;

Here the predicate separated adds another variable that is just used as a witness that there is some number between x and y (the predicate is equivalent to abs(x-y)>0).

The model has 36 solutions (1,3, 1,4, ..., 8,10). However, if you consider the solution 3,8, there are 5 different choices of z that makes the predicate true. In general, a user is most likely only interested in solutions that differ in the output variables.

When translating the above MiniZinc to CNF the predicate internal z-variable will not be distinguished from the "real" problem variables x and y. For counting the solutions, you would need to distinguish the literals that correspond to the domains of output variables in the model, and to instruct the SAT solver to only consider two solutions different if those literals are different (not sure if that is a feature that is available).