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: no
Solve time: 1m22s

Solution

Let the given set of pixels be a finite region of the square grid. A tatami tiling is a partition of these pixels into dominoes such that no three dominoes meet at a common corner. We encode both the covering condition and the tatami condition as a Boolean formula.

For every possible placement $d$ of a domino covering two adjacent pixels of the region, introduce a Boolean variable $x_d$. The interpretation is

$$ x_d=1 $$

if and only if the domino placement $d$ is chosen in the tiling.

For every pixel $p$, let $D(p)$ be the set of domino placements that cover $p$. The requirement that every pixel be covered by at least one chosen domino gives the clause

$$ \bigvee_{d\in D(p)}x_d . $$

We must also prevent two selected dominoes from covering the same pixel. For every pixel $p$ and every pair of distinct dominoes $d,e\in D(p)$, include the binary clause

$$ (\bar{x}_d\vee\bar{x}_e). $$

The conjunction of these clauses forces every pixel to be covered by exactly one chosen domino.

It remains to encode the tatami restriction. Consider every grid vertex $v$ that is a corner shared by four possible unit squares. A violation occurs exactly when three dominoes meet at $v$. Let $C(v)$ be the set of domino placements having $v$ as one of their corners. For every triple of distinct dominoes $d,e,f\in C(v)$, include the clause

$$ (\bar{x}_d\vee\bar{x}_e\vee\bar{x}_f). $$

This clause forbids the simultaneous choice of any three dominoes meeting at the same corner. Since the covering clauses already guarantee that selected dominoes form a complete domino tiling, the additional clauses remove precisely the tilings that violate the tatami condition.

The complete SAT instance is therefore

$$ F= \bigwedge_{p} \left(\bigvee_{d\in D(p)}x_d\right) \wedge \bigwedge_{p} \bigwedge_{\substack{d,e\in D(p)\d\ne e}} (\bar{x}d\vee\bar{x}e) \wedge \bigwedge{v} \bigwedge{\substack{d,e,f\in C(v)\d,e,f\ \text{distinct}}} (\bar{x}_d\vee\bar{x}_e\vee\bar{x}_f). $$

If a SAT solver finds a satisfying assignment of $F$, the dominoes corresponding to variables with value $1$ form a tatami tiling. The first group of clauses proves that every pixel is covered, the second group proves that no pixel is covered twice, and the third group proves that no corner has three incident dominoes. Hence the satisfying assignment gives a valid tatami tiling.

Conversely, if a tatami tiling exists, set $x_d=1$ exactly for the dominoes in that tiling and set every other variable to $0$. Every pixel clause is satisfied because the tiling covers the region, every binary exclusion clause is satisfied because no two dominoes overlap, and every ternary exclusion clause is satisfied because the tiling has no corner where three dominoes meet. Therefore the resulting assignment satisfies $F$.

Thus the original tiling problem has a solution exactly when the constructed SAT instance is satisfiable. A SAT solver can therefore decide whether a tatami tiling exists and, when one exists, recover it from the true variables. This completes the proof. ∎