Rudy's OBTF

Home / Computer science / Zebra puzzle / Computation

Constraints: Fact 5

The green house is immediately to the right of the ivory house.

Using

\begin{align*} a & = x_{4, i, 2} \\ b & = x_{4, (i - 1), 3} \\ \end{align*}

derive the conjunctive normal form as in Fact 1 but with \(\forall i > 1\)

\begin{equation*} \forall i > 1 \quad (\lnot a \lor b) \end{equation*}

noting that

the left-most house (\(i = 1\)) cannot be green
as the ivory house would then be out of bounds
the right-most house (\(i = m\)) cannot be ivory
as the green house would then be out of bounds

\begin{equation*} (\lnot x_{4, 1, 2}) \land (\lnot x_{4, m, 3}) \end{equation*}

and compute

for i in range(m)[1:]:
    a = x[Attribute.COLOR, i, Color.GREEN]
    b = x[Attribute.COLOR, i - 1, Color.IVORY]
    model.add_bool_or(a.Not(), b)

model.add_bool_or(x[Attribute.COLOR, 0, Color.GREEN].Not())
model.add_bool_or(x[Attribute.COLOR, m - 1, Color.IVORY].Not())