title: How to use Picat to create CNF files from Minizinc files?
body: <p>I'm interested in counting the number of solutions a problem have (not enumerating the solutions). For that, I have tools that uses <a href="https://people.sc.fsu.edu/%7Ejburkardt/data/cnf/cnf.html" rel="nofollow noreferrer">CNF</a> files. I want to convert <a href="https://www.minizinc.org/" rel="nofollow noreferrer">Minizinc</a> files (mzn or Flatzinc fzn format) and convert it to CNF.</p>
  <p>I learned <a href="http://picat-lang.org/" rel="nofollow noreferrer">Picat</a> has the ability to &quot;dump&quot; a CNF file after loading the constraints. Moreover, Picat has a clever Module that interprets basic Flatzinc files. I modified the module <a href="http://picat-lang.org/flatzinc/fzn_picat_sat.pi" rel="nofollow noreferrer">fzn_picat_sat.pi</a> to &quot;dump&quot; 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) <a href="https://www.dropbox.com/s/jc3pxn9m2l2v1sa/fzn_picat_sat.pi?dl=0" rel="nofollow noreferrer">modified version</a> of fzn_picat_sat.pi.</p>
  <p>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.</p>
  <p>What happens : Most Flatzinc files I tried worked just fine. But some seem to give unwanted results. For example, <a href="https://www.dropbox.com/s/pu0zo6blbtbzxzh/Sequence.mzn?dl=0" rel="nofollow noreferrer">the following mzn</a> translate to <a href="https://www.dropbox.com/s/l0leaq02ne58nxu/Sequence.fzn?dl=0" rel="nofollow noreferrer">this Flatzinc file</a>. That file has only 211 solutions, but the <a href="https://www.dropbox.com/s/y5khzpdzz17l8zs/Sequence.cnf?dl=0" rel="nofollow noreferrer">CNF file dumped</a> by Picat has over 130k solutions. Many SAT solvers can show that the CNF file has over 211 solutions (for example <a href="https://www.msoos.org/cryptominisat5/" rel="nofollow noreferrer">cryptominisat</a> with the option <code>--maxsol</code>). 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 <code>% fzn_interpretation_error</code>.</p>
  <p>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.</p>