Rudy’s OBTF Rudolf Adamkovič

Home / Computer science / Zebra puzzle / Computation


Constraints: Fact 1

The Englishman lives in the red house.

Using

\begin{align*} a & = x_{5, i, 1} \\ b & = x_{4, i, 4} \\ \end{align*}

derive the conjunctive normal form by the definition of conditional

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

and compute

for i in range(m):
    a = x[Attribute.NATION, i, Nation.ENGLISH]
    b = x[Attribute.COLOR, i, Color.RED]
    model.add_bool_or(a.Not(), b)

© 2025 Rudolf Adamkovič under GNU General Public License version 3.
Made with Emacs and secret alien technologies of yesteryear.