Exact gets unsatisfiable input on models/3_jugs_regular16650499634232442.bt

[JoD]

When running bigtest, one problem still remains: tests/test_exact.py::test_model[models/3_jugs_regular16650499634232442.bt]

Exact reports unsatisfiable, while it should not be. I've checked by outputting the variables and constraints received by Exact, and solving these with OR-tools. See jugs_on_exact_input.py.txt.

I'll minimize and dig deeper later.

[IgnaceBleukx]

Ok I'm pretty sure the issue has to do with duplicate naming of variables.
Bigtest does not use the built-in Model.from_file which checks for potential naming issues with variables, but rather directly loads the model using pickle.loads.

If I change the names of the variables when loading the model (e.g., lowercase all of varnames), the model is SAT!

So actually this is not a problem with exact, nor the transformations, but with bigtest :)

[JoD]

Interesting catch! Another reason to create our own model files at some point. So, what do we do for now? Keep things as is?

[tias]

To be determined by Wout, but as a minimal I think it makes sense to 'overwrite' messed up pickles (e.g. this one and the abs ones) with new pickles with compatible objects.

Text-based model files are desirable at some point though, e.g. also to measure object creating times/regressions.