Personal website

Computation

Find all solutions of the Zebra puzzle using constraint programming,

limiting all constraints to conjunctive normal form.

Imports

from enum import IntEnum
from ortools.sat.python.cp_model import CpModel, CpSolver, CpSolverSolutionCallback

Model
```
model = CpModel()
```

Attributes

Animal	Drink	Cigarettes	Color	Nation
dog	coffee	Chesterfield	blue	English
fox	orange juice	Kool	green	Japanese
horse	milk	Lucky Strike	ivory	Norwegian
snails	tea	Old Gold	red	Spanish
zebra	water	Parliament	yellow	Ukrainian

attributes = ["ANIMAL", "DRINK", "CIGARETTES", "COLOR", "NATION"]
animals = ["DOG", "FOX", "HORSE", "SNAILS", "ZEBRA"]
drinks = ["COFFEE", "ORANGE_JUICE", "MILK", "TEA", "WATER"]
cigarettes = ["CHESTERFIELD", "KOOL", "LUCKY_STRIKE", "OLD_GOLD", "PARLIAMENT"]
colors = ["BLUE", "GREEN", "IVORY", "RED", "YELLOW"]
nations = ["ENGLISH", "JAPANESE", "NORWEGIAN", "SPANISH", "UKRAINIAN"]

Attribute = IntEnum("Attribute", attributes, start=0)
Animal = IntEnum("Animal", animals, start=0)
Drink = IntEnum("Drink", drinks, start=0)
Cigarettes = IntEnum("Cigarettes", cigarettes, start=0)
Color = IntEnum("Color", colors, start=0)
Nation = IntEnum("Nation", nation, start=0)

Decision variables
- \(1 \leq h \leq l\) with \(l = 5\) attributes
- \(1 \leq i \leq m\) with \(m = 5\) houses
- \(1 \leq j \leq n\) with \(n = 5\) attribute values
```
l, m, n = 5, 5, 5
```
\begin{equation*} \underset{1 \leq h \leq \ell}{X_h} = \begin{pmatrix} x_{h11} & & \cdots & & x_{h1n} \\ & \ddots & & & \\ \vdots & & x_{hij} & & \vdots \\ & & & \ddots & \\ x_{hm1} & & \cdots & & x_{hmn} \end{pmatrix} \in {\{0, 1\}}^{m \times n} \end{equation*}
```
x = {
    (h, i, j): model.new_bool_var("x_{%d, %d, %d}" % (h + 1, i + 1, j + 1))
    for h in range(l)
    for i in range(m)
    for j in range(n)
}
```
Constraints: Exactly one attribute value per house
Knowing each row of every \(X_h\) must contain exactly one \(1\)
\begin{equation*} \forall h \forall j \sum_{i = 1}^{m} x_{hij} = 1 \end{equation*}
derive the conjunctive normal form
\begin{align*} \forall h \forall j \sum_{i = 1}^{m} x_{hij} = 1 \quad \iff \quad & \forall h \forall j \Bigg( \sum_{i = 1}^{m} x_{hij} \leq 1 \Bigg) \land \Bigg( \sum_{i = 1}^{m} x_{hij} \geq 1 \Bigg) \\[1ex] \forall h \forall j \sum_{i = 1}^{m} x_{hij} \geq 1 \quad \iff \quad & \forall h \forall j (x_{h1j} \lor x_{h2j} \lor x_{h3j} \lor \cdots \lor x_{hmj}) \\[1ex] \forall h \forall j \sum_{i = 1}^{m} x_{hij} \leq 1 \quad \iff \quad & \forall h \forall j \forall i \forall q < i \> (\lnot x_{hij} \lor \lnot x_{hqj}) \end{align*}
and compute
```
for h in range(l):
    for j in range(n):
        model.add_bool_or(x[h, i, j] for i in range(m))
        for i1 in range(m):
            for i2 in range(i1):
                model.add_bool_or(x[h, i1, j].Not(), x[h, i2, j].Not())
```
Constraints: Exactly one house per attribute value
Knowing each column of every \(X_h\) must contain exactly one \(1\),
\begin{equation*} \forall h \forall i \sum_{j = 1}^{n} x_{hij} = 1 \end{equation*}
derive the conjunctive normal form as in the previous step
\begin{align*} \forall h \forall i \quad & (x_{hi1} \lor x_{hi2} \lor x_{hi3} \lor \cdots \lor x_{hin}) \\ \forall h \forall i \forall j \forall q < j \quad & (\lnot x_{hij} \lor \lnot x_{hiq}) \\ \end{align*}
and compute
```
for h in range(l):
    for i in range(m):
        model.add_bool_or(x[h, i, j] for j in range(n))
        for j1 in range(n):
            for j2 in range(j1):
                model.add_bool_or(x[h, i, j1].Not(), x[h, i, j2].Not())
```
Constraints: Fact 1
The Englishman lives in the red house.

