This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
en:dydaktyka:csp:lab2 [2017/03/13 15:58] msl |
en:dydaktyka:csp:lab2 [2019/06/27 15:49] 127.0.0.1 external edit |
||
|---|---|---|---|
| Line 48: | Line 48: | ||
| ==== Channeling ==== | ==== Channeling ==== | ||
| - | If you have more than one model of the same problem, you can combine them into one 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. | + | 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: [[http://ai.ia.agh.edu.pl/wiki/en:dydaktyka:csp:lab1#n-queens|N-Queens]] again | * Problem: [[http://ai.ia.agh.edu.pl/wiki/en:dydaktyka:csp:lab1#n-queens|N-Queens]] again | ||
| * Assignment: | * Assignment: | ||
| - Download, extract and comprehend {{:en:dydaktyka:csp:csp_n_queens.zip|the model}} (or use your own) | - Download, extract and comprehend {{:en:dydaktyka:csp:csp_n_queens.zip|the model}} (or use your own) | ||
| - | - Add the other problem definition to the problem | + | - Add another model of the problem |
| - | * Example: if the queens were assigned to the columns, you may now assign them to the rows | + | * 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 | ||
| - Channel constraints from the both models: | - Channel constraints from the both models: | ||
| - | * You may use channeling constraint [[http://www.minizinc.org/doc-lib/doc-globals-channeling.html#Ifunction-array-bo-int-bc-of-var-int-cl-inverse-po-array-bo-int-bc-of-var-int-cl-f-pc|''inverse'']] | + | * create constraint that connects variables from the model |
| - Compare running time of the normal and channeled model | - Compare running time of the normal and channeled model | ||
| - | - Give yourself a high five, <wrap lo>however new solvers are good enough to solve n-queens without the channeling. This technique is still valid for the more complicated problems</wrap> | + | - 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? | ||
| + | - Compare running time again | ||
| + | - Give yourself a [[https://youtu.be/kMUkzWO8viY|self-five]], <wrap lo>in this case, it may not improve the running time, but the technique itself is very useful in more complex problems</wrap> | ||
| - | ===== Search Modeling ===== | + | <code> |
| - | + | array[int] of var bool: qb0 = array1d(qb); | |
| - | So far we haven't talked about the way solver looks for the solution. There are many different techniques to solve to constraint programming problem, however basic techniques often perform a DFS (backtracking) search with two steps at every node: | + | array[int] of var bool: qb1 = [ qb[j,i] | i,j in 1..n ]; |
| - | - select variable --- choose, which variable will receive a value in this step | + | array[int] of var bool: qb2 = [ qb[i,j] | i in reverse(1..n), j in 1..n ]; |
| - | - select value --- choose, which value from the variable's domain will be chosen | + | array[int] of var bool: qb3 = [ qb[j,i] | i in 1..n, j in reverse(1..n) ]; |
| - | You may control this procedure in MiniZinc using search annotations just after the solve keyword. e.g. <code> | + | array[int] of var bool: qb4 = [ qb[i,j] | i in 1..n, j in reverse(1..n) ]; |
| - | solve :: int_search(array, first_fail, indomain_min, complete) satisfy; | + | 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) ]; | ||
| </code> | </code> | ||
| - | mean that że integer (''int'') variables from the ''array'' should be search exhaustively (''complete'') according to the simple strategy: | ||
| - | * select variable which has to lowest amount of available values (''first_fail'') | ||
| - | * select the smallest available value (''indomain_min''). | ||
| - | In order to define more interesting search strategies one has to use so called MiniSearch language, which still isn't a part of the MiniZincIDE package. | + | ===== Reified Constraints ===== |
| - | ==== N-Queens Again ==== | + | [[https://en.wikipedia.org/wiki/Reification|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 :) |
| - | + | ||
| - | * Definition: same as always. | + | ==== Stable Marriage Problem ===== |
| - | * Assignments: | + | * 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 [[https://en.wikipedia.org/wiki/Stable_marriage_problem|wikipedia]]. |
| - | - Run model using Gecode (Gist, bundled) solver --- select it in the configuration tab | + | * Assignment: |
| - | * play with the search :) | + | - Download, extract, comprehend {{ :en:dydaktyka:csp:stable_marriage.zip |the model}} |
| - | - Check four different search strategies<code> | + | - Add missing variables, constraints |
| - | int_search(rows, input_order, indomain_min, complete); | + | - Give a high-five to your teacher :) |
| - | int_search(rows, input_order, indomain_median, complete); | + | |
| - | int_search(rows, first_fail, indomain_min, complete); | + | |
| - | int_search(rows, first_fail, indomain_median, complete);</code> | + | |
| - | - Read about the [[http://www.minizinc.org/doc-lib/doc-annotations-search.html|different strategies]]. Select one according to your taste. | + | |
| - | - Compare solving time of the problem using different stragies. | + | |
| - | - Don't worry, be happy. | + | |
