1 // Copyright 2011 Hakan Kjellerstrand hakank@gmail.com
2 // Licensed under the Apache License, Version 2.0 (the "License");
3 // you may not use this file except in compliance with the License.
4 // You may obtain a copy of the License at
5 //
6 //     http://www.apache.org/licenses/LICENSE-2.0
7 //
8 // Unless required by applicable law or agreed to in writing, software
9 // distributed under the License is distributed on an "AS IS" BASIS,
10 // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11 // See the License for the specific language governing permissions and
12 // limitations under the License.
13 package com.google.ortools.contrib;
14 
15 import com.google.ortools.Loader;
16 import com.google.ortools.constraintsolver.DecisionBuilder;
17 import com.google.ortools.constraintsolver.IntVar;
18 import com.google.ortools.constraintsolver.Solver;
19 import java.io.*;
20 import java.text.*;
21 import java.util.*;
22 
23 public class WhoKilledAgatha {
24   /**
25    * Implements the Who killed Agatha problem. See
26    * http://www.hakank.org/google_or_tools/who_killed_agatha.py
27    */
solve()28   private static void solve() {
29     Solver solver = new Solver("WhoKilledAgatha");
30 
31     //
32     // data
33     //
34     final int n = 3;
35     final int agatha = 0;
36     final int butler = 1;
37     final int charles = 2;
38 
39     String[] names = {"Agatha", "Butler", "Charles"};
40 
41     //
42     // variables
43     //
44     IntVar the_killer = solver.makeIntVar(0, 2, "the_killer");
45     IntVar the_victim = solver.makeIntVar(0, 2, "the_victim");
46 
47     IntVar[] all = new IntVar[2 * n * n]; // for branching
48 
49     IntVar[][] hates = new IntVar[n][n];
50     IntVar[] hates_flat = new IntVar[n * n];
51     for (int i = 0; i < n; i++) {
52       for (int j = 0; j < n; j++) {
53         hates[i][j] = solver.makeIntVar(0, 1, "hates[" + i + "," + j + "]");
54         hates_flat[i * n + j] = hates[i][j];
55         all[i * n + j] = hates[i][j];
56       }
57     }
58 
59     IntVar[][] richer = new IntVar[n][n];
60     IntVar[] richer_flat = new IntVar[n * n];
61     for (int i = 0; i < n; i++) {
62       for (int j = 0; j < n; j++) {
63         richer[i][j] = solver.makeIntVar(0, 1, "richer[" + i + "," + j + "]");
64         richer_flat[i * n + j] = richer[i][j];
65         all[(n * n) + (i * n + j)] = richer[i][j];
66       }
67     }
68 
69     //
70     // constraints
71     //
72 
73     // Agatha, the butler, and Charles live in Dreadsbury Mansion, and
74     // are the only ones to live there.
75 
76     // A killer always hates, and is no richer than his victim.
77     //     hates[the_killer, the_victim] == 1
78     //     hates_flat[the_killer * n + the_victim] == 1
79     solver.addConstraint(solver.makeEquality(
80         solver
81             .makeElement(
82                 hates_flat, solver.makeSum(solver.makeProd(the_killer, n).var(), the_victim).var())
83             .var(),
84         1));
85 
86     //    richer[the_killer, the_victim] == 0
87     solver.addConstraint(solver.makeEquality(
88         solver
89             .makeElement(
90                 richer_flat, solver.makeSum(solver.makeProd(the_killer, n).var(), the_victim).var())
91             .var(),
92         0));
93 
94     // define the concept of richer:
95     //     no one is richer than him-/herself...
96     for (int i = 0; i < n; i++) {
97       solver.addConstraint(solver.makeEquality(richer[i][i], 0));
98     }
99 
100     // (contd...) if i is richer than j then j is not richer than i
101     //   if (i != j) =>
102     //       ((richer[i,j] = 1) <=> (richer[j,i] = 0))
103     for (int i = 0; i < n; i++) {
104       for (int j = 0; j < n; j++) {
105         if (i != j) {
106           IntVar bi = solver.makeIsEqualCstVar(richer[i][j], 1);
107           IntVar bj = solver.makeIsEqualCstVar(richer[j][i], 0);
108           solver.addConstraint(solver.makeEquality(bi, bj));
109         }
110       }
111     }
112 
113     // Charles hates no one that Agatha hates.
114     //    forall i in 0..2:
115     //       (hates[agatha, i] = 1) => (hates[charles, i] = 0)
116     for (int i = 0; i < n; i++) {
117       IntVar b1a = solver.makeIsEqualCstVar(hates[agatha][i], 1);
118       IntVar b1b = solver.makeIsEqualCstVar(hates[charles][i], 0);
119       solver.addConstraint(solver.makeLessOrEqual(solver.makeDifference(b1a, b1b).var(), 0));
120     }
121 
122     // Agatha hates everybody except the butler.
123     solver.addConstraint(solver.makeEquality(hates[agatha][charles], 1));
124     solver.addConstraint(solver.makeEquality(hates[agatha][agatha], 1));
125     solver.addConstraint(solver.makeEquality(hates[agatha][butler], 0));
126 
127     // The butler hates everyone not richer than Aunt Agatha.
128     //    forall i in 0..2:
129     //       (richer[i, agatha] = 0) => (hates[butler, i] = 1)
130     for (int i = 0; i < n; i++) {
131       IntVar b2a = solver.makeIsEqualCstVar(richer[i][agatha], 0);
132       IntVar b2b = solver.makeIsEqualCstVar(hates[butler][i], 1);
133       solver.addConstraint(solver.makeLessOrEqual(solver.makeDifference(b2a, b2b).var(), 0));
134     }
135 
136     // The butler hates everyone whom Agatha hates.
137     //     forall i : 0..2:
138     //         (hates[agatha, i] = 1) => (hates[butler, i] = 1)
139     for (int i = 0; i < n; i++) {
140       IntVar b3a = solver.makeIsEqualCstVar(hates[agatha][i], 1);
141       IntVar b3b = solver.makeIsEqualCstVar(hates[butler][i], 1);
142       solver.addConstraint(solver.makeLessOrEqual(solver.makeDifference(b3a, b3b).var(), 0));
143     }
144 
145     // Noone hates everyone.
146     //     forall i in 0..2:
147     //         (sum j in 0..2: hates[i,j]) <= 2
148     for (int i = 0; i < n; i++) {
149       IntVar[] tmp = new IntVar[n];
150       for (int j = 0; j < n; j++) {
151         tmp[j] = hates[i][j];
152       }
153       solver.addConstraint(solver.makeLessOrEqual(solver.makeSum(tmp).var(), 2));
154     }
155 
156     // Who killed Agatha?
157     solver.addConstraint(solver.makeEquality(the_victim, agatha));
158 
159     //
160     // search
161     //
162     DecisionBuilder db =
163         solver.makePhase(all, solver.CHOOSE_FIRST_UNBOUND, solver.ASSIGN_MIN_VALUE);
164 
165     solver.newSearch(db);
166 
167     //
168     // output
169     //
170     while (solver.nextSolution()) {
171       System.out.println("the_killer: " + names[(int) the_killer.value()]);
172     }
173     solver.endSearch();
174 
175     // Statistics
176     System.out.println();
177     System.out.println("Solutions: " + solver.solutions());
178     System.out.println("Failures: " + solver.failures());
179     System.out.println("Branches: " + solver.branches());
180     System.out.println("Wall time: " + solver.wallTime() + "ms");
181   }
182 
main(String[] args)183   public static void main(String[] args) throws Exception {
184     Loader.loadNativeLibraries();
185     WhoKilledAgatha.solve();
186   }
187 }
188