Rudy's OBTF

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)