Download
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;