Rudy's OBTF

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)