TAOCP 7.2.2.2 Exercise 118

Section 7.2.2.2: Satisfiability

Exercise 118. [20] [20] A tatami tiling is a covering by dominoes in which no three share a corner:

(Notice that $\frac{\Box}{\Box}$ is disallowed, but $\frac{\Box}{\Box}$ would be fine.) Explain how to use a SAT solver to find a tatami tiling that covers a given set of pixels, unless no such tiling exists.

Verified: yes
Solve time: 3m24s

---

Let the region be a finite set of unit pixels $P \subset \mathbb{Z}^2$. A domino tiling is represented by choosing edges of the grid graph induced on $P$.

A grid edge corresponds to an unordered adjacent pair ${p,q}\subset P$. Introduce a Boolean variable

$$ x_{pq} \in {0,1}, \quad x_{pq}=1 \iff \text{pixels } p,q \text{ are covered by a domino}. $$

1. Domino tiling constraints (exact cover)

Let $\operatorname{Inc}(p)$ be the set of grid edges ${p,q}$ with $q \in P$.

(a) Each pixel is covered at least once

$$ \bigvee_{x_{pq}\in \operatorname{Inc}(p)} x_{pq}. $$

(b) Each pixel is covered at most once

For all distinct edges $x_{pq}, x_{pr} \in \operatorname{Inc}(p)$,

$$ (\neg x_{pq} \vee \neg x_{pr}). $$

These clauses enforce that each pixel belongs to exactly one chosen domino.

2. Geometric notion of “domino touches a vertex”

Let $V$ be the set of grid vertices. A vertex $v=(i,j)$ is a corner of a pixel $p=(a,b)$ (unit square) if

$$ v \in {(a,b),(a+1,b),(a,b+1),(a+1,b+1)}. $$

For a domino variable $x_{pq}$, define a constant predicate

$$ c_{v,pq} = \begin{cases} 1 & \text{if } v \text{ is a corner of } p \text{ or } q,\ 0 & \text{otherwise.} \end{cases} $$

Thus a domino “touches” a vertex $v$ exactly when $c_{v,pq}=1$.

For each vertex $v$, define the set

$$ S_v = {, x_{pq} \mid c_{v,pq}=1 ,}. $$

This set is computable from geometry before building the SAT instance.

3. Tatami constraint (no three dominoes meet at a vertex)

The tatami condition is:

At every vertex $v$, at most two distinct dominoes touch $v$.

Since “domino $x_{pq}$ touches $v$” is exactly the membership $x_{pq}\in S_v$, the constraint becomes:

$$ \sum_{x_{pq}\in S_v} x_{pq} \le 2. $$

4. CNF encoding of the tatami constraint

For each vertex $v$ and for every triple of distinct variables

$$ x_{e_1}, x_{e_2}, x_{e_3} \in S_v, $$

add the clause

$$ (\neg x_{e_1} \vee \neg x_{e_2} \vee \neg x_{e_3}). $$

This enforces that no three dominoes simultaneously touch the same vertex.

5. Correctness of the encoding

Soundness

A satisfying assignment of the SAT formula:

• selects exactly one domino incident to each pixel, hence forms a valid domino tiling,
• and satisfies all vertex clauses, hence no vertex $v$ has three or more incident true variables in $S_v$.

Therefore no grid vertex is shared by three dominoes, so the tiling is tatami.

Completeness

Given any tatami tiling:

• define $x_{pq}=1$ exactly for the dominoes in the tiling,
• each pixel is covered exactly once, so the exact-cover clauses hold,
• and since no vertex is incident to three dominoes, every triple clause at every $v$ is satisfied.

Thus the assignment satisfies the SAT formula.

6. Conclusion

The construction yields a CNF formula of size polynomial in $|P|$, with variables $x_{pq}$ for adjacent pixel pairs and standard exact-cover constraints plus triple-forbidden clauses per vertex.

The formula is satisfiable if and only if the given region admits a tatami tiling. A SAT solver can therefore be used directly to find such a tiling or certify that none exists. ∎