MiniZinc with Picat

[Jakob Baumann]

Hello all,

i wanted to replay some benchmarks from the MiniZinc Challenge with OR-Tools and PicatSAT. I added OR-Tools successfully to the MiniZinc IDE (via Preferences-> add solver), but failed so far doing the same with PicatSAT. An existence_error is thrown, so i guess im missing some packages. Which Picat packages do i need, and where do i get them? Any recommendations?

Thanks a lot

Jakob

(this might be a repost from my 1st post in this group, but that one is still held back for moderation since 4 days apparently, sorry for inconvenience)

[Hakan Kjellerstrand]

For working with Picat as a FlatZinc solver you must first install Picat from http://picat-lang.org/ . The specific flatzinc parser is also necessary and

I recommend that you download the GitHub version: https://github.com/nfzhou/fzn_picat  .

Placed (copy/link) the directory "mzn_lib" at your favorite place of global definitions (e.g.  in share/minizinc). I've called the directory picat_sat (used in the msc file shown below).

The program fzn_picat.sat.pi must be run by Picat and it seems that MiniZinc require just a single executable in the "exexutable" option so I have written a small executable shell script (called run_picat_sat.sh ) that runs the PicatSAT solver (it's a Linux script so you might have to adjust it if using some other environment):

""""

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

"""

The configuration file (picat_sat.msc) is then defined as:

{ "id": "picat_sat",

  "name": "picat_sat",

  "description": "Picat FlatZinc solver",

  "version": "3.1",

   "mznlib": "-Gpicat_sat",

   "executable": ""executable": "/path/to/run_picat_sat.sh"",

    "tags": ["sat","int"],

    "stdFlags": ["-a","-n","-f"],

    "supportsMzn": false,

    "supportsFzn": true,

    "needsSolns2Out": true,

    "needsMznExecutable": false,

     "needsStdlibDir": false,

     "isGUIApplication": false

}

If you place this file together with the other msc files (e.g. share/minizinc/solvers/) then MiniZincIDE should show the PicatSAT as a solver automatically.

Hope this helps.

/Hakan

[Jakob Baumann]

Hi Hakan,

thanks a lot for your help. I managed to add the solver configuration as you described, at least I'm able now to call a solver using "minizinc --solver <solver ID> <Model>.mzn" in command prompt or in the dropdown solver selection in the MiniZincIDE. As I'm on Windows, I made a "run_picat_sat.cmd" instead of a "run_picat_sat.sh" file and of course changed the path to a "windows-style". (Also, in the .msc file, I assume the double "executable": ""executable": is a typo, as it only works with one "executable":. )

However, when I try to solve a model using command prompt or MiniZincIDE, I get a "Undefined procedure: main/0" error. I'm using the cygwin-version of picat, as the executable (picat.exe for Windows) is missing in the github version. Might that be a reason?

And what does "mznlib":"-Gpicat_sat" reference to? Shouldn't it be the path where I placed the "mznlib" folder from the flatzinc parser? (I tested both ways, same error "undefined procedure: main/0")

Greetings

Jakob

[Hakan Kjellerstrand]

* Exactly how do you run the program with "run_picat_sat.sh" and what is the content of the program?

   What happens if you run fzn_picat_sat.pi directory from command line:

     $ /path/to/picat.exe /path/to/fzn_picat_sat.pi

   ?

   It should give a usage message of fzn_picat_sat.pi

* The "mzn_lib:-Gpicat_sat" is the place of the directory of the definitions for the global constraints.

   As mentioned earlier:: Place (copy/link) the directory "mzn_lib" at your favorite place of global definitions (e.g.  in share/minizinc). I've called the directory "picat_sat" (used in the msc file shown below).

   (And yes, two "executable" in the .msc is a typo.)

Hope this helps

/Hakan

--
You received this message because you are subscribed to the Google Groups "MiniZinc" group.
To unsubscribe from this group and stop receiving emails from it, send an email to minizinc+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/minizinc/aa30fe8d-867d-46cf-ba79-94b3aeec1461n%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

[Jakob Baumann]

I set Picat as Path Variable in Windows, therefore the content of my "run_picat_sat.cmd" was just
<picat "C:\Program Files\MiniZinc\share\minizinc\picat_sat\fzn_picat_sat.pi"> ("" because of blank spaces in path).
Getting into more detail on the error "*** Undefined procedure: main/0" I realised, that an argument (here: a flatzinc file) needs to be passed.
I then realised, that your .sh file actually has a placeholder for arguments ($*). Orignally, I thought this is an EOF, because I'm not that familiar with Linux.
Therefore my updated .cmd is:

<picat "C:\Program Files\MiniZinc\share\minizinc\picat_sat\fzn_picat_sat.pi" %*> ("" because of blank spaces in path).

Now it works just fine..., however, only if I set "needsSolns2Out" in the solver configuration file to false, as it returns "solns2out_base: could not parse solution" otherwise.
Well, I can live with those not so nice formatted solutions - unless you know a quick fix for that :)

So thank you a lot for your help. I also appreciate all those example models you provided on your webpage!
Greetings
Jakob

[Hakan Kjellerstrand]

Glad that it - kind of - works now.

Regarding the solns2out error message, MiniZinc can be a little picky when parsing the output from a FlatZinc parser. All output that is not in the proper solution, e.g. debug output or show the path of the files etc, must be prepended with a "%" (comment) character.  

What is the exact output when you run the same Picat command from the command line for a simple model, e.g. http://www.hakank.org/minizinc/send_more_money.mzn   ?

/Hakan

To view this discussion on the web visit https://groups.google.com/d/msgid/minizinc/1063e329-3cd5-404d-bb04-de9bf03e9274n%40googlegroups.com.