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.

1) Exactly how do you translate the ,mzn file to .fzn? Are you including Picat's global definitions when doing this? 2) How do you get a sat solver to generate all solutions? — hakank, Aug 18 '20 at 20:28
@hakank: [cryptominisat](https://www.msoos.org/cryptominisat5/) has a `--maxsol` option to enumerate solutions. Otherwise, one could add a clause with all inverted literals of the solution to forbid this solution to be found again. — Axel Kemper, Aug 18 '20 at 21:59
Could it be that the Picat translation adds auxiliary variables, and the resulting solutions differ only in these auxiliary variables? — Axel Kemper, Aug 18 '20 at 22:07
One way to do to enumerate all solutions is exactly as @AxelKemper says and use --maxsol of cryptominisat. Many (if not all) of SAT solvers will have an option like this. — Exeloz, Aug 19 '20 at 02:49
@hakank I answered to the second question with my previous comment. For the first question, as specified in the question, I use mzn2fzn, wich seems to be a know tool since it is mentionned in the file fzn_picat_sat.pi. And if I'm not mistaken, you are part of the team that made this module possible, therefore I hope what I say is understandable. — Exeloz, Aug 19 '20 at 02:53
@AxelKemper Maybe Picat adds auxilary variables that changes the number of solutions. But I can give multiple example very similar to the one above where the resulting CNF works just fine and gives the expected number of solutions. Maybe I misunderstand some things about all this, it is very possible. But even with added variables, I would hope I'd get the expected number of solutions. So, if this is the case, is there any way to know which variables should be removed when I'm counting the solutions? — Exeloz, Aug 19 '20 at 02:58
@AxelKemper Thanks for the tip about cryptominisat. The SAT solvers I tested (minisat, lingeling, glucose) don't support all solutions what I know. I also found bc_minisat_all. — hakank, Aug 19 '20 at 05:29
@Exeloz The reason `fzn_interpretation_error` is thrown is because fzn_picat_sat try to translate an MiniZInc output variable to CNF, but that requires that the variables are instantiated and this is not the case when using `[dump]`. I'm not sure if this influence the rest of the translation. Though I tested with a simple 8 queens model and got 288 solutions instead of 92 so something is strange. Can you link to a MiniZinc model were you get the correct solution with a SAT solver? — hakank, Aug 19 '20 at 05:36
@hakank Actually, I can. I did test the 8-queens using non binary variables in the Minizinc file. Here is a simple [mzn file](https://www.dropbox.com/s/2dezd1qu668j2kr/nqueens-int.mzn?dl=0), and the corresponding [fzn](https://www.dropbox.com/s/lb0tt9ly1nsrv0r/nqueens-int.fzn?dl=0), and the corresponding [CNF](https://www.dropbox.com/s/wmhcyug7pu0mcbt/nqueens-int.cnf?dl=0) given by Picat having 92 solution. — Exeloz, Aug 19 '20 at 12:52
@Exeloz Thanks for the queens model. I can confirm that the CNF version yield 92 solutions. However, the CNF for this model (http://hakank.org/minizinc/queens4,mzn ) (using `all_different` constraints) give 288 solutions. It seems that the all_different constraint give some extra internal variables. — hakank, Aug 19 '20 at 14:38
@Exeloz Regarding the `fzn_interpretation_error`: If you comment out the calls to `fzn_output` in the Picat program, the error message should go away. — hakank, Aug 19 '20 at 14:41
@hakank Regarding the error, thank you for the tip. As for the queen model, I agree my model was sub-optimal in many ways as I did not use any global constraint. I tried to avoid this constraints since the header of fzn_picat_sat.pi warns that alldifferent/1 should not be decomposed by mzn2fzn. I would like to also point out that I do not use any global constraints in Sequence.mzn linked in the the question. So even if alldifferent/1 give some extra internal variables, I do not understand about Sequence.mzn. But there is definitely something going on here — Exeloz, Aug 19 '20 at 14:48
@Exeloz I think Mikael's answer is on the spot regarding internal variables. In the Sequence case there is a lot of extra variables created in the FlatZinc file (the one with `var_is_introduced`), though the FlatZinc solvers only outputs solutions where the variables tagged as `output_array` are different. I don't know how to avoid handling the internal variables in the CNF file (well, they are part of the model so they should be included in the model) or identify them in some intelligent way. — hakank, Aug 19 '20 at 15:03
@hakank Fair enough, it does make a lot of sense, thats for sure. But I do hope to find a tool that could do the job, but that will be for another question, eventually. — Exeloz, Aug 19 '20 at 15:08
Let us [continue this discussion in chat](https://chat.stackoverflow.com/rooms/220099/discussion-between-hakank-and-exeloz). — hakank, Aug 19 '20 at 15:21

score 3 · Accepted Answer · answered Aug 19 '20 at 05:38

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).

Actually, I have [tools to only consider a subset of variables](https://github.com/meelgroup/ganak) when counting the solutions. (This is not offered in a solver that I know of). So, if there was a way to know what variables are the output variables, I'd be able to do whatever I'm trying to do. Do you know of any way to do this? Thanks for the explanation by the way. — Exeloz, Aug 19 '20 at 12:55
This answers makes sense and with a very compelling model. I appreciate the time you took. I will accept this answer and still hope to find a way to pick the right variables while doing the counting. — Exeloz, Aug 19 '20 at 15:10
Thanks. As I have never used Picat myself, I can't help you with that. — Zayenz, Aug 20 '20 at 06:17
@Exeloz output variables are conveniently marked as such with an annotation in the FlatZinc file that is generated by the mzn2fzn compiler (or minizinc). You can check Picat parser to find out whether it retains those tags. If not, you can create internal data structures to remember them and then use them as it pleases you. — Patrick Trentin, Aug 31 '20 at 16:31

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

1 Answers1