zebra puzzle

         Zebra Puzzle Brute Force Finder

A. Second Edition
In <The Matrix>, Morpheus said to Neo that there was a big difference between knowing the path and waling through the path.
It seems fitting this scenario. To test a solution is always much easier than finding the solution. Let me tell you something
I figure out from this puzzle which I spent a lot time on it before. This is a permutation problem which means you are supposed
to find one sequence from all the permutation of a set. Usually this is not the hardest one. In my opinion, the partition and
combination problem is more difficult because it may spent more time to generate the combination and partition pattern. (I am
not very sure about it.)
Alright, here we go to walk the path!
B.The problem
Consider the following story:

In 5 houses, each with a different color, live 5 persons of different nationalities, each of whom prefer a different kind of chocolate, a different drink, and a different pet.

The following facts are given:
　 Your task is to answer the question "Where does the zebra live, and in which house do they drink water?"
  1. Solve this task by encoding the facts and the problem in propositional logic.
  2. Apply your propositional satisfiability tester to verify your claim and to compute a model.
    　
　
C.The idea of program
　

How do you find the solution if you already have a logic tester? The easiest and brainless work is to generate all pattern

to test them one by one. And since this is a permutation problem, I just generate all the permutation to test them. The

first quick version is done without even a brain job because when I finished I felt very hungry and realized that the

permutation is a little bit too many, say 120x120x... So, I did two thing next, finish my dinner with some rice and bread

and went for shopping while leaving the program running. It is quite to my surprise that there is a result when I came

back. Then with a quick scan I realized that something is wrong. Quite easily I figure out that the tester has a serious

stupid bug! Then I began to do the cheating job by reducing the permutation pattern with some knowledge from the problem.

Say, I will only generate "food" permutation with 'German at end, "color" permutation with 'Red at fourth position because

my "national" permutation is fixed with this sequence: '(Norwegian Spaniard Ukrainian English Japanese) which is also the

sequence of "number".

D.The major functions
　
E.Further improvement
Bugs are inevitable and I will update new versions asap.
　
F.File listing
1. zebra.txt
2. permutation.txt
3. bruteforce.txt
　
file name: zebra.txt
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;propositional logic tester for "zebra puzzle"
;;1. to run just (zebra solution) where solution is a vector of vector. The five vector in 
;;	solution is the five persons's data which is each a vector of sequence defined as 
;;	national, pet, color, number, chocolate, drink
;;2. Each data is assumed a string (except number) that begins with capital letter
;;3. There are two group of testers, single existence or double relation tester, so I divide them
;;	into two group for easy clarifications.
;;
;;author: nick huang  date: nov. 8, 2005
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;House   Color     Nationality   Animal    Beverage    Flower
;  1     Yellow    Norwegian     Fox       Water       Swiss
;  2     Blue      Ukrainian     Horse     Tea         American
;  3     Red       English       Snails    Milk        Belgian 
;  4     Ivory     Spaniard      Dog       O.J.        Canadian 
;  5     Green     Japanese      Zebra     Coffee      German 
;



