1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 | /* Langford's number problem in Comet Langford's number problem (CSP lib problem 24) """ Arrange 2 sets of positive integers 1..k to a sequence, such that, following the first occurence of an integer i, each subsequent occurrence of i, appears i+1 indices later than the last. For example, for k=4, a solution would be 41312432 """ * John E. Miller: Langford's Problem http://www.lclark.edu/~miller/langford.html * Encyclopedia of Integer Sequences for the number of solutions for each k Also, see the following models: - MiniZinc: http://www.hakank.org/minizinc/langford2.mzn - Gecode/R: http://www.hakank.org/gecode_r/langford.rb This Comet model was created by Hakan Kjellerstrand (hakank@gmail.com) Also, see my Comet page: http://www.hakank.org/comet */ // Licenced under CC-BY-4.0 : http://creativecommons.org/licenses/by/4.0/ import cotfd; // import cotls; // import cotln; int t0 = System.getCPUTime(); int k = 4; if (System.argc() >= 3) { k = System.getArgs()[2].toInt(); } range positionDomain = 1..2*k; Solver<CP> m(); var<CP>{int} position[i in positionDomain](m, positionDomain); var<CP>{int} solution[i in positionDomain](m, 1..k); Integer num_solutions(0); // explore<m> { exploreall<m> { forall(i in 1..k) { m.post(position[i+k] == position[i] + i+1 ); m.post(solution[position[i]] == i ); m.post(solution[position[k+i]] == i); } m.post(alldifferent(position)); // symmetry breaking m.post(solution[1] < solution[2*k]); } using { // label(position); // label(solution); /* forall(i in positionDomain : !position[i].bound()) {// by (-position[i].getSize()) { label(position[i]); } forall(i in positionDomain : !solution[i].bound()) {// by (-solution[i].getSize()) { label(solution[i]); } */ labelFF(m); // cout << position << endl; cout << solution << endl; num_solutions := num_solutions + 1; } cout << "num_solutions: " << num_solutions << endl; int t1 = System.getCPUTime(); cout << "time: " << (t1-t0) << endl; cout << "#choices = " << m.getNChoice() << endl; cout << "#fail = " << m.getNFail() << endl; cout << "#propag = " << m.getNPropag() << endl; |