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.

@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 The same two that jlcarr found in the Reddit thread? Or do we know there are more than two in total?

@robinhouston so far I have three (unchecked):

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

@robinhouston I'll leave that running for a bit longer, then try a different solver, and maybe adding some extra constraints to force the divisions to be integers. That may or may not help, solver performance tuning is a maddening business!

@pozorvlak Is there any way to assess progress? One of the more maddening aspects of working with solvers is not knowing whether it's worth leaving it running or not; i.e. whether it's likely to finish in hours, or millennia

@robinhouston @pozorvlak

I'm in trouble!

@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 I haven't yet tried using search-strategy annotations, but I think that could be productive - getting the solver to nail down the possible values of v[3,4] seems like a good start.

@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.