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