Constraint Satisfaction Problem

I'm struggling my way through Artificial Intelligence: A Modern Approach in order to alleviate my natural stupidity. In trying to solve some of the exercises, I've come up against the "Who Owns the Zebra" problem, Exercise 5.13 in Chapter 5. This has been a topic here on SO but the responses mostly addressed the question "how would you solve this if you had a free choice of problem solving software available?"

I accept that Prolog is a very appropriate programming language for this kind of problem, and there are some fine packages available, e.g. in Python as shown by the top-ranked answer and also standalone. Alas, none of this is helping me "tough it out" in a way as outlined by the book.

The book appears to suggest building a set of dual or perhaps global constraints, and then implementing some of the algorithms mentioned to find a solution. I'm having a lot of trouble coming up with a set of constraints suitable for modelling the problem. I'm studying this on my own so I don't have access to a professor or TA to get me over the hump - this is where I'm asking for your help.

I see little similarity to the examples in the chapter.

I was eager to build dual constraints and started out by creating (the logical equivalent of) 25 variables: nationality1, nationality2, nationality3, ... nationality5, pet1, pet2, pet3, ... pet5, drink1 ... drink5 and so on, where the number was indicative of the house's position.

This is fine for building the unary constraints, e.g.

The Norwegian lives in the first house:

nationality1 = { :norway }.

But most of the constraints are a combination of two such variables through a common house number, e.g.

The Swede has a dog:

nationality[n] = { :sweden } AND pet[n] = { :dog }

where n can range from 1 to 5, obviously. Or stated another way:

    nationality1 = { :sweden } AND pet1 = { :dog } 
XOR nationality2 = { :sw开发者_StackOverfloweden } AND pet2 = { :dog } 
XOR nationality3 = { :sweden } AND pet3 = { :dog } 
XOR nationality4 = { :sweden } AND pet4 = { :dog } 
XOR nationality5 = { :sweden } AND pet5 = { :dog } 

...which has a decidedly different feel to it than the "list of tuples" advocated by the book:

( X1, X2, X3 = { val1, val2, val3 }, { val4, val5, val6 }, ... )

I'm not looking for a solution per se; I'm looking for a start on how to model this problem in a way that's compatible with the book's approach. Any help appreciated.

There are several libraries for CSP solving:

• Gecode (C++)
• Choco (Java)
• clp(*) module in SICStus Prolog

And there are many more. These can be used for efficient constraint solving.

On the other hand if you want to implement your general constraint solver, an idea to implement a CSP Solver: build a constraint graph, where the nodes are the constraint variables and constraints the connections. For every variable store the possible domain, and build a notification mechanism. The constraints are notified when its related variables change, and then start a propagation process: by looking at the current values of the related variables reduce the domains of possible variables.

Propagation example:

• Variables (with domain): X - {1,2,3,4,5} - Y {1,2,3,4,5}
• Constraint: X + Y < 4
• When the constraint propagates, you can infer, that neither X nor Y can be 3, 4 nor 5, because then the constraint would fail, so the new domains are: X- {1,2} Y - {1,2}
• Now both domains of X and Y have changed the constraints listening to X and Y should be notified to propagate.

It is possible that propagation is not enough. In this case a backtracking/backjumping search is used: we try to select the value of a single variable, propagate the changes, etc.

This algorithm is considered quite fast while it is easy to understand. I have some implementation that solves our special case of problems very efficiently.

Thanks to everyone for some helpful information!

The hint I really needed came to me in a traffic jam. Rather than assigning nationalities, pets etc. to houses (variables named country1, country2, pet1, pet2), what I needed to do was assign houses to the elements of the domain! Example:

(9) norway = 1        ; unary constraint: The Norwegian lives in the 1st house
(2) britain = dog     ; binary constraint: Dog is in same house as the Brit
(4) green - ivory = 1 ; relative positions

This allowed me to find simple formulations for my constraints, like this:

