Who Owns The Zebra?
June 16, 2009
We previously used John McCarthy’s amb operator to solve a logic problem, but as logic problems become more complicated, they are best solved using a logic programming language such as Prolog. There are several embeddings of Prolog in Scheme; the best-known is Kanren, as described in the book The Reasoned Schemer by Daniel P. Friedman, Welliam E. Byrd and Oleg Kiselyov. Our solution follows that of Nils Holm in his book Logic Programming in Scheme.
Logic programming languages have a vocabulary different than imperative or functional languages. In place of functions, logic programming languages offer relations. Logic programming languages have goals (sometimes called objectives) that either succeed or fail. Rather than evaluating expressions, computation in logic programming languages proceeds by unification, in which the variables of two expressions are bound in a consistent manner.
Here is Holm’s solution to the zebra puzzle:
(define (zebra)
(fresh (h)
(run* (h)
(all (== h (list (list 'norwegian (_) (_) (_) (_)) ; 10
(_)
(list (_) (_) 'milk (_) (_)) ; 9
(_)
(_)))
(memo (list 'englishman (_) (_) (_) 'red) h) ; 2
(lefto (list (_) (_) (_) (_) 'green) ; 6
(list (_) (_) (_) (_) 'ivory) h) ; 6
(nexto (list 'norwegian (_) (_) (_) (_)) ; 15
(list (_) (_) (_) (_) 'blue) h) ; 15
(memo (list (_) 'kools (_) (_) 'yellow) h) ; 8
(memo (list 'spaniard (_) (_) 'dog (_)) h) ; 3
(memo (list (_) (_) 'coffee (_) 'green) h) ; 4
(memo (list 'ukrainian (_) 'tea (_) (_)) h) ; 5
(memo (list (_) 'luckystrikes 'orangejuice (_) (_)) h) ; 13
(memo (list 'japanese 'parliaments (_) (_) (_)) h) ; 14
(memo (list (_) 'oldgolds (_) 'snails (_)) h) ; 7
(nexto (list (_) (_) (_) 'horse (_)) ; 12
(list (_) 'kools (_) (_) (_)) h) ; 12
(nexto (list (_) (_) (_) 'fox (_)) ; 11
(list (_) 'chesterfields (_) (_) (_)) h) ; 11
(memo (list (_) (_) 'water (_) (_)) h)
(memo (list (_) (_) (_) 'zebra (_)) h)))))
There are four goals: == performs unification, memo tests whether a list contains a particular element, lefto checks if one element is immediately to the left of another in a list, and nexto checks if one element is immediately adjacent to another in a list (by convention, goals are spelled with names that end in the letter o). All is an operator that succeeds only if all its sub-goals succeed. Run* is the interface between normal Scheme and the logic extensions; (run* (h) ...) displays the unification of h, which is not a Scheme variable but a logic variable. Fresh creates a new logical environment and defines h as a logic variable, in a manner similar to the let syntax of normal Scheme.
The == and memo goals are part of the standard system, but lefto and nexto are specific to the zebra puzzle:
(define (lefto x y l)
(fresh (d)
(any (all (caro l x)
(cdro l d)
(caro d y))
(all (cdro l d)
(lefto x y d)))))
(define (nexto x y l)
(any (lefto x y l)
(lefto y x l)))
Thus, the body of zebra is an all operator that succeeds when all of its sub-objectives succeed. The first objective unifies the logic variable h with a list of houses, each represented as a five-element list of nationality, cigarette, drink, pet, and house color. Each fact of the puzzle is encoded as a goal; for instance, the second goal constrains the englishman to live in the red house, and the third goal constrains the ivory house to be to the left of the green house. The last two goals mention water and the zebra, because they do not appear in any of the other goals.
The solution takes less than a second:
> (zebra)
((norwegian kools water fox yellow)
(ukrainian chesterfields tea horse blue)
(englishman oldgolds milk snails red)
(japanese parliaments coffee zebra green)
(spaniard luckystrikes orangejuice dog ivory))
The norwegian drinks water. The japanese owns the zebra.
The complete code, including the logic primitives, is given at http://programmingpraxis.codepad.org/408Ehwhb (you should be aware that it uses a later version of the logic primitives than the book). Wikipedia provides more information about the zebra puzzle, including a complete solution by deduction, without a computer.
Programming Praxis 
There’s a slight error in your code: you have the ivory house to the right of the green house instead of the other way round. Flipping the constraint for number 6 around should fix it.
[…] Praxis – Who Owns The Zebra? By Remco Niemeijer In Today’s Programming Praxis problem we have to solve a logic puzzle. The provided solution uses a 182-line […]
My Haskell solution (see http://bonsaicode.wordpress.com/2009/06/16/programming-praxis-who-owns-the-zebra/ for a version with comments):
import Data.List
import qualified Data.Map as M
type Grid = M.Map String (M.Map Int [String])
data Constraint = Link (String, String) (String, String)
| PosLink (String, String) Int
| NextTo (String, String) (String, String)
| RightOf (String, String) (String, String)
deriving Eq
type Solver = ([Constraint], Grid)
addConstraint :: Constraint -> Solver -> Solver
addConstraint c (cs, g) = (c : cs, g)
removeIf :: (String, String) -> (String, String) ->
[String -> String -> Int -> Grid -> Bool] -> Grid -> Grid
removeIf (f1, v1) (f2, v2) cs g = M.adjust (M.mapWithKey (\k ->
if and [c f1 v1 k g | c <- cs] then delete v2 else id)) f2 g notAt :: (Int -> Int) -> String -> String -> Int -> Grid -> Bool
notAt f f1 v1 i g = M.notMember (f i) (g M.! f1) ||
notElem v1 (g M.! f1 M.! (f i))
runConstraint :: Constraint -> Grid -> Grid
runConstraint (Link a b) = removeIf a b conds . removeIf b a conds
where conds = [(\f1 v1 k -> notElem v1 . (M.! k) . (M.! f1))]
runConstraint (PosLink (f1,v1) i) =
M.adjust (M.update (const $ Just [v1]) i) f1
runConstraint (NextTo a b) = removeIf a b [notAt pred, notAt succ]
runConstraint (RightOf a b) = removeIf a b [notAt pred] .
removeIf b a [notAt succ]
adjustOthers :: Eq k => (v -> v) -> k -> M.Map k v -> M.Map k v
adjustOthers f k = M.mapWithKey (\k’ v -> if k’ == k then v else f v)
simplify :: Grid -> Grid
simplify g = foldr ($) (M.mapWithKey (\_ v ->
M.mapWithKey (\i x -> let d = x \\ concat (M.elems $ M.delete i v)
in if length d == 1 then d else x) v) g)
[ M.adjust (adjustOthers (\\ take 1 x) i) f
| (f, v) <- M.assocs g, (i, x) <- M.assocs v, length x == 1] run :: Solver -> Solver
run (cs, g) = (cs, simplify $ foldr runConstraint g cs)
apply :: Solver -> Solver
apply = head . head . dropWhile (null . tail) . group . iterate run
solved :: M.Map k (M.Map k’ [v]) -> Bool
solved g = and [False | (_, v) <- M.assocs g, (_, xs) <- M.assocs v, length xs /= 1] solve :: Solver -> [String]
solve s = map (unwords . map head) . transpose . map (M.elems) .
M.elems $ head [ r | let (cs, g) = apply s,
(f, v) <- M.assocs $ g, (i, xs) <- M.assocs v, x <- xs, let (_, r) = apply (cs, M.adjust (M.adjust (const [x]) i) f g), solved r ] grid :: Grid grid = M.fromList . zip (words "owner brand drink pet color") $ map (M.fromList . zip [1..] . replicate 5) [words "Englishman Ukranian Norwegian Japanese Spaniard", words "Old_Gold Kools Chesterfields Lucky_Strike Parliaments", words "Coffee Tea Milk Orange_Juice Water", words "Dog Snails Horse Fox Zebra", words "Red Green Ivory Yellow Blue"] problem :: Solver problem = foldr addConstraint ([], grid) [Link ("owner", "Englishman") ("color", "Red"), Link ("owner", "Spaniard") ("pet", "Dog"), Link ("drink", "Coffee") ("color", "Green"), Link ("owner", "Ukranian") ("drink", "Tea"), RightOf ("color", "Ivory") ("color", "Green"), Link ("brand", "Old_Gold") ("pet", "Snails"), Link ("brand", "Kools") ("color", "Yellow"), PosLink ("drink", "Milk") 3, PosLink ("owner", "Norwegian") 1, NextTo ("brand", "Chesterfields") ("pet", "Fox"), NextTo ("brand", "Kools") ("pet", "Horse"), Link ("brand", "Lucky_Strike") ("drink", "Orange_Juice"), Link ("owner", "Japanese") ("brand", "Parliaments"), NextTo ("owner", "Norwegian") ("color", "Blue")] main :: IO () main = mapM_ putStrLn $ solve problem [/sourcecode]
A more elegant solution (see http://bonsaicode.wordpress.com/2009/06/22/who-owns-the-zebra-reloaded/ for more detail):
import Data.List
indexOf :: (Eq a) => [a] -> a -> Int
indexOf xs x = head $ elemIndices x xs
nextTo :: Int -> Int -> Bool
nextTo a b = abs (a – b) == 1
rightOf :: Int -> Int -> Bool
rightOf a b = a == b + 1
options :: String -> [[String]]
options = permutations . words
solution :: [[String]]
solution = head [transpose [cs, os, ds, ss, ps] |
cs <- options "red green ivory yellow blue", let color = indexOf cs, color "green" `rightOf` color "ivory", os <- options "english spaniard ukranian norwegian japanese", let owner = indexOf os, owner "norwegian" == 0, owner "english" == color "red", owner "norwegian" `nextTo` color "blue", ds <- options "coffee tea milk juice water", let drinks = indexOf ds, drinks "milk" == 2, drinks "coffee" == color "green", owner "ukranian" == drinks "tea", ss <- options "old_gold kools chesterfields parliaments lucky_strike", let smokes = indexOf ss, smokes "kools" == color "yellow", smokes "lucky_strike" == drinks "juice", owner "japanese" == smokes "parliaments", ps <- options "dog snails fox horse zebra", let pet = indexOf ps, owner "spaniard" == pet "dog", smokes "old_gold" == pet "snails", smokes "chesterfields" `nextTo` pet "fox", smokes "kools" `nextTo` pet "horse"] main :: IO () main = mapM_ print solution [/sourcecode]
One I did in Python 3.0.1, using the stadard library’s itertools module for the permutations:
Here’s the pastebin:
http://pastebin.com/f41c6cbf8