Using
\begin{align*} a & = x_{5, i, 1} \\ b & = x_{4, i, 4} \\ \end{align*}
derive the conjunctive normal form by the definition of conditional
\begin{equation*} \forall i \quad a \implies b \equiv (\lnot a \lor b) \end{equation*}
and compute
```
for i in range(m):
    a = x[Attribute.NATION, i, Nation.ENGLISH]
    b = x[Attribute.COLOR, i, Color.RED]
    model.add_bool_or(a.Not(), b)
```
Constraints: Fact 2
The Spaniard owns the dog.

Using
\begin{align*} a & = x_{5, i, 4} \\ b & = x_{1, i, 1} \\ \end{align*}
derive the conjunctive normal form as in Fact 1
\begin{equation*} \forall i \quad (\lnot a \lor b) \end{equation*}
and compute
```
for i in range(m):
    a = x[Attribute.NATION, i, Nation.SPANISH]
    b = x[Attribute.ANIMAL, i, Animal.DOG]
    model.add_bool_or(a.Not(), b)
```
Constraints: Fact 3
Coffee is drunk in the green house.

Using
\begin{align*} a & = x_{2, i, 1} \\ b & = x_{4, i, 2} \\ \end{align*}
derive the conjunctive normal form as in Fact 1
\begin{equation*} \forall i \quad (\lnot a \lor b) \end{equation*}
and compute
```
for i in range(m):
    a = x[Attribute.DRINK, i, Drink.COFFEE]
    b = x[Attribute.COLOR, i, Color.GREEN]
    model.add_bool_or(a.Not(), b)
```
Constraints: Fact 4
The Ukrainian drinks tea.

Using
\begin{align*} a & = x_{5, i, 5} \\ b & = x_{2, i, 4} \\ \end{align*}
derive the conjunctive normal form as in Fact 1
\begin{equation*} \forall i \quad (\lnot a \lor b) \end{equation*}
and compute
```
for i in range(m):
    a = x[Attribute.NATION, i, Nation.UKRAINIAN]
    b = x[Attribute.DRINK, i, Drink.TEA]
    model.add_bool_or(a.Not(), b)
```
Constraints: Fact 5
The green house is immediately to the right of the ivory house.

Using
\begin{align*} a & = x_{4, i, 2} \\ b & = x_{4, (i - 1), 3} \\ \end{align*}
derive the conjunctive normal form as in Fact 1 but with \(\forall i > 1\)
\begin{equation*} \forall i > 1 \quad (\lnot a \lor b) \end{equation*}
noting that
- the left-most house (\(i = 1\)) cannot be green
  as the ivory house would then be out of bounds
- the right-most house (\(i = m\)) cannot be ivory
  as the green house would then be out of bounds
\begin{equation*} (\lnot x_{4, 1, 2}) \land (\lnot x_{4, m, 3}) \end{equation*}
and compute
```
for i in range(m)[1:]:
    a = x[Attribute.COLOR, i, Color.GREEN]
    b = x[Attribute.COLOR, i - 1, Color.IVORY]
    model.add_bool_or(a.Not(), b)

model.add_bool_or(x[Attribute.COLOR, 0, Color.GREEN].Not())
model.add_bool_or(x[Attribute.COLOR, m - 1, Color.IVORY].Not())
```
Constraints: Fact 6
The Old Gold smoker owns snails.