(def constraints
  #{
   [:con-eq :england :red]
   [:con-eq :spain :dog]
   [:abs-pos :norway 1]
   [:con-eq :kools :yellow]
   [:next-to :chesterfields :fox]
   [:next-to :norway :blue]
   [:con-eq :winston :snails]
   [:con-eq :lucky :oj]
   [:con-eq :ukraine :tea]
   [:con-eq :japan :parliaments]
   [:next-to :kools :horse]
   [:con-eq :coffee :green]
   [:right-of :green :ivory]
   [:abs-pos :milk 3]
   })

I'm not done yet (puttering at this only part time) but I will post a complete solution once I work it out.

Update: About 2 weeks later, I've come up with a working solution in Clojure:

(ns houses
  [:use [htmllog] clojure.set]  
  )

(comment
  [ 1] The Englishman lives in the red house.
  [ 2] The Spaniard owns the dog.
  [ 3] The Norwegian lives in the first house on the left.
  [ 4] Kools are smoked in the yellow house.
  [ 5] The man who smokes Chesterfields lives in the house next to the man with the fox.
  [ 6] The Norwegian lives next to the blue house.
  [ 7] The Winston smoker owns snails.
  [ 8] The Lucky Strike smoker drinks orange juice.
  [ 9] The Ukrainian drinks tea.
  [10] The Japanese smokes Parliaments.
  [11] Kools are smoked in the house next to the house where the horse is kept.
  [12] Coffee is drunk in the green house.
  [13] The Green house is immediately to the right (your right) of the ivory house.
  [14] Milk is drunk in the middle house.

  “Where does the zebra live, and in which house do they drink water?”
)

(def positions #{1 2 3 4 5})

(def categories {
          :country #{:england :spain :norway :ukraine :japan}
          :color #{:red :yellow :blue :green :ivory}
          :pet #{:dog :fox :snails :horse :zebra}
          :smoke #{:chesterfield :winston :lucky :parliament :kool}
          :drink #{:orange-juice :tea :coffee :milk :water}
})

(def constraints #{
                    ; -- unary
          '(at :norway 1) ; 3
          '(at :milk 3) ; 14
                    ; -- simple binary
          '(coloc :england :red) ; 1
          '(coloc :spain :dog) ; 2
          '(coloc :kool :yellow) ; 4
          '(coloc :winston :snails) ; 7
          '(coloc :lucky :orange-juice) ; 8
          '(coloc :ukraine :tea) ; 9
          '(coloc :japan :parliament) ; 10
          '(coloc :coffee :green) ; 12
                    ; -- interesting binary
          '(next-to :chesterfield :fox) ; 5
          '(next-to :norway :blue) ; 6
          '(next-to :kool :horse) ; 11
          '(relative :green :ivory 1) ; 13
})

; ========== Setup ==========

(doseq [x (range 3)] (println))