(define Norwegian (vector 'Norwegian 'Fox   'Yellow 1 'Swiss    'Water))
(define Ukrainian (vector 'Ukrainian 'Horse 'Blue   2 'American 'Tea))
(define English   (vector 'English   'Snail 'Red    3 'Belgian  'Milk))
(define Spaniard  (vector 'Spaniard  'Dog   'Ivory  4 'Canadian 'Juice))
(define Japanese  (vector 'Japanese  'Zebra 'Green  5 'German   'Coffee))

(define solution (vector Norwegian Ukrainian English Spaniard Japanese))

;this defines the sequence of data in vector
;VERY IMPORTANT: I assume data is a string starting with capital letter like 'Canadian , 'Tea
(define national 0)
(define pet 1)
(define color 2)
(define number 3)
(define chocolate 4)
(define drink 5)



;assume f1 is to the left of f2
;we can filter those irrelevent conditions
(define immediateneighbourcheck
	(lambda (ls f1 f2)
		(if (null? ls)
			#f
			(let ((num (vector-ref (car ls) number))) 
				;then we need to check if f2 is to left of f1
				(if (f1 (car ls))
					(dorightneighbour (cdr ls) f2 num)
					(if (f2 (car ls))
						(doleftneighbour (cdr ls) f1 num)
						(immediateneighbourcheck (cdr ls) f1 f2)
					)
				)
			)
		)
	)
)



(define neighbourwraper
	(lambda (f num)
		(lambda (v)
			(and (f v)(= (vector-ref v number) num))
		)
	)
)

(define doleftneighbour
	(lambda (ls f num)
		(begin ;(pp (list "doleftneighbour ls=" ls "f=" f  "num=" num))
		(if (= num 1)
			#f
			(begin ;;(pp "before neighbourwrapper ")
			(foreach ls (neighbourwraper f (- num 1)))
			)
		))
	)
)

(define dorightneighbour
	(lambda (ls f num)
		(begin ;(pp (list "dorightneighbour num=" num))
		(if (= num 5)
			#f
			(foreach ls (neighbourwraper f (+ num 1)))
		))
	)
)

(define doneighbour
	(lambda (ls f num)
		(begin ;(pp (list "doneighbour ls=" ls "f=" f "num=" num)) 
		(if (doleftneighbour ls f num)
			#t
			(dorightneighbour ls f num)
		))	
	)
)


;filter the irrelevent node which satisfy none of two conditions
(define doneighbourcheck
	(lambda (ls f1 f2)
		(if (null? ls)
			#f
			(let ((num (vector-ref (car ls) number))) 
				;the two condition are equivalent, no order restriction
				(if (f1 (car ls))
					(doneighbour (cdr ls) f2 num)
					(if (f2 (car ls))
						(doneighbour (cdr ls) f1 num)
						(doneighbourcheck (cdr ls) f1 f2)
					)
				)
			)
		)
	)
)

(define neighbourcheck
	(lambda (vv f1 f2)
		(doneighbourcheck (vector->list vv) f1 f2)
	)
)
			

(define check
	(lambda (index value)
		(lambda (v)
			(eq? (vector-ref v index) value)
		)
	)
)

(define foreach
	(lambda (ls f)
		(if (null? ls)
			#f
			(if (f (car ls))
				;(begin (pp(list "foreach check of car ls=" (car ls)))
				#t;)
				(foreach (cdr ls) f)
			)
		)
	)
)

(define existcheck
	(lambda (vv f)
		(foreach (vector->list vv) f)
	)
)


		

	
;The Englishman lives in the red house. 
(define check1
	(lambda (v)
		(and ((check national 'English) v)((check color 'Red) v))
	)
)

;The Spaniard owns a dog. 
(define check2
	(lambda (v)
		(and ((check national 'Spaniard) v)((check pet 'Dog) v))
	)
)

;The Norwegian lives in the first house on the left. 
(define check3
	(lambda (v)
		(and ((check national  'Norwegian) v)((check number 1) v))
	)
)

;Swiss chocolate is eaten in the yellow house.
(define check4
	(lambda (v)
		(and ((check chocolate 'Swiss) v)((check color 'Yellow) v))
	)
)


;The man who eats american chocolate lives in the house next to the man with the fox.
(define check5
	(lambda (vv)
		(neighbourcheck vv (check chocolate 'American) (check pet 'Fox))
	)
)

	
;The Norwegian lives next to the blue house.
(define check6
	(lambda (vv)
		(neighbourcheck vv (check national 'Norwegian)(check color 'Blue))
	)
)

;The person who eats belgian chocolate owns snails
(define check7
	(lambda (v)
		(and ((check chocolate 'Belgian) v)((check pet 'Snail) v))
	)
)

;The person who drinks orange juice eats canadian chocolate
(define check8
	(lambda (v)
		(and ((check drink 'Juice) v)((check chocolate 'Canadian) v))
	)
)

;The Ukrainian drinks tea. 
(define check9
	(lambda (v)
		(and ((check national 'Ukrainian) v)((check drink 'Tea) v))
	)
)

;The Japanese eats german chocolate.
(define check10
	(lambda (v)
		(and ((check national 'Japanese) v)((check chocolate 'German) v))
	)
)

;Swiss chocolate is eaten in the house next to the house where the horse is kept. 
(define check11
	(lambda (vv)
		(neighbourcheck vv (check chocolate 'Swiss)(check pet 'Horse))
	)
)

;Coffee is drunk in the green house. 
(define check12
	(lambda (v)
		(and ((check drink 'Coffee) v)((check color 'Green) v))
	)
)

;The green house is immediately to the right (your right) of the ivory house
(define check13
	(lambda (vv)
		; immediateneighbourcheck assumes the sequence of param is their sequence
		; i.e. first condition is left and second condition is on right
		(immediateneighbourcheck (vector->list vv) (check color 'Ivory)(check color 'Green))
	)
)

;Milk is drunk in the middle house. 
(define check14
	(lambda (v)
		(and ((check drink 'Milk) v) ((check number 3) v))
	)
)


;some conditions checking is just an existence check
(define singlecheck
	(lambda (vv)		
		(and (existcheck vv check1)(existcheck vv check2)
			(existcheck vv check3)(existcheck vv check4)
			(existcheck vv check7)(existcheck vv check8)
			(existcheck vv check9)(existcheck vv check10)
			(existcheck vv check12)(existcheck vv check14)
		)
	)
)

(define doublecheck
	(lambda (vv)
		(and (check5 vv)(check6 vv)(check11 vv)(check13 vv))		
	)
)


;;this is the all checking and assume solution is a double-dimension vector
;;i.e. (vector English Norwegian ...) where Englis is (vector national pet color ...)
;;for example, the vector Japanese might look like this:
;;(define Japanese (vector 'Japanese 'Zebra 'Green 3 'Canadian 'Tea))

;;And then you place all five person vector into a vector solution:
;;(define solution (vector Japanese English ...)

;;To run the testing, just
;;(zebra solutionname)

(define zebra
	(lambda (solution)
		(and (singlecheck solution)(doublecheck solution))
	)
)



file name: permutation.txt
(define foreach_op
	(lambda (f)
		(lambda (ls)
			(if   (null? ls)
				'()
				(cons (f (car ls)) ((foreach_op f) (cdr ls)))
			)
		)
	)
)
	
; (define splitlist
;	(lambda (ls)
;		(lambda (ls lst)
;			(if (null? lst)
;				(cons ls '()
;			
		
(define findhead_n
	(lambda (ls n)
		(if (null? ls)
			'()
			(if (= n 0)
				'()
				(cons (car ls) (findhead_n (cdr ls) (- n 1)))
			)
		)
	)
)

(define findtail_n
	(lambda (ls n)
		(if (null? ls)
			'()
			(if (= n 0)
				ls
				(findtail_n (cdr ls) (- n 1))
			)
		)
	)
)

(define concat 
	(lambda (ls1 ls2)
		(if (null? ls1)
			ls2
			(cons (car ls1) (concat (cdr ls1) ls2))
		)
	)
)

(define doinsertlist
	(lambda (ls x n)
		(if (= n 0) 
			(list (cons x ls))
			(cons (concat (findhead_n ls n) (cons x (findtail_n ls n) ) ) 
				(doinsertlist ls x (- n 1))
			)
		)	
	)
)

(define insertlist
	(lambda (x ls)
		(doinsertlist ls x (length ls))
		
	)
)

(define insertlistop
	(lambda (x)
		(lambda (ls)
			(insertlist x ls)
		)
	)
)
				
;(define dopermutation
;	(lambda (x ls)
;		(if (null? ls)
;			(list (list x))
;			(insertlist x (dopermutation x (cdr ls)))
;			;(foreach (insertlistop x) (dopermutation x (cdr ls)))
;		)
;	)
;)

(define concatlist
	(lambda (ls)
		(if (null? ls)
			'()
			(concat (car ls) (concatlist (cdr ls)))
		)
	)
)

(define permutation
	(lambda (ls)
		(if (null? (cdr ls))
			(list ls)
			(concatlist ((foreach_op (insertlistop (car ls))) (permutation (cdr ls))))
		)
	)
)
			
　
file name: bruteforce.txt

(load "zebra.txt")
(load "permutation.txt")

(define mylist '(1 2 3 4 5))

(define nationallist '(Norwegian Spaniard Ukrainian English Japanese))
(define animallist '(Fox Zebra Horse Snail Dog ))
(define colorlist '(Yellow Red Ivory Green Blue))
(define numberlist '(1 2 3 4 5))
(define foodlist '(Belgian Canadian German Swiss American))
(define drinklist '(Water Juice Tea Water Coffee Milk))

(define test '((Japanese Spaniard English Ukrainian Norwegian)
  (Dog Snail Horse Zebra Fox)
  (Blue Green Yellow Ivory Red)
  (1 5 3 4 2)
  (German Belgian American Swiss Canadian)
  (Water Coffee Milk Tea Juice Water))
)

(define addfirst
	(lambda (x)
		(lambda (ls)
			(cons x ls)
		)
	)
)

(define addsecond
	(lambda (x)
		(lambda (ls)
			(cons (car ls)(cons x (cdr ls)))
		)
	)
)

(define addthird
	(lambda (x)
		(lambda (ls)
			(cons (car ls)(cons (cadr ls)(cons x (cddr ls))))
		)
	)
)

(define addfourth
	(lambda (x)
		(lambda (ls)
			(cons (car ls)(cons (cadr ls)(cons (caddr ls)(cons x (cdddr ls)))))
		)
	)
)

(define addend
	(lambda (x)
		(lambda (ls)
			(append ls (list x))
		)
	)
)

(define permnational 
	(lambda ()
		(list nationallist)
	)
)

(define permanimal
	(lambda ()
		(map (addsecond 'Dog) (permutation '(Fox Zebra Horse Snail)))
	)
)

(define permdrink
	(lambda ()
		(map (addthird 'Tea) (permutation '(Water Juice Water Coffee Milk)))
	)
)

(define permcolor
	(lambda ()
		(map (addfourth 'Red)(permutation '(Yellow Ivory Green Blue)))
	)
)
	
(define permnumber
	(lambda ()
		(map (addfirst 1)(permutation '(2 3 4 5)))
	)
)

(define permfood
	(lambda ()
		(map (addend 'German) (permutation '(Belgian Canadian Swiss American)))
	)
)

(define bruteforce 
	(lambda ()
		(dobruteforce (permnational)(permanimal)(permcolor)(permnumber)(permfood)(permdrink))
	)
)

;nationperm animalperm colorperm numberperm foodperm drinkperm

(define dobruteforce
	(lambda (nationperm animalperm colorperm numberperm foodperm drinkperm)
		(if (null? drinkperm)
			(dobruteforce nationperm animalperm colorperm numberperm (cdr foodperm) 
				(permdrink))
			(if (null? foodperm)
				(dobruteforce nationperm animalperm colorperm (cdr numberperm) (permfood)
					drinkperm)
				(if (null? numberperm)
					(dobruteforce nationperm animalperm (cdr colorperm)  (permnumber) 
						foodperm drinkperm)
					(if (null? colorperm)
						(dobruteforce nationperm (cdr animalperm) (permcolor) numberperm 
							foodperm drinkperm)
						(if (null? animalperm)
							(dobruteforce (cdr nationperm)  (permanimal) colorperm 
								numberperm foodperm	drinkperm)
							(if (null? nationperm)
								#f
								(if (checkchoice (car nationperm)(car animalperm)(car colorperm)
									(car numberperm)(car foodperm)(car drinkperm))
									(makechoice (car nationperm)(car animalperm)(car colorperm)
										(car numberperm)(car foodperm)(car drinkperm))
									(dobruteforce nationperm animalperm colorperm numberperm foodperm 
										(cdr drinkperm))
								)
							)
						)
					)
				)
			)
		)
	)
)

(define makechoice
	(lambda (nationchoice animalchoice colorchoice numberchoice foodchoice drinkchoice)
		(if (null? nationchoice);;all choices must be same length, so be null at same time
			'()
			(cons (vector (car nationchoice)(car animalchoice)(car colorchoice)(car numberchoice)
				(car foodchoice)(car drinkchoice)) 
				(makechoice (cdr nationchoice)(cdr animalchoice)(cdr colorchoice)(cdr numberchoice)
					(cdr foodchoice)(cdr drinkchoice))
			)
		)
	)
)

		

(define checkchoice 
	(lambda (nationchoice animalchoice colorchoice numberchoice foodchoice drinkchoice)
		(zebra  (list->vector (makechoice nationchoice animalchoice colorchoice
			numberchoice foodchoice drinkchoice))			
		)
	)
)
		
						
(define mytest (list->vector
	(makechoice (car test) (cadr test) (caddr test)(cadddr test)(cadr (cdddr test)) (caddr (cdddr test))))
)
　










The result is like following :



> (time (bruteforce))
(time (bruteforce))
2822929 ms real time
2822929 ms cpu time (2822929 user, 0 system)
552358 collections accounting for 648856 ms real time (648846 user, 0 system
)
286761554760 bytes allocated
no minor faults
no major faults
(#(Norwegian Fox Yellow 1 Swiss Water)
#(Spaniard Dog Ivory 4 Canadian Juice)
#(Ukrainian Horse Blue 2 American Tea)
#(English Snail Red 3 Belgian Milk)
#(Japanese Zebra Green 5 German Coffee))
>



			



				 back.gif (341 bytes)       up.gif (335 bytes)         next.gif (337 bytes)