Rudy's OBTF

Home / Computer science / Zebra puzzle / Computation

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)