No reified version of 'yuck_table_int' available

[xiroV]

I'm using MiniZinc to model different kinds of problems and compare the performance of different solvers. I've seen good results using Yuck on previous problems, but my current model depends on a reified version of the table constraint, which does not seem to exist for Yuck. Is this correct? Is it something that would be implemented at some point?

A small example which returns the error:

MiniZinc: flattening error: 'yuck_table_int' is used in a reified context but no reified version is available

Example:

include "table.mzn";

array[1..3,1..2] of int: someArray = array2d(1..3,1..2,
                        [1,2,
                         2,3,
                         4,5]);

array[int] of int: someVal = [2,3];
var bool: someVar;

constraint someVar >= table(someVal, someArray);

[informarte]

Just add the line

predicate yuck_table_int_reif(array[int] of var int: x, array[int] of int: t, var bool: satisfied);

to your model.

This trick will work for all global constraints implemented by Yuck.

I am still hesitating to provide this capability through Yuck's MiniZinc library because there are no clear requirements on which reified constraints to implement (beyond the basic FlatZinc vocabulary) and different solvers actually have different capabilities (e.g. Chuffed does not support table_int_reif, Gecode is the only solver to provide member_int_reif), so it's easy to create a vendor lock-in situation for users, and that's clearly against the spirit of MiniZinc. I think this topic deserves a wider discussion among solver developers.

[xiroV]

Thanks a lot for taking the time to explain this. I guess it makes sense, and I'll try to add the predicate to my model.

[informarte]

@xiroV, did you try the proposed workaround and was Yuck able to solve your problem?

[informarte]

I posted a question about reified global constraints in the MiniZinc forum: https://www.minizinc.org/forum.html?place=msg%2Fminizinc%2FBorILnSsq0k%2Fa8BM-dszCQAJ

[xiroV]

@informarte, I decided, partly because of your answer, to change my model to avoid this problem. I didn't want to limit myself to just a few solvers that supports this.

However, I did try your suggested workaround before changing the model. This however led to yuck crashing (got some Java/Scala error). Didn't look much into it, since I already decided to change the model, but I can try to reproduce if it would be of any interest to you. However it could have been because of something else. I'm still just taking my first steps into the world of constraint programming and MiniZinc :)

On the sample model however (from my initial comment), it works flawlessly.

On a final note, yuck is still not able to solve my problem, and neither is any of the other solvers I'm using, so I guess I'll have to get back to the drawing board.

With regards to your post on the MiniZinc forum, I think it's a really good suggestion to standardize these things, such that other people won't run into the same problems that I had. I can add that Oscar seems to support reified table constraint as well.

[informarte]

@xiroV, I am definitely interested in the crash. If you manage to reproduce it, please provide at least the stack trace. Thanks!

[xiroV]

Actually I realize that it is likely a problem in my model, and not yuck, since Gecode and Oscar reports Unsatisfiable. Yuck is just giving a stack trace which might be why I noticed it. I think I tracked it down to a predicate that looks something like

predicate my_pred(...) = table(...) \/ table(...);

and then using this in a reified context:

constraint viol >= sum(... where mypred(...))(1)

If that makes any sense. Unfortunately I don't have time to look at it any further, but here's that stack trace:

