Last active
March 24, 2018 02:10
-
-
Save vigov5/c4725b095adbb5ea6c92cf4f92440e4d to your computer and use it in GitHub Desktop.
Solver and Problem Generator for Old Riddle task of Code War 2017 - Online Round
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| from z3 import * | |
| import random | |
| # http://www.mensus.net/brain/logic.shtml?code=9FFFFE.113260F1 | |
| Toyota,Renault,Volvo,Porsche,Ferrari,RollsRoyce,VW = Ints('Toyota Renault Volvo Porsche Ferrari RollsRoyce VW') | |
| brown,red,pink,black,green,gray,blue = Ints('brown red pink black green gray blue') | |
| coffee,lemonade,milk,icetea,espresso,soda,wine = Ints('coffee lemonade milk icetea espresso soda wine') | |
| orchids,lilies,crocuses,hyacinth,tulips,cactuses,dahlias = Ints('orchids lilies crocuses hyacinth tulips cactuses dahlias') | |
| chocolate,cheese,eggs,potatoes,spaghetties,cookies,steaks = Ints('chocolate cheese eggs potatoes spaghetties cookies steaks') | |
| Italian,Swede,Spanish,Swiss,British,Greek,German = Ints('Italian Swede Spanish Swiss British Greek German') | |
| cats,mice,horses,dogs,snakes,turtles,tortoises = Ints('cats mice horses dogs snakes turtles tortoises') | |
| Cubans,Bluemaster,Pall,Chersterfields,Prince,Dunhill,Marlboro = Ints('Cubans Bluemaster Pall Chersterfields Prince Dunhill Marlboro') | |
| Baseball,Basketball,Tennis,Rugby,Badminton,IceHockey,Lacrosse = Ints('Baseball Basketball Tennis Rugby Badminton IceHockey Lacrosse') | |
| redwoods,pines,palm,birch,nut,willows,eucalyptus = Ints('redwoods pines palm birch nut willows eucalyptus') | |
| s = Solver() | |
| s.add(Distinct(Toyota,Renault,Volvo,Porsche,Ferrari,RollsRoyce,VW)) | |
| s.add(Distinct(brown,red,pink,black,green,gray,blue)) | |
| s.add(Distinct(coffee,lemonade,milk,icetea,espresso,soda,wine)) | |
| s.add(Distinct(orchids,lilies,crocuses,hyacinth,tulips,cactuses,dahlias)) | |
| s.add(Distinct(chocolate,cheese,eggs,potatoes,spaghetties,cookies,steaks)) | |
| s.add(Distinct(Italian,Swede,Spanish,Swiss,British,Greek,German)) | |
| s.add(Distinct(cats,mice,horses,dogs,snakes,turtles,tortoises)) | |
| s.add(Distinct(Cubans,Bluemaster,Pall,Chersterfields,Prince,Dunhill,Marlboro)) | |
| s.add(Distinct(Baseball,Basketball,Tennis,Rugby,Badminton,IceHockey,Lacrosse)) | |
| s.add(Distinct(redwoods,pines,palm,birch,nut,willows,eucalyptus)) | |
| tmp = [ | |
| 'Toyota Renault Volvo Porsche Ferrari RollsRoyce VW', | |
| 'brown red pink black green gray blue', | |
| 'coffee lemonade milk icetea espresso soda wine', | |
| 'orchids lilies crocuses hyacinth tulips cactuses dahlias', | |
| 'chocolate cheese eggs potatoes spaghetties cookies steaks', | |
| 'Italian Swede Spanish Swiss British Greek German', | |
| 'cats mice horses dogs snakes turtles tortoises', | |
| 'Cubans Bluemaster Pall Chersterfields Prince Dunhill Marlboro', | |
| 'Baseball Basketball Tennis Rugby Badminton IceHockey Lacrosse', | |
| 'redwoods pines palm birch nut willows eucalyptus', | |
| ] | |
| for l in tmp: | |
| for k in l.split(" "): | |
| eval("s.add(%s>=1, %s<=7)" % (k, k)) | |
| # There are two houses between the crocuses and the cats. | |
| s.add(Or(crocuses==cats+3, crocuses==cats-3)) | |
| # The person drinking soda lives directly to the right of the gray house. | |
| s.add(soda==gray+1) | |
| # The person smoking Chersterfields lives directly to the right of the person eating steaks. | |
| s.add(Chersterfields==steaks+1) | |
| # The horses live directly to the left of the person drinking coffee. | |
| s.add(horses==coffee-1) | |
| # The person with birch trees has cats. | |
| s.add(birch==cats) | |
| # There is one house between the redwoods and the snakes. | |
| s.add(Or(redwoods==snakes+2, redwoods==snakes-2)) | |
| # The person eating potatoes lives directly next to the brown house. | |
| s.add(Or(potatoes==brown+1, potatoes==brown-1)) | |
| # There is one house between the Tennis player and the person eating spaghetties on the right | |
| s.add(Tennis==spaghetties-2) | |
| # There is one house between the Swede and the driver of the Porsche. | |
| s.add(Or(Swede==Porsche+2, Swede==Porsche-2)) | |
| # The cactuses grow in front of house four. | |
| s.add(cactuses==4) | |
| # There are two houses between the black and pink house on the right | |
| s.add(black==pink-3) | |
| # The dahlias grow to the right of the person drinking icetea. | |
| s.add(dahlias>icetea) | |
| # There is one house between the Rugby player and the person eating eggs on the right | |
| s.add(Rugby==eggs-2) | |
| # The person playing Badminton smokes Prince. | |
| s.add(Badminton==Prince) | |
| # There is one house between the palm trees and the person smoking Cubans on the left | |
| s.add(palm==Cubans+2) | |
| # The person eating cheese lives to the left of the brown house. | |
| s.add(cheese<brown) | |
| # The turtles live directly to the right of the person smoking Chersterfields. | |
| s.add(Chersterfields==turtles-1) | |
| # There are two houses between the black house and the house the British lives in on the right | |
| s.add(black==British-3) | |
| # The eucalyptus trees do not grow in front of house four. | |
| s.add(eucalyptus!=4) | |
| # There are two houses between the German and the redwoods on the left | |
| s.add(redwoods==German-3) | |
| # The Renault driver lives directly next to Lacrosse player. | |
| s.add(Or(Renault==Lacrosse+1, Renault==Lacrosse-1)) | |
| # There are two houses between the VW driver and the person smoking Bluemaster on the left | |
| s.add(Bluemaster==VW-3) | |
| # The cats live directly next to the blue house. | |
| s.add(Or(cats==blue+1, cats==blue-1)) | |
| # There are two houses between the house of the person eating potatoes and the green house on the right | |
| s.add(potatoes==green-3) | |
| # The Rolls Royce driver lives to the right of the Volvo driver. | |
| s.add(RollsRoyce>Volvo) | |
| # The Swiss lives directly next to the Badminton player. | |
| s.add(Or(Swiss==Badminton+1, Swiss==Badminton-1)) | |
| # The Rugby player lives directly to the left of the person smoking Dunhill. | |
| s.add(Rugby==Dunhill-1) | |
| # The person in house three drinks milk. | |
| s.add(milk==3) | |
| # There are two houses between the Baseball player and the person drinking wine on the right | |
| s.add(Baseball==wine-3) | |
| # There are two houses between the tortoises and the dogs. | |
| s.add(Or(tortoises==dogs+3, tortoises==dogs-3)) | |
| # There is one house between the dogs and the person drinking lemonade. | |
| s.add(Or(dogs==lemonade+2, dogs==lemonade-2)) | |
| # There are two houses between the pink house and the house the Swede lives in on the left | |
| s.add(pink==Swede+3) | |
| # The British lives directly next to the orchids. | |
| s.add(Or(British==orchids+1, British==orchids-1)) | |
| # There is one house between the house where the tulips grow and the red house. | |
| s.add(Or(tulips==red+2, tulips==red-2)) | |
| # The person in house five does not drink wine. | |
| s.add(wine!=5) | |
| # There is one house between the cats and the person eating chocolate on the right | |
| s.add(cats==chocolate-2) | |
| # The VW driver lives directly to the left of the Ferrari driver. | |
| s.add(VW==Ferrari-1) | |
| # The Rolls Royce is not parked in front of house seven. | |
| s.add(RollsRoyce!=7) | |
| # There is one house between the crocuses and the cactuses. | |
| s.add(Or(crocuses==cactuses+2, crocuses==cactuses-2)) | |
| # There is one house between the German and the Marlboro smoking person. | |
| s.add(Or(German==Marlboro+2, German==Marlboro-2)) | |
| # There is one house between the willows and the person smoking Cubans on the right | |
| s.add(willows==Cubans-2) | |
| # There are two houses between the Lacrosse player and the person drinking coffee on the left | |
| s.add(coffee==Lacrosse-3) | |
| # The Italian lives in the blue house. | |
| s.add(Italian==blue) | |
| # There are two houses between the lilies and the Tennis player on the left | |
| s.add(Tennis==lilies-3) | |
| # There is one house between the Spanish and the driver of the VW on the left. | |
| s.add(VW==Spanish-2) | |
| # There are two houses between the turtles and the person eating eggs. | |
| s.add(Or(turtles==eggs+3, turtles==eggs-3)) | |
| # The Italian lives to the left of the Badminton player. | |
| s.add(Italian<Badminton) | |
| # There is one house between the lilies and the Ferrari. | |
| s.add(Or(lilies==Ferrari+2, lilies==Ferrari-2)) | |
| # The orchids grow to the left of the Basketball player. | |
| s.add(orchids<Basketball) | |
| # The nut trees grow directly next to the person drinking wine. | |
| s.add(Or(nut==wine+1, nut==wine-1)) | |
| r = s.check() | |
| print r | |
| if r==unsat: | |
| exit(0) | |
| m=s.model() | |
| print(m) | |
| result = { | |
| "dogs": 2, | |
| "eucalyptus": 6, | |
| "tulips": 5, | |
| "cheese": 1, | |
| "Swede": 1, | |
| "Ferrari": 5, | |
| "German": 5, | |
| "espresso": 5, | |
| "Basketball": 7, | |
| "hyacinth": 1, | |
| "steaks": 4, | |
| "Prince": 6, | |
| "IceHockey": 2, | |
| "red": 7, | |
| "orchids": 3, | |
| "Porsche": 3, | |
| "green": 5, | |
| "tortoises": 5, | |
| "chocolate": 5, | |
| "Cubans": 3, | |
| "icetea": 1, | |
| "lemonade": 4, | |
| "Volvo": 1, | |
| "snakes": 4, | |
| "Greek": 3, | |
| "crocuses": 6, | |
| "Marlboro": 7, | |
| "Renault": 6, | |
| "Toyota": 7, | |
| "brown": 3, | |
| "blue": 2, | |
| "wine": 6, | |
| "Lacrosse": 5, | |
| "gray": 6, | |
| "spaghetties": 6, | |
| "dahlias": 2, | |
| "pines": 4, | |
| "RollsRoyce": 2, | |
| "eggs": 3, | |
| "cookies": 7, | |
| "Swiss": 7, | |
| "Pall": 4, | |
| "nut": 7, | |
| "mice": 7, | |
| "Spanish": 6, | |
| "lilies": 7, | |
| "Italian": 2, | |
| "willows": 1, | |
| "Baseball": 3, | |
| "milk": 3, | |
| "Dunhill": 2, | |
| "potatoes": 2, | |
| "Bluemaster": 1, | |
| "VW": 4, | |
| "redwoods": 2, | |
| "British": 4, | |
| "turtles": 6, | |
| "palm": 5, | |
| "Badminton": 6, | |
| "Rugby": 1, | |
| "black": 1, | |
| "pink": 4, | |
| "cactuses": 4, | |
| "Tennis": 4, | |
| "birch": 3, | |
| "cats": 3, | |
| "horses": 1, | |
| "coffee": 2, | |
| "Chersterfields": 5, | |
| "soda": 7 | |
| } | |
| cs = [] | |
| mapping = {k:[] for k in ['a', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'k', 'l', 'n', 'o', 'p', 'r', 's', 't', 'u', 'w', 'y'] | |
| } | |
| for k, v in result.items(): | |
| if v < len(k): | |
| print k, k[v] | |
| mapping[k[v]].append(k) | |
| cs = list(set(cs)) | |
| flag = "notsoeasyhuh" | |
| print " + ".join(["'%s'[i%d]" % (random.choice(mapping[c]), idx) for idx,c in enumerate(flag)]) | |
| # CodeWar{'lemonade'[i0] + 'marlboro'[i1] + 'chersterfields'[i2] + 'tulips'[i3] + 'horses'[i4] + 'greek'[i5] + 'basketball'[i6] + 'cats'[i7] + 'hyacinth'[i8] + 'cheese'[i9] + 'cactuses'[i10] + 'orchids'[i11]} | |
| # i0..i11 is number of the hourse that have that object | |
| # CodeWar{notsoeasyhuh} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment