The problem is said to contain symmetry if there exist classes of equivalent solutions — solutions, which are called symmetrical because there exists a simple mechanical procedure to obtain one from another. Graph Coloring Problem has a very obvious symmetry — in every solution we can freely swap colors, e.g. every red node repaint as blue, and every blue node repaint as red. Solutions of this kind aren't bad, just redundant, leading to a much bigger search space. Symmetry breaking prunes the search space by removing symmetries from the problem.

All files required to solve the assignments are available via the repository, so clone it first.

• Problem: Same as before
• Assignment:
  1. Look at and comprehend lab3/graph_coloring/graph_coloring.mzn model.
  2. Try to solve the basic_data.dzn instance.
     • You can use the model created during previous classes
     • There is a chance, that problem would too difficult to be solved in a reasonable time.
  3. File data_with_clique.dzn includes info about the largest clique in the graph
     • minColorsNumber - size of the largest clique
     • maxClique - indexes of the vertices forming the largest clique
  4. Improve model to make use of the info about the largest clique
  5. Try to solve the problem again.

• Definition: Knapsack problem with several identical knapsacks instead of one.
• Assignment:
  1. Find a symmetry in the problem.
  2. Look at and comprehend lab3/multi_knapsack/multi_knapsack.mzn.
     • Note : this model is not an example of good constraint model; it's just used to show a common technique to break symmetries
     • Note use of the at_most global constraint.
     • There is a defined predicate named knapsack → it's the first example of user-defined predicate
  3. Run model with the associated data file:
     • The problem may be too hard for the solver
  4. Break symmetry using ''lex_less_eq'' global constraint.
  5. Run the new model with the same data file

There is a good chance the problem can be defined in more than one way. Also you may find a set of constraints that is sufficient to define the problem. That's cool, however there can exist so called “redundant constraints”; redundant because they do not have an impact on the number or quality of the solutions. The only reason to include them in the model is that they may contain additional info about the structure of the problem, therefore giving solver an opportunity to prune the search space (most of the solver prune the search space by propagating constraints, a redundant constraint may boost this process).

• Definition: Same as before
• Assignment:
  1. Look at and comprehend lab3/magic_series/magic_series.mzn
  2. Add redundant constraints, hints:
     • what should be equal the sum of the magic sequence?
     • what should be equal the sum of sequence elements multiplied by their indexes (if indexing starts from 0)?
  3. Compare solving time with and without the redundant constraints.
  4. Smile with satisfaction

If you have more than one model of the same problem, you can combine them into a single model. Why would one do that? Mostly because some constraints are easier to express with different variables. Other reason could be that the second model often makes a great example of the redundant constraints.

• Problem: N-Queens again
• Assignment:
  1. Look at and comprehend lab3/n_queens/n_queens.mzn
  2. Add another model of the problem
     • try to use the boolean array of variables array[1..n, 1..n] of var bool: qb; (queen boolean)
     • add missing constraints so the second model was also independent
  3. Channel constraints from the both models:
     • create constraint that connects variables from the model
  4. Compare running time of the normal and channeled model
  5. Add symmetry breaking to the problem by using lex_lesseq constraint on the different permutations of the qb array
     • below the assignments there is a code listing with all permutations calculated in MiniZinc, can you tell what symmetries they represent?
  6. Compare running time again
  7. Give yourself a self-five, in this case, it may not improve the running time, but the technique itself is very useful in more complex problems

array[int] of var bool: qb0 = array1d(qb);
array[int] of var bool: qb1 = [ qb[j,i] | i,j in 1..n ];
array[int] of var bool: qb2 = [ qb[i,j] | i in reverse(1..n), j in 1..n ];
array[int] of var bool: qb3 = [ qb[j,i] | i in 1..n, j in reverse(1..n) ];
array[int] of var bool: qb4 = [ qb[i,j] | i in 1..n, j in reverse(1..n) ];
array[int] of var bool: qb5 = [ qb[j,i] | i in reverse(1..n), j in 1..n ];
array[int] of var bool: qb6 = [ qb[i,j] | i,j in reverse(1..n) ];
array[int] of var bool: qb7 = [ qb[j,i] | i,j in reverse(1..n) ];

Reification in Constraint Programming means treating the constraint as a first-order citizen, i.e. you can use the constraint as a boolean value in your model. If you've used the bool2int function in the Magic Sequence problem, you could do that only because the constraint = has been reified. Reification allows us to create models with “soft constraints” or “conditional constraints”, i.e. one constraint has to be satisfed only if the second one is satisfied too, otherwise they both can be ignored. To do that, one has only to reify the constraints and connect them with the implication: constraint1 → constraint2. Let's practice this quite useful technique :)

• Problem: There are two classes of objects (men and women, for example) that have to be matched according to their preferences. We say that a matching (marriage) is unstable if both spouses would prefer to be with somebody else. You can read more about this problem on wikipedia.
• Assignment:
  1. Look at and comprehend lab3/stable-marriage/stable-marriage.mzn
  2. Add missing variables, constraints
  3. Give a high-five to your teacher :)