00:00:02 Thread 1/ main: java.lang.UnsupportedOperationException: empty.min
00:00:02 Thread 1/ main: scala.collection.TraversableOnce.min(TraversableOnce.scala:221)
00:00:02 Thread 1/ main: scala.collection.TraversableOnce.min$(TraversableOnce.scala:219)
00:00:02 Thread 1/ main: scala.collection.mutable.ArrayOps$ofInt.min(ArrayOps.scala:242)
00:00:02 Thread 1/ main: yuck.constraints.IntegerTable.initialize(IntegerTable.scala:67)
00:00:02 Thread 1/ main: yuck.constraints.IntegerTable.initialize(IntegerTable.scala:22)
00:00:02 Thread 1/ main: yuck.core.Space.initialize(Space.scala:383)
00:00:02 Thread 1/ main: yuck.annealing.SimulatedAnnealing.<init>(SimulatedAnnealing.scala:40)
00:00:02 Thread 1/ main: yuck.flatzinc.runner.FlatZincSolverGenerator$BaseSolverGenerator.call(FlatZincSolverGenerator.scala:85)
00:00:02 Thread 1/ main: yuck.flatzinc.runner.FlatZincSolverGenerator$BaseSolverGenerator.call(FlatZincSolverGenerator.scala:54)
00:00:02 Thread 1/ main: yuck.core.OnDemandGeneratedSolver.$anonfun$call$3(Solver.scala:134)
00:00:02 Thread 1/ main: scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)
00:00:02 Thread 1/ main: yuck.util.arm.package$.$anonfun$scoped$1(package.scala:42)
00:00:02 Thread 1/ main: yuck.util.logging.LazyLogger.$anonfun$withTimedLogScope$1(LazyLogger.scala:149)
00:00:02 Thread 1/ main: yuck.util.arm.package$.$anonfun$scoped$1(package.scala:42)
00:00:02 Thread 1/ main: yuck.core.OnDemandGeneratedSolver.call(Solver.scala:133)
00:00:02 Thread 1/ main: yuck.core.ParallelSolver$SolverRunner.$anonfun$run$3(Solver.scala:199)
00:00:02 Thread 1/ main: scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)
00:00:02 Thread 1/ main: yuck.util.arm.package$.$anonfun$scoped$1(package.scala:42)
00:00:02 Thread 1/ main: yuck.util.logging.LazyLogger.$anonfun$withTimedLogScope$1(LazyLogger.scala:149)
00:00:02 Thread 1/ main: yuck.util.arm.package$.$anonfun$scoped$1(package.scala:42)
00:00:02 Thread 1/ main: yuck.core.ParallelSolver$SolverRunner.$anonfun$run$2(Solver.scala:198)
00:00:02 Thread 1/ main: scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)
00:00:02 Thread 1/ main: yuck.util.arm.package$.$anonfun$scoped$1(package.scala:42)
00:00:02 Thread 1/ main: yuck.core.ParallelSolver$SolverRunner.$anonfun$run$1(Solver.scala:197)
00:00:02 Thread 1/ main: scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)
00:00:02 Thread 1/ main: yuck.util.arm.package$.$anonfun$scoped$1(package.scala:42)
00:00:02 Thread 1/ main: yuck.core.ParallelSolver$SolverRunner.run(Solver.scala:196)
00:00:02 Thread 1/ main: java.base/java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:515)
00:00:02 Thread 1/ main: java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
00:00:02 Thread 1/ main: java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
00:00:02 Thread 1/ main: java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
00:00:02 Thread 1/ main: java.base/java.lang.Thread.run(Thread.java:834)
Exception in thread "main" java.lang.UnsupportedOperationException: empty.min
    at scala.collection.TraversableOnce.min(TraversableOnce.scala:221)
    at scala.collection.TraversableOnce.min$(TraversableOnce.scala:219)
    at scala.collection.mutable.ArrayOps$ofInt.min(ArrayOps.scala:242)
    at yuck.constraints.IntegerTable.initialize(IntegerTable.scala:67)
    at yuck.constraints.IntegerTable.initialize(IntegerTable.scala:22)
    at yuck.core.Space.initialize(Space.scala:383)
    at yuck.annealing.SimulatedAnnealing.<init>(SimulatedAnnealing.scala:40)
    at yuck.flatzinc.runner.FlatZincSolverGenerator$BaseSolverGenerator.call(FlatZincSolverGenerator.scala:85)
    at yuck.flatzinc.runner.FlatZincSolverGenerator$BaseSolverGenerator.call(FlatZincSolverGenerator.scala:54)
    at yuck.core.OnDemandGeneratedSolver.$anonfun$call$3(Solver.scala:134)
    at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)
    at yuck.util.arm.package$.$anonfun$scoped$1(package.scala:42)
    at yuck.util.logging.LazyLogger.$anonfun$withTimedLogScope$1(LazyLogger.scala:149)
    at yuck.util.arm.package$.$anonfun$scoped$1(package.scala:42)
    at yuck.core.OnDemandGeneratedSolver.call(Solver.scala:133)
    at yuck.core.ParallelSolver$SolverRunner.$anonfun$run$3(Solver.scala:199)
    at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)
    at yuck.util.arm.package$.$anonfun$scoped$1(package.scala:42)
    at yuck.util.logging.LazyLogger.$anonfun$withTimedLogScope$1(LazyLogger.scala:149)
    at yuck.util.arm.package$.$anonfun$scoped$1(package.scala:42)
    at yuck.core.ParallelSolver$SolverRunner.$anonfun$run$2(Solver.scala:198)
    at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)
    at yuck.util.arm.package$.$anonfun$scoped$1(package.scala:42)
    at yuck.core.ParallelSolver$SolverRunner.$anonfun$run$1(Solver.scala:197)
    at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)
    at yuck.util.arm.package$.$anonfun$scoped$1(package.scala:42)
    at yuck.core.ParallelSolver$SolverRunner.run(Solver.scala:196)
    at java.base/java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:515)
    at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
    at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
    at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
    at java.base/java.lang.Thread.run(Thread.java:834)

So in case this is, as I suspect, a problem with how I have modelled things, I apologize for the inconvenience :)

[informarte]

It seems that the table implementation cannot deal with empty tables. I will look into this problem. Thanks a lot for the stack trace!

[informarte]

The problem with empty tables was already fixed in release 20190319. To avoid a regression, I added a test case.

[informarte]

The documentation of MiniZinc 2.3.0 clarifies that solver libraries should provide reified versions of constraints whenever possible, see https://www.minizinc.org/doc-2.3.0/en/fzn-spec.html#reified-and-half-reified-predicates, so Yuck will be extended accordingly.

[informarte]

@xiroV, I released a new version of Yuck with support for table_int_reif.