array[1..1000] of var 1..1000: solution; constraint forall(i in 1..998)(solution[i]<solution[i+2]); constraint solution[999]<solution[2]; solve satisfy;
i.e.: create an array "solution" of length 1000, populated by integers between 1 and 1000, such that solution[i] < solution[i+2] and solution[999] < solution[2].
There's only one solution to this: [1,501,2,502,...]
MiniZinc/Gecode takes about 60 msec to find that solution. From previous experience there's about 30 msec of overhead in calling MZ, so the search time is around 30 msec.
There are 1000^1000 possible ways to populate that array, of which only one satisfies the constraints, so evidently Gecode isn't just rolling the dice until it finds a solution that works.
Even a naive search strategy that starts by guessing a value for solution[1], then solution[2], and so on, testing constraints at every step, is going to run forever because it takes waaaay too long to discover that a bad choice at the start will trip you up later. For example, if you start with solution[1]=1 & solution[2]=500, you can get very nearly to the end of the array going [1,500,2,501,...] before discovering that there's no legal option for entry 999.
My understanding is that among other things, MZ/Gecode are smart enough to use the supplied constraints to build relationships between the variables. If you know solution[i] is in 1..1000 and solution[3]>solution[1], then you can establish that solution[3] must be at least 2 and solution[1] is at most 999. The constraint that solution[5]>solution[3] then lets you restrict range for solution[1] to 1..998 and solution[5] to 3..1000, and so on.
If you build a problem complex enough, then you'll reach a point where it can't be solved purely by this kind of logic, and trial-and-error is necessary. (Or, sometimes it's easy to find a solution, but you're looking for the best solution under some metric.)
At that point, random guessing among the not-yet-eliminated values is one option for the search strategy, and sometimes it's effective - I found it useful in one of the assignment questions. But there are others. Choosing the best one is the tricky part!
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2015-10-20 08:48 pm (UTC)Test code:
array[1..1000] of var 1..1000: solution;
constraint forall(i in 1..998)(solution[i]<solution[i+2]);
constraint solution[999]<solution[2];
solve satisfy;
i.e.: create an array "solution" of length 1000, populated by integers between 1 and 1000, such that solution[i] < solution[i+2] and solution[999] < solution[2].
There's only one solution to this: [1,501,2,502,...]
MiniZinc/Gecode takes about 60 msec to find that solution. From previous experience there's about 30 msec of overhead in calling MZ, so the search time is around 30 msec.
There are 1000^1000 possible ways to populate that array, of which only one satisfies the constraints, so evidently Gecode isn't just rolling the dice until it finds a solution that works.
Even a naive search strategy that starts by guessing a value for solution[1], then solution[2], and so on, testing constraints at every step, is going to run forever because it takes waaaay too long to discover that a bad choice at the start will trip you up later. For example, if you start with solution[1]=1 & solution[2]=500, you can get very nearly to the end of the array going [1,500,2,501,...] before discovering that there's no legal option for entry 999.
My understanding is that among other things, MZ/Gecode are smart enough to use the supplied constraints to build relationships between the variables. If you know solution[i] is in 1..1000 and solution[3]>solution[1], then you can establish that solution[3] must be at least 2 and solution[1] is at most 999. The constraint that solution[5]>solution[3] then lets you restrict range for solution[1] to 1..998 and solution[5] to 3..1000, and so on.
If you build a problem complex enough, then you'll reach a point where it can't be solved purely by this kind of logic, and trial-and-error is necessary. (Or, sometimes it's easy to find a solution, but you're looking for the best solution under some metric.)
At that point, random guessing among the not-yet-eliminated values is one option for the search strategy, and sometimes it's effective - I found it useful in one of the assignment questions. But there are others. Choosing the best one is the tricky part!