Using
\begin{align*} a & = x_{3, i, 4} \\ b & = x_{1, i, 4} \\ \end{align*}
derive the conjunctive normal form as in Fact 1
\begin{equation*} \forall i \quad (\lnot a \lor b) \end{equation*}
and compute
```
for i in range(m):
    a = x[Attribute.CIGARETTES, i, Cigarettes.OLD_GOLD]
    b = x[Attribute.ANIMAL, i, Animal.SNAILS]
    model.add_bool_or(a.Not(), b)
```
Constraints: Fact 7
Kools are smoked in the yellow house.

Using
\begin{align*} a & = x_{3, i, 2} \\ b & = x_{4, i, 5} \\ \end{align*}
derive the conjunctive normal form as in Fact 1
\begin{equation*} \forall i \quad (\lnot a \lor b) \end{equation*}
and compute
```
for i in range(m):
    a = x[Attribute.CIGARETTES, i, Cigarettes.KOOL]
    b = x[Attribute.COLOR, i, Color.YELLOW]
    model.add_bool_or(a.Not(), b)
```
Constraints: Fact 8
Milk is drunk in the middle house.

Using
\begin{equation*} a = x_{2, 3, 3} \end{equation*}
derive the conjunctive normal form
\begin{equation*} (a) \end{equation*}
and compute
```
a = x[Attribute.DRINK, 2, Drink.MILK]
model.add_bool_or(a)
```
Constraints: Fact 9
The Norwegian lives in the first house.

Using
\begin{equation*} a = x_{5, 1, 3} \end{equation*}
derive the conjunctive normal form
\begin{equation*} (a) \end{equation*}
and compute
```
a = x[Attribute.NATION, 0, Nation.NORWEGIAN]
model.add_bool_or(a)
```
Constraints: Fact 10
The man who smokes Chesterfields lives in the house next to the man with the fox.

Using
\begin{align*} a & = x_{3, i, 1} \\ b & = x_{1, (i + 1), 2} \\ c & = x_{1, (i - 1), 2} \\ \end{align*}
derive the conjunctive normal form by the definition of conditional
\begin{equation*} \forall i \quad \begin{cases} a \implies b \equiv (\lnot a \lor b) & i = 1 \\ a \implies b \lor c \equiv \lnot a \lor (b \lor c) \equiv (\lnot a \lor b \lor c) & 1 < i < m \\ a \implies c \equiv (\lnot a \lor c) & i = m \\ \end{cases} \end{equation*}
and compute
```
for i in range(m):

    # NOTE Use `x.get(...)' instead of `x[...]' to skip bound checking.
    a = x.get((Attribute.CIGARETTES, i, Cigarettes.CHESTERFIELD))
    b = x.get((Attribute.ANIMAL, i + 1, Animal.FOX))
    c = x.get((Attribute.ANIMAL, i - 1, Animal.FOX))

    if i == 0:
        model.add_bool_or(a.Not(), b)
    elif 0 < i < m - 1:
        model.add_bool_or(a.Not(), b, c)
    elif i == m - 1:
        model.add_bool_or(a.Not(), c)
```

Constraints: Fact 11

Kools are smoked in the house next to the house where the horse is kept.

Using

\begin{align*} a & = x_{3, i, 2} \\ b & = x_{1, (i + 1), 3} \\ c & = x_{1, (i - 1), 3} \\ \end{align*}

derive the conjunctive normal form as in Fact 10

\begin{equation*} \forall i \quad \begin{cases} (\lnot a \lor b) & i = 1 \\ (\lnot a \lor b \lor c) & 1 < i < m \\ (\lnot a \lor c) & i = m \\ \end{cases} \end{equation*}

and compute

for i in range(m):

    # NOTE Use `x.get(...)' instead of `x[...]' to skip bound checking.
    a = x.get((Attribute.CIGARETTES, i, Cigarettes.KOOL))
    b = x.get((Attribute.ANIMAL, i + 1, Animal.HORSE))
    c = x.get((Attribute.ANIMAL, i - 1, Animal.HORSE))

    if i == 0:
        model.add_bool_or(a.Not(), b)
    elif 0 < i < m - 1:
        model.add_bool_or(a.Not(), b, c)
    elif i == m - 1:
        model.add_bool_or(a.Not(), c)

