Home / Computer science / Zebra puzzle / Computation
Constraints: Exactly one attribute value per house
Knowing each row of every \(X_h\) must contain exactly one \(1\)
\begin{equation*} \forall h \forall j \sum_{i = 1}^{m} x_{hij} = 1 \end{equation*}derive the conjunctive normal form
\begin{align*} \forall h \forall j \sum_{i = 1}^{m} x_{hij} = 1 \quad \iff \quad & \forall h \forall j \Bigg( \sum_{i = 1}^{m} x_{hij} \leq 1 \Bigg) \land \Bigg( \sum_{i = 1}^{m} x_{hij} \geq 1 \Bigg) \\[1ex] \forall h \forall j \sum_{i = 1}^{m} x_{hij} \geq 1 \quad \iff \quad & \forall h \forall j (x_{h1j} \lor x_{h2j} \lor x_{h3j} \lor \cdots \lor x_{hmj}) \\[1ex] \forall h \forall j \sum_{i = 1}^{m} x_{hij} \leq 1 \quad \iff \quad & \forall h \forall j \forall i \forall q < i \> (\lnot x_{hij} \lor \lnot x_{hqj}) \end{align*}and compute
for h in range(l):
for j in range(n):
model.add_bool_or(x[h, i, j] for i in range(m))
for i1 in range(m):
for i2 in range(i1):
model.add_bool_or(x[h, i1, j].Not(), x[h, i2, j].Not())