From 7cfbb1778221ad37b8298244cdbe2972fbb8e6fb Mon Sep 17 00:00:00 2001 From: hakank Date: Sun, 10 Oct 2010 19:54:04 +0000 Subject: [PATCH] Added labeled_dice.py who_killed_agatha.py --- python/labeled_dice.py | 145 +++++++++++++++++++++++ python/who_killed_agatha.py | 223 ++++++++++++++++++++++++++++++++++++ 2 files changed, 368 insertions(+) create mode 100644 python/labeled_dice.py create mode 100644 python/who_killed_agatha.py diff --git a/python/labeled_dice.py b/python/labeled_dice.py new file mode 100644 index 0000000000..5d0f8b58e2 --- /dev/null +++ b/python/labeled_dice.py @@ -0,0 +1,145 @@ +# Copyright 2010 Hakan Kjellerstrand hakank@bonetmail.com +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +""" + + Labeled dice problem in Google CP Solver. + + From Jim Orlin 'Colored letters, labeled dice: a logic puzzle' + http://jimorlin.wordpress.com/2009/02/17/colored-letters-labeled-dice-a-logic-puzzle/ + ''' + My daughter Jenn bough a puzzle book, and showed me a cute puzzle. There + are 13 words as follows: BUOY, CAVE, CELT, FLUB, FORK, HEMP, JUDY, + JUNK, LIMN, QUIP, SWAG, VISA, WISH. + + There are 24 different letters that appear in the 13 words. The question + is: can one assign the 24 letters to 4 different cubes so that the + four letters of each word appears on different cubes. (There is one + letter from each word on each cube.) It might be fun for you to try + it. I'll give a small hint at the end of this post. The puzzle was + created by Humphrey Dudley. + ''' + + Jim Orlin's followup 'Update on Logic Puzzle': + http://jimorlin.wordpress.com/2009/02/21/update-on-logic-puzzle/ + + + Compare with the following models: + * ECLiPSe: http://hakank.org/eclipse/labeled_dice.ecl + * Comet : http://www.hakank.org/comet/labeled_dice.co + * Gecode : http://hakank.org/gecode/labeled_dice.cpp + * SICStus: http://hakank.org/sicstus/labeled_dice.pl + * Zinc : http://hakank.org/minizinc/labeled_dice.zinc + + + This model was created by Hakan Kjellerstrand (hakank@bonetmail.com) + Also see my other Google CP Solver models: http://www.hakank.org/google_or_tools/ +""" + +from constraint_solver import pywrapcp + + +def main(): + + # Create the solver. + solver = pywrapcp.Solver('Labeled dice') + + # + # data + # + n = 4 + m = 24 + A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,Y = range(m) + letters = ["A","B","C","D","E","F","G","H","I","J","K","L","M", + "N","O","P","Q","R","S","T","U","V","W","Y"] + + num_words = 13 + words = [ + [B,U,O,Y], + [C,A,V,E], + [C,E,L,T], + [F,L,U,B], + [F,O,R,K], + [H,E,M,P], + [J,U,D,Y], + [J,U,N,K], + [L,I,M,N], + [Q,U,I,P], + [S,W,A,G], + [V,I,S,A], + [W,I,S,H] + ] + + # + # declare variables + # + dice = [solver.IntVar(0, n-1, 'dice[%i]'%i) for i in range(m)] + + # + # constraints + # + + # the letters in a word must be on a different die + for i in range(num_words): + solver.Add(solver.AllDifferent([dice[words[i][j]] for j in range(n)], True)) + + # there must be exactly 6 letters of each die + for i in range(n): + b = [solver.IsEqualCstVar(dice[j], i) for j in range(m)] + solver.Add(solver.Sum(b) == 6) + + + # + # solution and search + # + solution = solver.Assignment() + solution.Add(dice) + + db = solver.Phase(dice, + solver.CHOOSE_FIRST_UNBOUND, + solver.ASSIGN_MIN_VALUE) + + # + # result + # + solver.NewSearch(db) + num_solutions = 0 + while solver.NextSolution(): + num_solutions += 1 + # print "dice:", [(letters[i],dice[i].Value()) for i in range(m)] + for d in range(n): + print "die %i:" % d, + for i in range(m): + if dice[i].Value() == d: + print letters[i], + print + + print "The words with the cube label:" + for i in range(num_words): + for j in range(n): + print "%s (%i)" % (letters[words[i][j]], dice[words[i][j]].Value()), + print + + print + + solver.EndSearch() + + print + print "num_solutions:", num_solutions + print "failures:", solver.failures() + print "branches:", solver.branches() + print "wall_time:", solver.wall_time() + +if __name__ == '__main__': + main() diff --git a/python/who_killed_agatha.py b/python/who_killed_agatha.py new file mode 100644 index 0000000000..c765a035b9 --- /dev/null +++ b/python/who_killed_agatha.py @@ -0,0 +1,223 @@ +# Copyright 2010 Hakan Kjellerstrand hakank@bonetmail.com +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +""" + + Who killed agatha? (The Dreadsbury Mansion Murder Mystery) in Google CP Solver. + + This is a standard benchmark for theorem proving. + + http://www.lsv.ens-cachan.fr/~goubault/H1.dist/H1.1/Doc/h1003.html + ''' + Someone in Dreadsbury Mansion killed Aunt Agatha. + Agatha, the butler, and Charles live in Dreadsbury Mansion, and + are the only ones to live there. A killer always hates, and is no + richer than his victim. Charles hates noone that Agatha hates. Agatha + hates everybody except the butler. The butler hates everyone not richer + than Aunt Agatha. The butler hates everyone whom Agatha hates. + Noone hates everyone. Who killed Agatha? + ''' + + Originally from F. J. Pelletier: + Seventy-five problems for testing automatic theorem provers. + Journal of Automated Reasoning, 2: 216, 1986. + + Note1: Since Google CP Solver/Pythons (currently) don't have + special support for logical operations on decision + variables (i.e. ->, <->, and, or, etc), this model + use some IP modeling tricks. + + Note2: There are 8 different solutions, all stating that Agatha + killed herself + + Compare with the following models: + * Choco : http://www.hakank.org/choco/WhoKilledAgatha.java + * Choco : http://www.hakank.org/choco/WhoKilledAgatha_element.java + * Comet : http://www.hakank.org/comet/who_killed_agatha.co + * ECLiPSE : http://www.hakank.org/eclipse/who_killed_agatha.ecl + * Gecode : http://www.hakank.org/gecode/who_killed_agatha.cpp + * JaCoP : http://www.hakank.org/JaCoP/WhoKilledAgatha.java + * JaCoP : http://www.hakank.org/JaCoP/WhoKilledAgatha_element.java + * MiniZinc: http://www.hakank.org/minizinc/who_killed_agatha.mzn + * Tailor/Essence': http://www.hakank.org/tailor/who_killed_agatha.eprime + * SICStus : http://hakank.org/sicstus/who_killed_agatha.pl + * Zinc :http://hakank.org/minizinc/who_killed_agatha.zinc + + + This model was created by Hakan Kjellerstrand (hakank@bonetmail.com) + Also see my other Google CP Solver models: http://www.hakank.org/google_or_tools/ +""" +from collections import defaultdict + +from constraint_solver import pywrapcp + +def var_matrix_array(solver, rows, cols, lb, ub, name): + x = [] + for i in range(rows): + t = [] + for j in range(cols): + t.append(solver.IntVar(lb, ub, '%s[%i,%i]'%(name, i,j))) + x.append(t) + return x + +def flatten_matrix(solver, m, rows, cols): + return [m[i][j] for i in range(rows) for j in range(cols)] + + +def print_flat_matrix(m_flat, rows, cols): + for i in range(rows): + for j in range(cols): + print m_flat[i*cols+j].Value(), + print + print + + +def main(the_killers): + + # Create the solver. + solver = pywrapcp.Solver('Who killed agatha?') + + # + # data + # + n = 3 + agatha = 0 + butler = 1 + charles = 2 + + # + # declare variables + # + the_killer = solver.IntVar(0,2, 'the_killer') + the_victim = solver.IntVar(0,2, 'the_victim' ) + + hates = var_matrix_array(solver, n, n, 0, 1, 'hates') + richer = var_matrix_array(solver, n, n, 0, 1, 'richer') + + hates_flat = flatten_matrix(solver, hates, n, n) + richer_flat = flatten_matrix(solver, richer, n, n) + + # + # constraints + # + + # Agatha, the butler, and Charles live in Dreadsbury Mansion, and + # are the only ones to live there. + + # A killer always hates, and is no richer than his victim. + # solver.Add(hates[the_killer, the_victim] == 1) + solver.Add(solver.Element(hates_flat,the_killer*n+the_victim) == 1) + + # solver.Add(richer[the_killer, the_victim] == 0) + solver.Add(solver.Element(richer_flat,the_killer*n+the_victim) == 0) + + # define the concept of richer: no one is richer than him-/herself + for i in range(n): + solver.Add(richer[i][i] == 0) + + # (contd...) if i is richer than j then j is not richer than i + # (i != j) => (richer[i,j] = 1) <=> (richer[j,i] = 0), + for i in range(n): + for j in range(n): + if i != j: + bi = solver.IsEqualCstVar(richer[i][j], 1) + bj = solver.IsEqualCstVar(richer[j][i], 0) + solver.Add(bi == bj) + + # Charles hates noone that Agatha hates. + #forall i : Range . + # (hates[agatha, i] = 1) => (hates[charles, i] = 0), + for i in range(n): + b1a = solver.IsEqualCstVar(hates[agatha][i], 1) + b1b = solver.IsEqualCstVar(hates[charles][i], 0) + solver.Add(b1a-b1b <= 0) + + # Agatha hates everybody except the butler. + solver.Add(hates[agatha][charles] == 1) + solver.Add(hates[agatha][agatha] == 1) + solver.Add(hates[agatha][butler] == 0) + + + # The butler hates everyone not richer than Aunt Agatha. + # forall i : Range . + # (richer[i, agatha] = 0) => (hates[butler, i] = 1), + for i in range(n): + b2a = solver.IsEqualCstVar(richer[i][agatha], 0) + b2b = solver.IsEqualCstVar(hates[butler][i], 1) + solver.Add(b2a-b2b<=0) + + + # The butler hates everyone whom Agatha hates. + #forall i : Range . + # (hates[agatha, i] = 1) => (hates[butler, i] = 1), + for i in range(n): + b3a = solver.IsEqualCstVar(hates[agatha][i], 1) + b3b = solver.IsEqualCstVar(hates[butler][i], 1) + solver.Add(b3a-b3b <= 0) + + + # Noone hates everyone. + # forall i : Range . + # (sum j : Range . hates[i,j]) <= 2, + for i in range(n): + solver.Add(solver.Sum([hates[i][j] for j in range(n)]) <= 2) + + + # Who killed Agatha? + solver.Add(the_victim == agatha) + + # + # solution and search + # + solution = solver.Assignment() + solution.Add(the_killer) + solution.Add(the_victim) + solution.Add(hates_flat) + solution.Add(richer_flat) + + # db: DecisionBuilder + db = solver.Phase(hates_flat + richer_flat, + solver.CHOOSE_FIRST_UNBOUND, + solver.ASSIGN_MIN_VALUE) + + solver.NewSearch(db) + num_solutions = 0 + while solver.NextSolution(): + print "the_killer:", the_killer.Value() + the_killers[the_killer.Value()] += 1 + print "the_victim:", the_victim.Value() + print "hates:" + print_flat_matrix(hates_flat,n,n) + print "richer:" + print_flat_matrix(richer_flat,n,n) + print + num_solutions += 1 + + solver.EndSearch() + + print + print "num_solutions:", num_solutions + print "failures:", solver.failures() + print "branches:", solver.branches() + print "wall_time:", solver.wall_time() + + +the_killers = defaultdict(int) +p = ["agatha", "butler", "charles"] +if __name__ == '__main__': + main(the_killers) + + print "\n" + for k in the_killers: + print "the killer %s was choosen in %i solutions" % (p[k], the_killers[k])