Some time ago I transcribed Solfegiato into python script and converted to MIDI notes. Then printed it as TAB where each note is shown on all strings if the fret number is in range. I spent a lot of time choosing strings and fingerings to make it playable. It was plainly obvious that a constraint solver (or wave function collapse) would be a great way to select options for a playing style (alternating vs sweep picking for example). I didn't get that far. Congrats on doing the interesting part!

Jesus, what's going on between -O3 and -O4? This type of a gain warrants investigation. Have you tried profiling both cases?

The authors of the Gecode solver could explain it better than me, but I think that -O3 and -O4 perform a first pass that pre-compute variable bounds and values, which could reduce the exploration space significantly.

That is about right. What happens at -O4 is that for every variable, the upper and lower bounds are tested, and if using the bound as the value for the variable would make the problem unsolvable, then that bound is discarded. For some problems, this can be very useful and reduce the time to find a solution significantly. For other problems, it might not find any value to remove, or the values removed might not help solution times at all. The -O5 level is the same, but instead of just testing boundary values for immediate failure, all values in the domain are tested.

As a side note, while MiniZinc uses Gecode for the optimization this is not actually anything special built-in to Gecode, it is just a usage of the library.