Modelling can be broken down into several steps. The first steps aim to express the problem so that one can get a solution. The rest of the steps aim to look for ways to improve the pruning so that one can get a solution quicker.
The following points are duplicated in the modelling examples found in the menu. It might be helpful to read an example in parallel with this page to get some concrete examples of each step.
The first step is to understand the problem, more specifically to understand what is required of a solution to the problem. Express the entire problem in a few concise bullet points that describe exactly what is expected of a solution.
The next step is to select how to represent the problem in terms of variables. The variables will need to include the sought solutions.
Try to pick a view that cuts down on the number of constraints that explicitly have to be expressed.
An example is the n-queens problem where the choice of view takes care of the constraint that there may only be one queen per column. Using for instance an n-times-n matrix of boolean variables would have required explicitly expressing that constraint.
There may very well be multiple views that are equally good at representing the problem. Being aware of more than one might help further down the line. Constraints might end up being hard to describe in one view, but trivial in another.
There’s no need to restrict oneself to only using one view. One can link multiple views using the channel constraints to get the best of both worlds.
Now apply your understanding of the problem. Take a look at the points and try to convert them into constraints (possibly multiple). Multiple views can help here since it might be easier to find corresponding constraints when looking at a different view of the problem.
Remember that reification can be used to combine constraints and thereby express complex rules. Reification should be thought of as a last resort as a single constraint will probably be more powerful than if you glue several constraints together with reification.
The last thing to think about is the branching. Anything that you tell Gecode to branch on will be required to be assigned in a solution. Do not branch on variables that you do not need the values of from a solution.
Selecting branching strategy is mostly a question about coming up with a heuristic that fits the problem. This can either be done by reasoning about how the possibilities should best be explored or by simply testing all the strategies to find out which work and which don’t.
By now you should be able to feed the solver a simple problem and get pack a correct solution. If it works fast enough for you then that’s great, if not then you need to tweak the performance.
Branching strategies can make a large difference. Which strategy is best depends on the problem. Compare the available ones if you haven’t already done so.
Using different propagation strength can, much like branching strategies, make a large difference. Much like branching strategies it’s a matter of reasoning or simply trying them out.
Just because you have given the solver enough constraints to be able to identify a solution doesn’t mean that you have to stop there. It might still be worth explicitly expressing some of the constraints that are implicitly given by the expressed constraints. It will not change the solutions, but it can help Gecode prune the search space faster.
In many situations symmetries will appear.
In the n-queens example there are several rotational and reflection symmetries. The chessboard can for instance be rotated without changing whether an assignment is a solution. Nothing is done to counter the symmetries in the example. There are in total only 12 unique solutions, but the example will return 92.
Symmetries are unnecessary since they add nothing. Removing them means that you get a smaller search space, which means that you can find a solution faster.
The way to remove symmetries is to impose additional constraints that do not remove any unique solutions, only symmetries. In the n-queens case you can for instance constrain the queen in the first column to be above the queen in the last column. Any solution that the additional constraint invalidates can be turned into a valid solution through reflection in the y-axis of the board. Hence only removing symmetries, not unique solutions.