(def var-cat    ; map of variable -> group 
      ; {:kool :smoke, :water :drink, :ivory :color, ... 
    (apply hash-map (apply concat 
        (for [cat categories vari (second cat)] 
      [vari (first cat)]))))

(prn "var-cat:" var-cat)

(def initial-vars    ; map of variable -> positions
      ; {:kool #{1 2 3 4 5}, :water #{1 2 3 4 5}, :ivory #{1 2 3 4 5}, ...
    (apply hash-map (apply concat 
        (for [v (keys var-cat)] [v positions]))))

(prn "initial-vars:" initial-vars)

(defn apply-unary-constraints
   "This applies the 'at' constraint. Separately, because it only needs doing once." 
   [vars]
   (let [update (apply concat
      (for [c constraints :when (= (first c) 'at) :let [[v d] (rest c)]]
   [v #{d}]))]
      (apply assoc vars update)))

(def after-unary (apply-unary-constraints initial-vars))

(prn "after-unary:" after-unary)

(def binary-constraints (remove #(= 'at (first %)) constraints))

(prn "binary-constraints:" binary-constraints)

; ========== Utilities ==========

(defn dump-vars
   "Dump map `vars` as a HTML table in the log, with `title`." 
   [vars title]
  (letfn [
        (vars-for-cat-pos [vars var-list pos]
          (apply str (interpose "<br/>" (map name (filter #((vars %) pos) var-list)))))]
      (log-tag "h2" title)
    (log "<table border='1'>")
    (log "<tr>")
    (doall (map #(log-tag "th" %) (cons "house" positions)))
    (log "</tr>")
    (doseq [cat categories]
      (log "<tr>")
          (log-tag "th" (name (first cat)))
          (doseq [pos positions]
          (log-tag "td" (vars-for-cat-pos vars (second cat) pos)))
      (log "</tr>")
      )
    (log "</table>")))

(defn remove-values
   "Given a list of key/value pairs, remove the values from the vars named by key." 
   [vars kvs]
   (let [names (distinct (map first kvs))
      delta (for [n names]
      [n (set (map second (filter #(= n (first %)) kvs)))])
      update (for [kv delta
         :let [[cname negative] kv]]
      [cname (difference (vars cname) negative)])]
      (let [vars (apply assoc vars (apply concat update))]
   vars)))

(defn siblings
   "Given a variable name, return a list of the names of variables in the same category."
   [vname]
   (disj (categories (var-cat vname)) vname))

(defn contradictory?
   "Checks for a contradiction in vars, indicated by one variable having an empty domain." 
   [vars]
   (some #(empty? (vars %)) (keys vars)))

(defn solved?
   "Checks if all variables in 'vars' have a single-value domain."
   [vars]
   (every? #(= 1 (count (vars %))) (keys vars)))

(defn first-most-constrained
   "Finds a variable having the smallest domain size > 1."
   [vars]
   (let [best-pair (first (sort (for [v (keys vars) :let [n (count (vars v))] :when (> n 1)] [n v])))]
      (prn "best-pair:" best-pair)
      (second best-pair)))   

;========== Constraint functions ==========

   (comment
      These functions make an assertion about the domains in map 'bvars', 
      and remove any positions from it for which those assertions do not hold. 
      They all return the (hopefully modified) domain space 'bvars'.)

   (declare bvars coloc next-to relative alldiff solitary)

   (defn coloc
      "Two variables share the same location." 
      [vname1 vname2]
      (if (= (bvars vname1) (bvars vname2)) bvars
   (do
      (let [inter (intersection (bvars vname1) (bvars vname2))]
         (apply assoc bvars [vname1 inter vname2 inter])))))

   (defn next-to 
      "Two variables have adjoining positions"
      [vname1 vname2]
      ; (prn "doing next-to" vname1 vname2)
      (let [v1 (bvars vname1) v2 (bvars vname2)
            bad1 (for [j1 v1 :when (not (or (v2 (dec j1)) (v2 (inc j1))))] [vname1 j1])
        bad2 (for [j2 v2 :when (not (or (v1 (dec j2)) (v1 (inc j2))))] [vname2 j2])
         allbad (concat bad1 bad2)]
   (if (empty? allbad) bvars 
      (do
         (remove-values bvars allbad)))))

   (defn relative
      "(position vname1) - (position vname2) = diff"  
      [vname1 vname2 diff]
      (let [v1 (bvars vname1) v2 (bvars vname2)
       bad1 (for [j1 v1 :when (not (v2 (- j1 diff)))] [vname1 j1])
         bad2 (for [j2 v2 :when (not (v1 (+ j2 diff)))] [vname2 j2])
         allbad (concat bad1 bad2)]
   (if (empty? allbad) bvars
      (do
         (remove-values bvars allbad)))))

   (defn alldiff
      "If one variable of a category has only one location, no other variable in that category has it."
      []
      (let [update (apply concat
   (for [c categories v (val c) :when (= (count (bvars v)) 1) :let [x (first (bvars v))]]
      (for [s (siblings v)]
         [s x])))]
   (remove-values bvars update)))

   (defn solitary
      "If only one variable of a category has a location, then that variable has no other locations."
      []
      (let [loners (apply concat
   (for [c categories p positions v (val c) 
      :when (and 
         ((bvars v) p)
         (> (count (bvars v)) 1)
         (not-any? #((bvars %) p) (siblings v)))]
      [v #{p}]))]
      (if (empty? loners) bvars
   (do
      ; (prn "loners:" loners)
      (apply assoc bvars loners)))))

;========== Solving "engine" ==========

(open)

(dump-vars initial-vars "Initial vars")

(dump-vars after-unary "After unary")

(def rules-list (concat (list '(alldiff)) binary-constraints (list '(solitary))))

(defn apply-rule
   "Applies the rule to the domain space and checks the result." 
   [vars rule]
   (cond
      (nil? vars) nil
      (contradictory? vars) nil
      :else 
   (binding [bvars vars]
   (let [new-vars (eval rule)]
      (cond
         (contradictory new-vars) (do 
      (prn "contradiction after rule:" rule) 
      nil)
         (= new-vars vars) vars  ; no change
         :else (do 
      (prn "applied:" rule)
      (log-tag "p" (str "applied: " (pr-str rule))) 
      (prn "result: " new-vars) 
      new-vars))))))

(defn apply-rules 
   "Uses 'reduce' to sequentially apply all the rules from 'rules-list' to 'vars'."
   [vars]
   (reduce apply-rule vars rules-list))

(defn infer
   "Repeatedly applies all rules until the var domains no longer change." 
   [vars]
   (loop [vars vars]
      (let [new-vars(apply-rules vars)]
      (if (= new-vars vars) (do 
         (prn "no change")
         vars)
      (do (recur new-vars))))))

(def after-inference (infer after-unary))

(dump-vars after-inference "Inferred")

(prn "solved?" (solved? after-inference))

(defn backtrack
   "solve by backtracking."
   [vars]
   (cond
      (nil? vars) nil
      (solved? vars) vars
      :else
      (let [fmc (first-most-constrained vars)]
   (loop [hypotheses (seq (vars fmc))]
      (if (empty? hypotheses) (do
         (prn "dead end.")
         (log-tag "p" "dead end.")
         nil)
         (let [hyp (first hypotheses) hyp-vars (assoc vars fmc #{hyp})]
      (prn "hypothesis:" fmc hyp)
      (log-tag "p" (str "hypothesis: " hyp))
      (dump-vars hyp-vars (str "Hypothesis: " fmc " = " hyp))
      (let [bt (backtrack (infer hyp-vars))]
         (if bt (do
      (prn "success!")
         (dump-vars bt "Solved")
         bt)
      (recur (rest hypotheses))))))))))

(prn "first-most-constrained:" (first-most-constrained after-inference))

(def solution (backtrack after-inference))

(prn "solution:" solution)

(close)

(println "houses loaded.")

This is 292 lines, but there's a lot of debug/diagnostic coding in there. In all, I'm pretty happy to have managed a reasonably short solution in Clojure. Functional programming made for a bit of a challenge but I managed to maintain a pretty consistent functional style.

Criticism welcome though!

For anyone who cares, here's the solution:

house       1       2               3       4             5
country     norway  ukraine         england spain         japan
color       yellow  blue            red     ivory         green
pet         fox     horse           snails  dog           zebra
smoke       kool    chesterfield    winston lucky         parliament
drink       water   tea             milk    orange-juice  coffee

Warning: I'm not sure this is what are you searching for, because I haven't read Artificial Intelligence: A Modern Approach, but I think what follow is interesting nonetheless.

Edi Weitz has an interesting page on this riddle, with explained source in Common Lisp and other sources in C++ and Common Lisp without detailed comments. I found the C++ source by Klaus Betzler particularly interesting (reformatted a little for enhanced clarity):

//  einstein.cpp  (c) Klaus Betzler 20011218

//  Klaus.Betzler@uos.de

//  `Einstein's Riddle´, the rules:

//  1 The Brit lives in the red house 
//  2 The Swede keeps dogs as pets 
//  3 The Dane drinks tea 
//  4 The green house is on the left of the white house 
//  5 The green house's owner drinks coffee 
//  6 The person who smokes Pall Mall rears birds 
//  7 The owner of the yellow house smokes Dunhill 
//  8 The man living in the centre house drinks milk 
//  9 The Norwegian lives in the first house 
// 10 The person who smokes Marlboro lives next to the one who keeps cats 
// 11 The person who keeps horses lives next to the person who smokes Dunhill 
// 12 The person who smokes Winfield drinks beer 
// 13 The German smokes Rothmans 
// 14 The Norwegian lives next to the blue house 
// 15 The person who smokes Marlboro has a neigbor who drinks water 

#undef WIN32           // #undef for Linux

#include <stdio.h>
#ifdef WIN32
  #include <windows.h>
#endif

inline unsigned long BIT(unsigned n) {return 1<<n;}

const unsigned long 
  yellow    = BIT( 0), 
  blue      = BIT( 1),
  red       = BIT( 2),
  green     = BIT( 3),
  white     = BIT( 4),

  norwegian = BIT( 5),
  dane      = BIT( 6),
  brit      = BIT( 7),
  german    = BIT( 8),
  swede     = BIT( 9),

  water     = BIT(10),
  tea       = BIT(11),
  milk      = BIT(12),
  coffee    = BIT(13),
  beer      = BIT(14),

  dunhill   = BIT(15),
  marlboro  = BIT(16),
  pallmall  = BIT(17),
  rothmans  = BIT(18),
  winfield  = BIT(19),

  cat       = BIT(20),
  horse     = BIT(21),
  bird      = BIT(22),
  fish      = BIT(23),
  dog       = BIT(24);

const char * Label[] = {
  "Yellow",   "Blue",    "Red",     "Green",   "White",
  "Norwegian","Dane",    "Brit",    "German",  "Swede",
  "Water",    "Tea",     "Milk",    "Coffee",  "Beer",
  "Dunhill",  "Marlboro","Pallmall","Rothmans","Winfield",
  "Cat",      "Horse",   "Bird",    "Fish",    "Dog"
};

const unsigned long color   = yellow   +blue    +red     +green   +white;
const unsigned long country = norwegian+dane    +brit    +german  +swede;
const unsigned long drink   = water    +tea     +milk    +coffee  +beer;
const unsigned long cigar   = dunhill  +marlboro+pallmall+rothmans+winfield;
const unsigned long animal  = cat      +horse   +bird    +fish    +dog;

unsigned long house [5] = {norwegian, blue, milk, 0, 0};  // rules 8,9,14
unsigned long result[5];

const unsigned long comb[] = { // simple rules
  brit+red,                    // 1
  swede+dog,                   // 2
  dane+tea,                    // 3
  green+coffee,                // 5
  pallmall+bird,               // 6
  yellow+dunhill,              // 7
  winfield+beer,               // 12
  german+rothmans              // 13
};

const unsigned long combmask[] = { // corresponding selection masks
  country+color,
  country+animal,
  country+drink,
  color+drink,
  cigar+animal,
  color+cigar,
  cigar+drink,
  country+cigar
};


inline bool SimpleRule(unsigned nr, unsigned which)
{
  if (which<8) {
    if ((house[nr]&combmask[which])>0)
      return false;
    else {
      house[nr]|=comb[which];
      return true;
    }
  }
  else {           // rule 4
    if ((nr==4)||((house[nr]&green)==0))
      return false;
    else
      if ((house[nr+1]&color)>0)
        return false;
      else {
        house[nr+1]|=white;
        return true;
      }
  }
}

inline void RemoveSimple(unsigned nr, unsigned which)
{
  if (which<8) 
    house[nr]&=~comb[which];
  else
    house[nr+1]&=~white;
}

inline bool DunhillRule(unsigned nr, int side)  // 11
{
  if (((side==1)&&(nr==4))||((side==-1)&&(nr==0))||((house[nr]&dunhill)==0))
    return false;
  if ((house[nr+side]&animal)>0)
    return false;
  house[nr+side]|=horse;
  return true;
}

inline void RemoveDunhill(unsigned nr, unsigned side)
{
  house[nr+side]&=~horse;
}

inline bool MarlboroRule(unsigned nr)    // 10 + 15
{
  if ((house[nr]&cigar)>0)
    return false;
  house[nr]|=marlboro;
  if (nr==0) {
    if ((house[1]&(animal+drink))>0)
      return false;
    else {
      house[1]|=(cat+water);
      return true;
    }
  }
  if (nr==4) {
    if ((house[3]&(animal+drink))>0)
      return false;
    else {
      house[3]|=(cat+water);
      return true;
    }
  }
  int i,k;
  for (i=-1; i<2; i+=2) {
    if ((house[nr+i]&animal)==0) {
      house[nr+i]|=cat;
      for (k=-1; k<2; k+=2) {
        if ((house[nr+k]&drink)==0) {
          house[nr+k]|=water;
          return true;
        }
      }
    }
  }
  return false;
}

void RemoveMarlboro(unsigned m)
{
  house[m]&=~marlboro;
  if (m>0)
    house[m-1]&=~(cat+water);
  if (m<4)
    house[m+1]&=~(cat+water);
}

void Recurse(unsigned recdepth)
{
  unsigned n, m;
  for (n=0; n<5; n++) {
    if (recdepth<9) {    // simple rules
      if (SimpleRule(n, recdepth)) {
        Recurse(recdepth+1);
        RemoveSimple(n, recdepth);
      }
    }
    else {               // Dunhill and Marlboro
      for (int side=-1; side<2; side+=2)
        if (DunhillRule(n, side)) {
          for (m=0; m<5; m++) 
            if (MarlboroRule(m))
              for (int r=0; r<5; r++)
                result[r] = house[r];
            else
              RemoveMarlboro(m);
          RemoveDunhill(n, side);
        }
    }
  }
}

int main()
{
  int index, i;
#ifdef WIN32
  LARGE_INTEGER time0, time1, freq;
  QueryPerformanceCounter(&time0);
#endif
  Recurse(0);
#ifdef WIN32
  QueryPerformanceCounter(&time1);
  QueryPerformanceFrequency(&freq);
  printf("\nComputation Time: %ld microsec\n\n", 
    (time1.QuadPart-time0.QuadPart)*1000000/freq.QuadPart);
#endif
  if (result[0]==0) {
    printf("No solution found !?!\n");
    return 1;
    }
  for (i=0; i<5; i++)
    if ((result[i]&animal)==0)
      for (index=0; index<25; index++)
        if (((result[i]&country)>>index)==1)
          printf("Fish Owner is the %s !!!\n\n", Label[index]);
  for (i=0; i<5; i++) {
    printf("%d: ",i+1);
    for (index=0; index<25; index++)
      if (((result[i]>>index)&1)==1)
        printf("%-12s",Label[index]);
    printf("\n\n");
    }
  return 0;
}

Here's how you model a binary constraints satisfaction problem

All the clues given in the riddle add constraints. With no constraints any combination is possible.

So what you want to do is to use elimination, which is actually the opposite approach of what you used in your examples. Here's how:

You need a matrix with one row for each nationality, and one column for each boolean attribute ("lives in a red house", "lives in a blue house", "has a dog", ...)

• Each cell in this matrix should initially be set to TRUE.

• Then you iterate through the list of constraints and try to apply them to your matrix. For example, the clue "The Englishman lives in the red house." sets each of the cells in the "red house" column to FALSE except for the one on the English nationality line.

• Skip clues that refer to attributes that are not yet inferred. For example: "The Winston smoker owns snails." -- well, if it is not yet determined who smokes Winston or who owns snails then skip this constraint for now.

This is also, by the way, how you solve sudoku puzzles and the like.