Back

@robinhouston MiniZinc, hand-code the equations with integer variables rather than trying to do anything clever with arrays.

@pozorvlak Oh, nice! This is precisely the sort of thing I was hoping to learn about by asking this question.

@robinhouston

Running robin_puzzle.mzn

=====UNSATISFIABLE=====
Finished in 908msec.

Guess I mistyped something...

@pozorvlak at least it's quick :-)

@robinhouston Fixed a divide-vs-plus error, now running for six minutes and counting.

@robinhouston Success! It found the first solution in 8m 30s on a 2021 M1 MacBook. Here's my program:

set of int: COORD = 1..6;
set of int: VALUE = 1..36;

array[COORD,COORD] of var VALUE: v;

include "alldifferent.mzn";

constraint alldifferent(v);

constraint v[1,4] = 9;
constraint v[3,3] = 10;
constraint v[4,2] = 20;
constraint v[4,3] = 29;

constraint v[1,1] - v[1,2] - v[1,3] * v[1,4] - v[1,5] / v[1,6] = -70;
constraint v[2,1] + v[2,2] * v[2,3] + v[2,4] - v[2,5] - v[2,6] = 333;
constraint v[3,1] - v[3,2] - v[3,3] / v[3,4] * v[3,5] - v[3,6] = -187;
constraint v[4,1] - v[4,2] + v[4,3] - v[4,4] - v[4,5] * v[4,6] = -134;
constraint v[5,1] - v[5,2] - v[5,3] + v[5,4] + v[5,5] - v[5,6] = 3;
constraint v[6,1] * v[6,2] + v[6,3] + v[6,4] - v[6,5] - v[6,6] = 790;

constraint v[1,1] - v[2,1] / v[3,1] - v[4,1] + v[5,1] * v[6,1] = 1170;
constraint v[1,2] + v[2,2] + v[3,2] + v[4,2] + v[5,2] - v[6,2] = 84;
constraint v[1,3] - v[2,3] + v[3,3] + v[4,3] - v[5,3] + v[6,3] = 21;
constraint v[1,4] - v[2,4] / v[3,4] * v[4,4] - v[5,4] - v[6,4] = -180;
constraint v[1,5] + v[2,5] + v[3,5] + v[4,5] - v[5,5] - v[6,5] = 71;
constraint v[1,6] * v[2,6] + v[3,6] + v[4,6] - v[5,6] - v[6,6] = 389;

solve satisfy;

@pozorvlak Oh, that's very nice. A pretty direct translation of the problem into a fairly transparent syntax. Which solver did you use? (I assume that's a relevant question, since Wikipedia says MiniZinc can be used with a variety of solvers.)

@robinhouston Gecode (the default solver), with default settings.

@robinhouston I just tried setting the "return all solutions" option and bumping up the optimisation level to -O5; it found two solutions within a minute and is continuing to chug away.

@pozorvlak @robinhouston

-O5 throws this error for me for your program, on an Intel CPU with Ubuntu 24.04.2:

minizinc: ./lib/chain_compressor.cpp:405: virtual bool MiniZinc::LECompressor::trackItem(MiniZinc::Item*): Assertion `call->id() != _env.constants.ids.int2float' failed.
Process finished with non-zero exit code 6.

... but -O1 runs. All other optimization levels beyond O1 fail. Bummer.

@pozorvlak @robinhouston

With -O1, found one solution in 7m 4 s:

v =
[| 27, 23, 8, 9, 26, 13
| 12, 15, 24, 25, 34, 30
| 2, 31, 10, 1, 14, 18
| 3, 20, 29, 6, 35, 4
| 32, 17, 21, 11, 5, 7
| 36, 22, 19, 28, 33, 16
|];

... which seems to be different from all your solutions so far.

@albertcardona @robinhouston weird! That's a similar timeframe to when I ran my program with -O1, but not the same solution I found. The -O5 run of my program eventually finished after an hour, with 28 solutions: https://gist.github.com/pozorvlak/a5c145fcc9db72190d6163e4596636c7

@pozorvlak @robinhouston

Thanks. I tried with HiGHS with -O1 but I'm getting:

MiniZinc: evaluation error: Abort: Unable to create linear formulation for the `float_times(X_INTRODUCED_2886_, X_INTRODUCED_2887_, X_INTRODUCED_2888_)` constraint. To flatten this instance a quadratic constraint is required, but the usage of these constraints is currently disabled for the selected solver. Define `QuadrFloat=true` if your solver supports quadratic constraints, or use integer variables.

In your code, I thought the variables were already defined as integers.

@albertcardona they are, but the intermediate results of divisions might be floats (or rather, the solver isn't smart enough to work out that they aren't). I've got a newer version that avoids division: https://github.com/pozorvlak/robin_puzzle/blob/main/robin_puzzle.mzn

@robinhouston

@albertcardona @robinhouston Removing the divisions made Gecode finish faster, in 36 minutes. It also allowed Chuffed (which I think converts the program to SAT?) to run on the program, but that was slower, at 1hr 30ish.

@albertcardona @robinhouston adding the annotation `int_search(v, dom_w_deg, indomain_split)` (use binary search on the domains of v, prioritising variables which have caused constraint failures) gets the time to find all 28 solutions down to 7min 41s on Gecode -O5!

@pozorvlak @robinhouston There is art in everything .. chapeau.

@albertcardona @robinhouston hah, turns out most of the benefit was in turning -O5 back on after the MiniZinc IDE crashed - with Gecode -O5 but no annotations it finished in 8min 58s. Now trying with a search annotation on j (the results of the three-factor divisions).

@albertcardona @robinhouston ....and that took twice as long, 15min 45s. Lol. Lmao.