PicatSat - getting started

[Martin Lester]

Hello.

I want to use PicatSat on some MiniZinc models in CSPLib, such as this one:

https://www.csplib.org/Problems/prob003/models/quasiGroup3NonIdempotent.mzn.html

Which versions of Picat, PicatSat and MiniZinc should I use?

For PicatSat in particular, there are 4 .pi files and a tarball here under the heading MiniZinc Challenge:

http://picat-lang.org/projects.html

But also a GitHub repository here, which seems similar but looks more up-to-date and has some instructions:

https://github.com/nfzhou/fzn_picat

I downloaded pre-compiled MiniZinc 2.6.3 (version matching MiniZinc Challenge 2022) and cloned the above repo. Then I ran:

./bin/minizinc --solver mzn-fzn -I /path/to/fzn_picat/mznlib/ /path/to/prob003/quasiGroup3NonIdempotent.mzn

and got:

Error: error: No FlatZinc solver specified

Indeed, the current version of MiniZinc doesn't list mzn-fzn as a solver. But it does have a compile-only option, -c, so I tried:

./bin/minizinc -c -I /path/to/fzn_picat/mznlib/ /path/to/prob003/quasiGroup3NonIdempotent.mzn

Which seemed to work. Then I tried to solve it with Picat 3.3#3:

../Picat/picat ../fzn_picat/fzn_picat_sat.pi /path/to/prob003/quasiGroup3NonIdempotent.fzn

and got an error:

% solving(/path/to/prob003/quasiGroup3NonIdempotent.fzn)
% loading /path/to/prob003/quasiGroup3NonIdempotent.fzn
% unsupported_constraint(fzn_all_different_int({_3c10,_3c18,_3c20,_3c28}))

The all-different constraint is pretty common, so I doubt PicatSat doesn't support it.

Maybe MiniZinc can't find PicatSat's definition of how to flatten it? I noticed that mznlib/ has a file called redefinitions.mzn, which I guess is instructing MiniZinc which constraints it provides its own implementations of. It looks like recent versions of MiniZinc have renamed that solver_redefinitions.mzn. If I rename redefinitions.mzn to that, and try recompiling with MiniZinc, I get a different error:

Error: type error: no function or predicate with name `fzn_array_int_union' found
/path/to/MiniZincIDE-2.6.3-bundle-linux-x86_64/share/minizinc/std/stdlib/stdlib_array.mzn:224.18-42

My guess is that there have been some changes between versions of MiniZinc, Picat and PicatSat that have introduced incompatibilities. So which versions should I use (or what else should I try)?

Yours,

Martin Lester.

[Hakan Kjellerstrand]

Hi Martin.

Here is how I use MiniZinc with the PicatSAT solver at https://github.com/nfzhou/fzn_picat . It's a little messy  but I think it's worth it. After you've done these steps you will be able to run MiniZinc as:

  $ minizinc quasiGroup3NonIdempotent.mzn --solver picat_sat

or in general

  $ minizinc model.mzn data.dzn -a -s --solver picat_sat

Using this, the minizinc program automatically translates the MiniZinc model to FlatZinc using the global constraints dedicated to PicatSAT.

You have already done some of the steps already but I want to describe the steps in full.

Here's the step:

1) Check out the PicatSAT solver from https://github.com/nfzhou/fzn_picat

2) Create a .msc definition file for PicatSAT

    Here is my own picat_sat.msc

"""

{
  "id": "picat_sat",
  "name": "picat_sat",
  "description": "Picat FlatZinc solver command line",
  "version": "3.3#3",
  "mznlib": "-Gpicat_sat",
  "executable": "/home/hakank/g12/picat/run_picat_sat.sh",
  "tags": ["cp","int"],
  "stdFlags": ["-a","-n","-p","-r"],
  "supportsMzn": false,
  "supportsFzn": true,
  "needsSolns2Out": true,
  "needsMznExecutable": false,
  "needsStdlibDir": false,
  "isGUIApplication": false
}

"""

  This file should be placed together with the other .msc files (gecode.msc, chuffed.msc etc), i.e.  in the directory

      <minizinc_installation>/share/minizinc/solvers/

   See below for comments on "mznlib" and "executable".

   * Copy/link the directory mznlib (i.e. https://github.com/nfzhou/fzn_picat/tree/main/mznlib) in a directory called picat_sat that MiniZinc can find. 

    This library contains PicatSAT's definitions of the global constraints (all_different etc). Without it the default MiniZinc definitions are used which tends to be slower than the dedicated PicatSAT definitions.

    I place this directory in the same directory that contains the directory ./gecode, ./chuffed in the MiniZinc installation. This should be the directory <minizinc_installation>/share/minizinc/

 

  The line

     "mznlib": "-Gpicat_sat",

   means that MiniZinc will check for the PicatSAT's definitions of the supported global constraints in the directory <minizinc_installation>/share/minizinc/picat_sat (it also checks some other directories but let's keep it simple).

 * Create a program/script that calls Picat and the fzn solver program

   The reason for having a separate program for calling the Picat program fzn_picat_sat.pi is that MiniZinc tends to give strange error messages if the "executable" entry is defined like this:

        "executable": "picat /home/hakank/picat/git/nfz/fzn_picat/fzn_picat_sat.pi",   

   (replace the path to fzn_picat_sat.pi ).

   At my Linux computer(s) I have the program /home/hakank/g12/picat/run_picat_sat.sh which simply includes this line

       picat /home/hakank/picat/git/nfz/fzn_picat/fzn_picat_sat.pi $*

   

   The program/script should be executable and the path stated the "executable" flag in the .mcs file, e.g.

      "executable": "/home/hakank/g12/picat/run_picat_sat.sh",  

      

Hopefully this is enough to use PicatSAT as a FlatZinc solver:

$ minizinc model.mzn --solver picat_sat

(And if you want some other MiniZinc models to play with, see my MiniZinc page: http://hakank.org/minizinc/)

Hope this helps,

Hakan

--
You received this message because you are subscribed to the Google Groups "Picat" group.
To unsubscribe from this group and stop receiving emails from it, send an email to picat-lang+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/picat-lang/926ea352-7611-4955-8c19-71334c246a7an%40googlegroups.com.

--

Hakan Kjellerstrand
http://www.hakank.org/
http://www.hakank.org/webblogg/
http://www.hakank.org/constraint_programming_blog/
http://twitter.com/hakankj
https://www.facebook.com/hakankj

[Neng-Fa Zhou]

I just updated the latest version of the fzn interpreter.

https://github.com/nfzhou/fzn_picat/blob/main/fzn_picat_sat.pi

You need the latest version of Picat to run this interpreter.  I also restored the file "redefinitions.mzn" so that the default definitions for implication constraints are used.

Cheers,

NF