search

unison-code / unison

Unison's source code
http://unison-code.github.io/
Other
101 stars 17 forks source link

Query regarding different solver in multi_backend (minizinc) #45

Closed utkarshyen closed 4 years ago

utkarshyen commented 4 years ago

Hello @robcasloz

I tried the steps you mentioned (https://github.com/unison-code/unison/issues/44) for using the multiback. However, I tried changing the solvers. Check some of the samples. Following cases I tried for which I got different behavior like (infinite loop).

  1. Using default unison with gecode.
    • Works perfectly fine.
  2. Using minizinc-solver script with gecode.
    • Hangs (infinite loop)
  3. Using minizinc-solver script with ortools.

    • Fails with below error.

      Not supported member_int Check failure stack trace: @ 0x7f674c3d9d04 google::LogMessage::Fail() @ 0x7f674c3d9c48 google::LogMessage::SendToLog() @ 0x7f674c3d9584 google::LogMessage::Flush() @ 0x7f674c3dd0ab google::LogMessageFatal::~LogMessageFatal() @ 0x7f674c8fecf7 operations_research::sat::(anonymous namespace)::CpModelProtoWithMapping::FillConstraint() @ 0x7f674c902b93 operations_research::sat::SolveFzWithCpModelProto() @ 0x402412 main @ 0x7f674ba81830 __libc_start_main @ 0x4028b9 _start @ (nil) (unknown) %%%mzn-stat: nSolutions=0 =====ERROR===== aeson-pretty: invalid json

real 0m9.739s user 0m9.551s sys 0m0.135s

  1. minizinc standalone binary with gecode.
    • Hangs (infinite loop)
  2. minizinc standalone binary with ortools.
    • works properly, sometimes fails.

Is there any difference between the binaries unison is using and open source binaries. Is the issue with the mzn model?

I could see, mzn-gecode, mzn-or-tools, mzn-or-tools-sat scripts invoking fzn-gecode. May I know difference between those? Binary I got from ortools/gecode are gecode, fz, cbc, etc.

Is your gecode solver binary is different from oss gecode?

Additionally, I don't have or generated mzn-or-tools, mzn-or-tools-sat scripts.

This is confusing me a bit as I'm a beginner into this. Can you please clear up my thoughts/views?

Regards, Utkarsh

utkarshyen commented 4 years ago

Hello @robcasloz,

I could see that whatever solver I use with multi_backend minizinc (gecode, ortools or chuffed) it is going into the infinite loop. Is the issue with mzn model file? Please note, tried setting the time limit. Resulted in ====UNKNOWN==== Solution.

Regards, UT

utkarshyen commented 4 years ago

Hello @robcasloz,

Sorry, below are the environment details, I'm running on ubuntu 16.04. Minizinc version - 2.4.2 Gecode version - 6.0.0 or-tools version - 7.0 (stable)

Can you please let me know the versions used for multi_backend minizinc-solver?

Regards, Utkarsh

robcasloz commented 4 years ago

Hi @utkarshyen,

In our experiments, we have used MiniZinc bundle 2.1.2 on Ubuntu 16.04. We have used the Chuffed solver available within the MiniZinc bundle. Assuming an input file unison.dzn, we invoke minizinc-solver like this:

minizinc-solver -o unison.out.json -dzn unison.dzn --topdown --chuffed --no-diffn --free --rnd DUMMY_FILENAME

In the actual experiments we use portfolio-solver, which invokes both minizinc-solver using Chuffed with this configuration by default and gecode-solver simultaneously, like this:

portfolio-solver -o unison.out.json unison.ext.json

(portfolio-solver implicitly expects to find a file unison.dzn in the same directory as unison.ext.json to be passed to minizinc-solver).

Sorry for the complexity and lack of documentation in this area, the Minizinc back-end is highly experimental :)

utkarshyen commented 4 years ago

Thank you @robcasloz again for detailed info. I'll give a try with this and explore more. Hmm....

Sorry for the complexity and lack of documentation in this area

No worries, I might prepare at my end :D

he Minizinc back-end is highly experimental :)

Indeed. It's highly interesting too if everything works in the end. :P

Regards, Utkarsh