TAOCP 7.2.2.2 Exercise 65

Let $x_{ij}$ denote the state of cell $(i,j)$ before a Life transition, and let $x'_{ij}$ denote its state after the transition.

taocpmathematicsalgorithmsvolume-4hard

Section 7.2.2.2: Satisfiability

Exercise 65. ▶ [28] $[28]$ Describe encodings of the Life transition function (35) into clauses. a) Use only the variables $x'{ij}$ and $x{ij}$. b) Use auxiliary variables with the Bailleux and Boufkhad encoding (20)–(21), sharing intermediate results between neighboring cells as discussed in the text.

Verified: no
Solve time: 2m21s

Setup

Let $x_{ij}$ denote the state of cell $(i,j)$ before a Life transition, and let $x'_{ij}$ denote its state after the transition. The neighborhood of $(i,j)$ consists of the eight cells adjacent horizontally, vertically, and diagonally. Write

$$ N_{ij}={(i+a,j+b):(a,b)\in{-1,0,1}^2,\ (a,b)\ne(0,0)}. $$

The Life transition rule in (35) states that

$$ x'_{ij}=1 $$

exactly when either the cell is alive and has two live neighbors, or it has three live neighbors. Thus, if

$$ s_{ij}=\sum_{(u,v)\in N_{ij}}x_{uv}, $$

then

$$ x'{ij}=1\iff (s{ij}=3)\vee(x_{ij}=1\land s_{ij}=2). $$

The task is to encode this Boolean relation as clauses.

Solution

For part (a), only the variables $x'{ij}$ and $x{ij}$ may be used. Let

$$ z_0=x'{ij},\qquad z_1=x{ij}, $$

and let the remaining variables $z_2,\ldots,z_9$ be the eight neighbor variables in any fixed order. The transition relation is a Boolean function of these ten variables. A clause can be obtained from every assignment that violates the Life rule.

For a binary vector

$$ a=(a_0,a_1,\ldots,a_9)\in{0,1}^{10}, $$

define the clause

$$ C(a)= \bigvee_{k=0}^{9} \begin{cases} z_k,&a_k=0,\ \bar z_k,&a_k=1. \end{cases} $$

This clause is false precisely on the assignment $z_k=a_k$ for all $k$. Therefore, if $\mathcal{B}$ is the set of all assignments that do not satisfy the Life transition rule, the required CNF formula is

$$ \bigwedge_{a\in\mathcal{B}}C(a). $$

Every clause in this formula contains only variables $x'{ij}$, $x{ij}$, and the eight neighboring variables. The formula is satisfied exactly by the assignments obeying the transition rule, because every violating assignment is excluded and every valid assignment satisfies every clause.

The construction uses a direct truth-table encoding. It is finite, because the ten variables have only $2^{10}$ possible assignments. The clauses corresponding to the valid assignments are omitted, while the clauses corresponding to the invalid assignments are included.

For part (b), introduce auxiliary variables that encode the number of live neighbors. The Bailleux and Boufkhad construction replaces a cardinality condition by a sequence of smaller cardinality relations. For a collection of Boolean variables

$$ y_1,\ldots,y_m, $$

the encoding introduces auxiliary variables representing partial sums. If

$$ s_i^j $$

denotes that among $y_1,\ldots,y_i$ at least $j$ variables are true, the clauses from (20) and (21) enforce the recurrence

$$ s_i^j\iff s_{i-1}^j\vee(y_i\land s_{i-1}^{j-1}), $$

with the corresponding CNF clauses from the encoding. The important point is that the same auxiliary variables may be reused whenever two cardinality expressions share partial sums.

For a cell $(i,j)$, apply this encoding to the eight variables

$$ {x_{uv}:(u,v)\in N_{ij}}. $$

Let the resulting auxiliary variables determine whether

$$ s_{ij}=2 $$

and whether

$$ s_{ij}=3. $$

The exact-count conditions are represented by

$$ E_2(s_{ij})=(s_{ij}\ge2)\land\neg(s_{ij}\ge3), $$

and

$$ E_3(s_{ij})=(s_{ij}\ge3)\land\neg(s_{ij}\ge4). $$

The transition rule can then be written as

$$ x'{ij}\iff E_3(s{ij})\vee(x_{ij}\land E_2(s_{ij})). $$

The implication from the right side to $x'_{ij}$ gives the clauses

$$ \bar E_3\vee x'_{ij}, $$

and

$$ \overline{x_{ij}}\vee\overline{E_2}\vee x'_{ij}, $$

where each cardinality expression is replaced by its Bailleux and Boufkhad clauses.

The reverse implication is

$$ x'{ij}\Rightarrow E_3(s{ij})\vee(x_{ij}\land E_2(s_{ij})). $$

Equivalently,

$$ \neg x'{ij}\vee E_3(s{ij})\vee(x_{ij}\land E_2(s_{ij})). $$

Distributing the conjunction gives

$$ (\neg x'{ij}\vee E_3(s{ij})\vee x_{ij}) \land (\neg x'{ij}\vee E_3(s{ij})\vee E_2(s_{ij})). $$

Each occurrence of $E_2$ and $E_3$ is replaced by the clauses generated by the auxiliary cardinality variables. This produces a CNF formula containing $x'{ij}$, $x{ij}$, the neighboring variables, and the auxiliary variables introduced by the cardinality encoding.

The sharing improvement described in the text is obtained by not building eight independent encodings for the neighborhoods. Adjacent cells have overlapping neighborhoods, so the partial-sum variables corresponding to common groups of cells are identical. The same auxiliary variables can therefore be used in the transition clauses of every cell that contains the corresponding group of neighbors. The resulting CNF has substantially fewer auxiliary variables while representing exactly the same Life transition relation.

Verification

For part (a), every assignment violating the Life rule belongs to $\mathcal{B}$ and falsifies its associated clause $C(a)$. Hence no violating assignment satisfies the CNF formula. Conversely, if an assignment satisfies the Life rule, it differs from every $a\in\mathcal{B}$ in at least one position, so every clause $C(a)$ has a true literal. Hence every satisfying assignment of the CNF formula is a valid Life transition.

For part (b), the auxiliary variables satisfy the Bailleux and Boufkhad clauses exactly when they represent the corresponding cardinality relations. Therefore the expressions $E_2(s_{ij})$ and $E_3(s_{ij})$ are true precisely when the neighborhood has exactly two or exactly three live cells. Substitution into

$$ x'{ij}\iff (s{ij}=3)\vee(x_{ij}=1\land s_{ij}=2) $$

gives the required Life rule. Sharing auxiliary variables between neighboring cells only identifies equal intermediate results and does not alter the represented Boolean function.

This completes the proof. ∎

Notes

The direct encoding in part (a) is conceptually simple but grows exponentially with the number of inputs to one transition rule. The auxiliary-variable encoding in part (b) replaces this truth-table expansion by a polynomial-size representation of the relevant counting conditions, which is the form suitable for SAT solvers.