Rudy's OBTF

Home / Computer science / Zebra puzzle / Computation

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)