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 | /* Steiner triplets in Comet. """ The ternary Steiner problem of order n is to find n(n-1)/6 sets of elements in {1,2,...,n} such that each set contains three elements and any two sets have at most one element in common. For example, the following shows a solution for size n=7: {1,2,3}, {1,4,5}, {1,6,7}, {2,4,6}, {2,5,7}, {3,4,7}, {3,5,6} Problem taken from: C. Gervet: Interval Propagation to Reason about Sets: Definition and Implementation of a PracticalLanguage, Constraints, An International Journal, vol.1, pp.191-246, 1997. """ Also see: Note: This model uses arrays of booleans as an representation of sets. 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; int t0 = System.getCPUTime(); int n = 7; int nb = (n * (n-1)) / 6; cout << "n: " << n << " nb: " << nb << endl; Solver<CP> m(); var <CP>{ bool } sets[1..nb, 1..n](m); Integer num_solutions(0); exploreall <m> { // explore<m> { forall (i in 1..nb) m.post( sum (j in 1..n) sets[i,j] == 3); forall (i in 1..nb, j in i+1..nb) { m.post( sum (k in 1..n) ( sets[i,k] && sets[j,k]) <= 1); } // symmetry breaking forall (i in 1..nb, j in i+1..nb) m.post(lexleq( all (k in 1..n) sets[i,k], all (k in 1..n) sets[j,k]) ); } using { label(m); num_solutions := num_solutions + 1; forall (i in 1..nb) { forall (j in 1..n) { if (sets[i,j]) cout << j << " " ; } cout << endl; } cout << endl; } cout << "\nnum_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; |