Home / Computer science / Zebra puzzle / Computation
Constraints: Exactly one house per attribute value
Knowing each column of every \(X_h\) must contain exactly one \(1\),
\begin{equation*} \forall h \forall i \sum_{j = 1}^{n} x_{hij} = 1 \end{equation*}derive the conjunctive normal form as in the previous step
\begin{align*} \forall h \forall i \quad & (x_{hi1} \lor x_{hi2} \lor x_{hi3} \lor \cdots \lor x_{hin}) \\ \forall h \forall i \forall j \forall q < j \quad & (\lnot x_{hij} \lor \lnot x_{hiq}) \\ \end{align*}and compute
for h in range(l):
for i in range(m):
model.add_bool_or(x[h, i, j] for j in range(n))
for j1 in range(n):
for j2 in range(j1):
model.add_bool_or(x[h, i, j1].Not(), x[h, i, j2].Not())