A. First 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.)

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:
　

• The Englishman lives in the red house.
• The Spaniard owns a dog.
• The Norwegian lives in the first house on the left.
• Swiss chocolate is eaten in the yellow house.
• The man who eats american chocolate lives in the house next to the man with the fox.
• The Norwegian lives next to the blue house.
• The person who eats belgian chocolate owns snails.
• The person who drinks orange juice eats canadian chocolate.
• The Ukrainian drinks tea.
• The Japanese eats german chocolate.
  　
• Swiss chocolate is eaten in the house next to the house where the horse is kept.
• Coffee is drunk in the green house.
• The green house is immediately to the right (your right) of the ivory house.
• Milk is drunk in the middle house.

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

　

D.The major functions

I have not tested them.

E.Further improvement

Bugs are inevitable and I will update new versions asap.

F.File listing

1. zebra.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))
				#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)
		(if ((check national 'English) v)
			((check color 'Red) v)
			#t
		)
	)
)

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

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

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


;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))
	)
)

The result is like following :