Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
MiniZinc: added kidney_exchange_model.mzn self_referential_sentence.mzn
- Loading branch information
Showing
3 changed files
with
162 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,109 @@ | ||
% | ||
% Kidney exchange in MiniZinc. | ||
% | ||
% A simple model of kidney exchange, inspired by Pascal Van Hentenryck's | ||
% introduction of the Coursera Course Discrete Optimization. | ||
% | ||
% The objective is to maximize the number of kidney exchanges given | ||
% the compatible | ||
% | ||
% Note that we are looking for cycles, which means that a person receiving | ||
% a kidney must be able to give a kidney. | ||
% | ||
|
||
% | ||
% This MiniZinc model was created by Hakan Kjellerstrand, hakank@gmail.com | ||
% See also my MiniZinc page: http://www.hakank.org/minizinc/ | ||
% | ||
|
||
include "globals.mzn"; | ||
|
||
int: num_people; | ||
array[1..num_people] of set of int: compatible; | ||
|
||
% people that has no no potential donors (and can't get a kidney) | ||
set of 1..num_people: non_compatible = { p | p in 1..num_people where card(compatible[p]) = 0 }; | ||
|
||
% The domains for each person | ||
array[1..num_people] of set of int: | ||
compatible_pruned = [ | ||
if card(compatible[p]) = 0 then {p} else (compatible[p] diff non_compatible) union {p} endif | ||
| p in 1..num_people ]; | ||
|
||
% | ||
% decision variables | ||
% | ||
|
||
% which kidney does person p get (or p if he/she gets no kidney) | ||
array[1..num_people] of var 1..num_people: x; | ||
|
||
var 0..num_people: z = sum([bool2int(x[i] != i) | i in 1..num_people]); | ||
|
||
% solve satisfy; | ||
% solve maximize z; | ||
solve :: int_search( | ||
x, | ||
first_fail, | ||
indomain_median, | ||
complete) | ||
maximize z; | ||
|
||
% Just allow the compatible people (+ p) in the domains | ||
% and remove uncompatible people. | ||
constraint | ||
forall(p in 1..num_people) ( | ||
x[p] in compatible_pruned[p] | ||
) | ||
/\ | ||
alldifferent(x) | ||
|
||
% experimental: first test if all are donors (-> circuit) | ||
% | ||
% works in MiniZinc v2.0, at least for some solvers. | ||
/\ (circuit(x) \/ true) | ||
; | ||
|
||
output [ | ||
"z: " ++ show(z) ++ "\n" ++ | ||
"x: " ++ show(x) ++ "\n" | ||
] | ||
++ | ||
[ | ||
"person: donor\n" | ||
] | ||
++ | ||
[ | ||
if fix(x[i] = i) then | ||
show_int(3, i) ++ ": -\n" | ||
else | ||
show_int(3, i) ++ ": " ++ show_int(3, x[i]) ++ "\n" | ||
endif | ||
| i in 1..num_people | ||
] | ||
++ | ||
[ | ||
show(x) ++ "\n" | ||
++ "z: " ++ show(z) ++ "\n" | ||
]; | ||
|
||
|
||
% | ||
% data | ||
% | ||
|
||
% The compatibility matrix | ||
% (from Pascal's introduction lecture) | ||
% who can give a kidney to person p | ||
% This is a directed graph | ||
% num_people = 8; | ||
% compatible = | ||
% [ | ||
% {2,3}, % 1 | ||
% {1,6}, % 2 | ||
% {1,4,7}, % 3 | ||
% {2}, % 4 | ||
% {2}, % 5 | ||
% {5}, % 6 | ||
% {8}, % 7 | ||
% {3}, % 8 | ||
% ]; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,50 @@ | ||
% | ||
% Self referential sentence in MiniZinc. | ||
% | ||
% E.g. from | ||
% http://puzzling.stackexchange.com/questions/1901/write-a-true-self-reflective-statement-about-the-digits-from-0-to-9-or-prove-it | ||
% | ||
% "This statement contains 1 0's, 7 1's, 3 2's, 2 3's, 1 4's, 1 5's, 1 6's, 2 7's, 1 8's, and 1 9's." | ||
% | ||
% Note: It happens that the number of occurrences of the digits are between 1..9 | ||
% so we don't have to worry about converting 10 to 1,0 etc. | ||
|
||
% | ||
% This MiniZinc model was created by Hakan Kjellerstrand, hakank@gmail.com | ||
% See also my MiniZinc page: http://www.hakank.org/minizinc/ | ||
% | ||
|
||
include "globals.mzn"; | ||
|
||
int: b = 9; % base | ||
int: n = 2*(b+1); | ||
|
||
% decision variables | ||
array[1..n] of var 0..b: x; | ||
|
||
|
||
solve satisfy; | ||
% solve :: int_search(x, first_fail, indomain_min, complete) satisfy; | ||
|
||
constraint | ||
% The digits 0..b are placed in positions x[i*2+1]. | ||
% Ensure that it is x[i*2+2] occurrences of the digit i | ||
forall(i in 0..b) ( | ||
x[i*2+1] = i | ||
/\ | ||
count(x,i,x[i*2+2]) | ||
) | ||
; | ||
|
||
output | ||
[ | ||
"x: ", show(x), "\n", | ||
"This statement contains " | ||
] | ||
++ | ||
[ | ||
show(x[i*2+2]) ++ " " ++ show(x[i*2+1]) ++ "'s, " ++ | ||
if i == b-1 then "and " else "" endif | ||
| i in 0..b | ||
]; | ||
|