Constraints: Fact 12
The Lucky Strike smoker drinks orange juice.

Using
\begin{align*} a & = x_{3, i, 3} \\ b & = x_{2, i, 2} \\ \end{align*}
derive the conjunctive normal form as in Fact 1
\begin{equation*} \forall i \quad (\lnot a \lor b) \end{equation*}
and compute
```
for i in range(m):
    a = x[Attribute.CIGARETTES, i, Cigarettes.LUCKY_STRIKE]
    b = x[Attribute.DRINK, i, Drink.ORANGE_JUICE]
    model.add_bool_or(a.Not(), b)
```
Constraints: Fact 13
The Japanese smokes Parliaments.

Using
\begin{align*} a & = x_{5, i, 2} \\ b & = x_{3, i, 5} \\ \end{align*}
derive the conjunctive normal form as in Fact 1
\begin{equation*} \forall i \quad (\lnot a \lor b) \end{equation*}
and compute
```
for i in range(m):
    a = x[Attribute.NATION, i, Nation.JAPANESE]
    b = x[Attribute.CIGARETTES, i, Cigarettes.PARLIAMENT]
    model.add_bool_or(a.Not(), b)
```

Constraints: Fact 14

The Norwegian lives next to the blue house.

Using

\begin{align*} a & = x_{5, i, 3} \\ b & = x_{4, (i + 1), 1} \\ c & = x_{4, (i - 1), 1} \\ \end{align*}

derive the conjunctive normal form as in Fact 10

\begin{equation*} \forall i \quad \begin{cases} (\lnot a \lor b) & i = 1 \\ (\lnot a \lor b \lor c) & 1 < i < m \\ (\lnot a \lor c) & i = m \\ \end{cases} \end{equation*}

and compute

for i in range(m):

    # NOTE Use `x.get(...)' instead of `x[...]' to skip bound checking.
    a = x.get((Attribute.NATION, i, Nation.NORWEGIAN))
    b = x.get((Attribute.COLOR, i + 1, Color.BLUE))
    c = x.get((Attribute.COLOR, i - 1, Color.BLUE))

    if i == 0:
        model.add_bool_or(a.Not(), b)
    elif 0 < i < m - 1:
        model.add_bool_or(a.Not(), b, c)
    elif i == m - 1:
        model.add_bool_or(a.Not(), c)

Solution

Who drinks water?

\(i\)-th house such that \(x_{2, i, 5} = 1\)
\(j\)-th nation such that \(x_{5, i, j} = 1\)

Who owns the zebra?

\(i\)-th house such that \(x_{1, i, 5} = 1\)
\(j\)-th nation such that \(x_{5, i, j} = 1\)

class SolutionPrinter(CpSolverSolutionCallback):
    def __init__(self):
        CpSolverSolutionCallback.__init__(self)
        self.__solution_count = 0

    def __solution(self, attribute, value):
        i = next(i for i in range(m) if self.value(x[attribute, i, value]))
        j = next(j for j in range(n) if self.value(x[Attribute.NATION, i, j]))
        return Nation(j).name

    def on_solution_callback(self) -> None:
        self.__solution_count += 1
        w = self.__solution(Attribute.DRINK, Drink.WATER)
        z = self.__solution(Attribute.ANIMAL, Animal.ZEBRA)
        print("Solution #%d" % self.__solution_count)
        print("Who drinks water? %s." % w)
        print("Who owns the zebra? %s." % z)

solver = CpSolver()
solver.SearchForAllSolutions(model, SolutionPrinter())

Solution #1
Who drinks water? NORWEGIAN.
Who owns the zebra? JAPANESE.