Search code examples
minizinc

Simple small problem takes a lot of time to prove unsatisfiability

My code generates minizinc problems on the flight, and recently I faced the following issue:

var int: a;
var int: b;

constraint a < b;
constraint a > b;

solve satisfy;

It takes enormous time (~ 2 mins on my machine) to prove unsatisfiability.

I tried different solvers and search strategies but failed to speed up the solving.

Unfortunately, I can't tie bounds and or/use MIP because of the specifics of my area. For example, I can have other constraints like a * b < 100 or a == arbitrary number.

Any thoughts? I will be very thankful for any advice.

best,

Solution

  • The issue is - as you mention - that there are no bounds on the variables which is not very good for CP solvers. Is there no way that you can give a large domain on the problem? For example with

    var -100000..100000: a;
var -100000..100000: b;

    then Gecode takes 0.5s to yield UNSAT.

    For your original problem (with var int), I tested with some SAT based / non-CP solvers which detect UNSAT quite fast:

    • geas: 5.282s

    • picatSAT: 0.115s

    • optimathSAT: 0.519s

    • mistral: 0.177s

    • oscar_cbls: 1.376s

    I also tested with the SAT hybrid solvers OR-tools and Chuffed, but they where quite slower on this specific problem.

    However, that is just one half of the problem, since the solver should also be fast on non-UNSAT instances, right? Then the SAT solvers might not be the fastest.

    One idea is to use a portfolio solver such as SunnyCP which has a pool of different FlatZinc solvers trying to solve the problem in parallel. (Unfortunately, my SunnyCP installation does not work right now so I can't test it.)