A stable way to refer to the CP-SAT solver using MiniZinc

[CervEdin]

What language and solver does this apply to?

minizinc/flatzinc backend

Describe the problem you are trying to solve.

When you call minizinc you may specify which solver you want to use, for example

minizinc --solver gecode model.mzn

which specifies to use gecode as a solver.

The identifier/tag of the or-tools solver has changed over time (as it has evolved). For example, the id used to be com.google.or-tools and now it's com.google.ortools.sat. Similarly, the tags of the solver has evolved. It used to be or-tools in addition to cp and int, but now that is dropped in favor of cpsatlp (it used to be cpsat for a while if I'm not misstaken).

The issue is that as a consumer of the solver, these changes become a breaking change on upgrade.

Describe the solution you'd like

Some kind of stable way of specifying the OR-Tools CP-SAT solver as my MiniZinc back-end.

Describe alternatives you've considered

If there was a fixed id, say com.google.ortools.sat, or if tags were added instead of replacing old tags, it wouldn't be a breaking change for us.

Additional context

Nothing. Thank you for the lovely solver.

[lperron]

Not my call :-)

The minizinc team has integrated CP_SAT and chosen the tag (com.google.ortools.sat).

I will still export cp-sat.msc with the id 'cp-sat' and the tag 'cp-sat' in OR-Tools if you want to test with an un-integrated version.

[CervEdin]

Thank you Laurent!

We install the CP-SAT solver independently of the MiniZinc project, so that's great. It's not a big deal for us, since we currently just overwrite cpsat.msc with our own solver configuration file. I'd just rather not do that, in case there are other changes, if for example the fzn flags are changed.

I'm not sure what's the most appropriate way forward here, I've been making some guesses and assumptions. Mainly about how the solver configuration files work but also which project the CP-SAT configuration file belongs to.

As a consumer of both the OR-Tools CP-SAT solver and MiniZinc is:

1. I preferably get the solver configuration file from the same place/version I get the solver
2. There's a consistent way for me to tell minizinc to use that specific solver

My assumption is that this is done by either referring to the solver by it's "name" or "tag". Of course I could simply add a tag, or change the name in the configuration file as a part of the script we use to install the CP-SAT solver. But I'm guessing there may be others out there who use both tools in a similar manner and can also benefit from a "stable" interface between the two tools.

I see that @Dekker1 added the solver configuration file back in 2020 I'm sure he can provide some valuable insight on the topic :)

[lperron]

I would use the minizinc included solver. Yes, it will be updated less often, but will be more stable.

And eventually, it will use the C++ binding and not the file based one, which will improve the whole experience. Laurent Perron | Operations Research | @.*** | (33) 1 42 68 53 00

Le lun. 3 juin 2024 à 16:45, Erik Cervin Edin @.***> a écrit :

Thank you Laurent!

We install the CP-SAT solver independently of the MiniZinc project, so that's great. It's not a big deal for us, since we currently just overwrite cpsat.msc with our own solver configuration file. I'd just rather not do that, in case there are other changes, if for example the fzn flags are changed.

I'm not sure what's the most appropriate way forward here, I've been making some guesses and assumptions. Mainly about how the solver configuration files work but also which project the CP-SAT configuration file belongs to.

As a consumer of both the OR-Tools CP-SAT solver and MiniZinc is:

1. I preferably get the solver configuration file from the same place/version I get the solver
2. There's a consistent way for me to tell minizinc to use that specific solver

My assumption is that this is done by either referring to the solver by it's "name" or "tag". Of course I could simply add a tag, or change the name in the configuration file as a part of the script we use to install the CP-SAT solver. But I'm guessing there may be others out there who use both tools in a similar manner and can also benefit from a "stable" interface between the two tools.

I see that @Dekker1 https://github.com/Dekker1 added the solver configuration file back in 2020 I'm sure he can provide some valuable insight on the topic :)

— Reply to this email directly, view it on GitHub https://github.com/google/or-tools/issues/4251#issuecomment-2145389839, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACUPL3JS65F5Q4TF7P2CAPDZFR6PPAVCNFSM6AAAAABIWHFFRSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCNBVGM4DSOBTHE . You are receiving this because you modified the open/close state.Message ID: <google/or-tools/issues/4251/2145389839 @.***>

[CervEdin]

I didn't know about MiniZinc using C++ bindings, that sounds promising.

We could use the solver bundled with the MiniZincIDE release but that would couple the releases and sometimes there are breaking changes in either project that holds us back from updating one or the other. In those situations it's useful to be able to mix and match the releases more freely.

[Dekker1]

Within the MiniZinc packages we just use the MSC file as provided by the or tools repository. It seems that the id for the solver was changed here: https://github.com/google/or-tools/commit/51564594cef289f5e9ee639c25fb1cdba801905c

The idea is that solvers can be referred to either using their full identifier + version (--solver com.google.ortools.sat@9.10), its full identifier (--solver com.google.ortools.sat), the final part of its identifier (--solver sat), or one of its tags (--solver lcg, preferences for different solvers can be added in the MiniZinc configuration).

Considering that the final part of the identifier sat now coincides with a common tag, it might be a good idea to consider changes the identifier.

[CervEdin]

@lperron and @Dekker1, did we come to a conclusion on the best way forward?

Sounds like the MiniZinc project copies https://github.com/google/or-tools/blob/stable/ortools/flatzinc/cpsat.msc.in when OR-tools in bundled with the MiniZinc IDE.

What we currently do is add our own solver configuration file (adding or-tools to tags) in our installation script of MiniZinc/OR-Tools so that we can continue to run minizinc --solver or-tools. However, this doesn't apply for those who install the MiniZinc toolchain using the MiniZinc installer and they have to manually fix the solver configuration file.

What @Dekker1 mentioned about --solver com.google.ortools.sat@9.10 was very interesting to hear (I didn't know about that). It sounds like a really useful feature for testing performance improvements and verifying against potential regression as a part of updating the OR-Tools CP-SAT solver.

For my use case, the id being com.google.ortools.sat is no different from com.google.ortools.cool-solver. My humble request is only that the id remains stable over time. But the point @Dekker1 made about sat being a common tag sounds like it deserves consideration.