Rudy's OBTF

Home / Computer science / Zebra puzzle / Computation

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)