Rudy's OBTF

Home / Computer science / Zebra puzzle / Computation

Constraints: Fact 14

The Norwegian lives next to the blue house.

Using

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

derive the conjunctive normal form as in Fact 10

\begin{equation*} \forall i \quad \begin{cases} (\lnot a \lor b) & i = 1 \\ (\lnot a \lor b \lor c) & 1 < i < m \\ (\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.NATION, i, Nation.NORWEGIAN))
    b = x.get((Attribute.COLOR, i + 1, Color.BLUE))
    c = x.get((Attribute.COLOR, i - 1, Color.BLUE))

    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)