A satoku matrix is an inverted adjacency matrix preserving clause boundary information for implementing a requirement update algorithm (see figure 1.3).

A satoku matrix \(\mathbb{S}\) is formally defined as a sequence
of *cell-matrix rows* \(c_{i},\; 0 \le i < |\mathbb{S}|\), where a
\(\mbox{\it cell-matrix row}\) \(c_i\) consists of *cells*
\(c_{i_g},\: 0 \le g < |\mathbb{S}|\). A *cell* \(c_{i_g}\)
consists of *cell rows* \(r_{i_{j_g}},\; 0 \le j < |c_{i_g}|\),
where a *cell row* \(r_{i_{j_g}}\) consists of *states*
\(s_{i_{j_{g_h}}},\; 0 \le h < |r_{i_{j_g}}|\). A *state*
\(s_{i_{j_{g_h}}}\) represents a *conflict relationship* CFR with
the *state* \(s_{g_{h_{i_j}}}\), where a *conflict relationship*
is either \(\mbox{\it possible} = 1\) or \(\mbox{\it
impossible} = 0\). A *state row* \(s_{i_j},\; 0 \le j < |c_{i_i}|\)
is the sequence of *cell rows* \(r_{i_{j_g}}\). The index scheme
is summarized in table 1.1.

For better readability, if a *cell row* \(r_{i_{j_g}}\) contains
more than one 1-state, all 1-states in \(r_{i_{j_g}}\) are
represented by a dash (-) (see figure 1.1).

Merging a sequence of *state rows* \(S\) into a *state row*
\(s_{i_j}\), denoted as \(\mathbf{Mrg}(s_{i_j}, S)\), is
defined by the algorithm in figure 1.2. It returns the number of \(1 \rightarrow 0\)
transitions performed.

\(\mathsf{transitions} \leftarrow 0\)

\(s_{i_{j_{e_f}}}' = 0,\; \def\pluseq{\mathrel{+}\mathrel{\mkern-2mu}=} \mathsf{transitions}\pluseq 1\)

\(s_{e_{f_{i_j}}}' = 0,\; \def\pluseq{\mathrel{+}\mathrel{\mkern-2mu}=} \mathsf{transitions}\pluseq 1\)

The requirement update algorithm in figure 1.3 distributes conflict relationships into all *cell rows*
which have a single 1-state. After applying the requirement update
algorithm, the satoku matrix \(\mathbb{S}\) is called
*consolidated*.

\(\mathsf{transitions} \leftarrow 1\)

\(\mathsf{transitions} \leftarrow 0\)

\(\def\pluseq{\mathrel{+}\mathrel{\mkern-2mu}=} \mathsf{transitions}\pluseq \mathbf{Mrg}(s_{i_j}, s_{g_h})\)
*// merge state row* \(s_{g_h}\) *into state row* \(s_{i_j}\)

The consolidated version of the Satoku Matrix Index Scheme Example from figure 1.1 is shown in figure 1.4. Notably \(s_{0_{2_{3_1}}}\) triggered a merge of \(s_{3_1}\) into \(s_{0_2}\). This led to state \(s_{3_{1_{1_2}}}\) causing \(1 \rightarrow 0\) transitions of state \(s_{0_{2_{1_2}}}\) and state \(s_{1_{2_{0_2}}}\).

A CNF formula \(F\) is a conjunction of \(m\) disjunctive clauses \(C_i\) each containing \(k_i\) literals \(l_j\), where a literal \(l_j\) is a negated or unnegated boolean variable:

\[\def\Nz{\mathbb{N}_0}%
\def\inNz#1{#1\in\Nz}%
F = \mathop{{\bigwedge}_{\mathstrut}}\limits_{i=0}^{m-1} \, C_i,\: m=|F|,\quad C_i = \mathop{{\bigvee}_{\!\!\mathstrut i}}\limits_{j=0}^{k_i-1} \, l_j,\: k_i = |C_i|,\quad \inNz{m,\!k_i}.\]

Mapping a CNF formula \(F\) to a satoku matrix \(\mathbb{S}\)
with the algorithm in figure 2.1 results in an *unconsolidated* satoku matrix
\(\mathbb{S}\).

extend each state row \(s_{e_f}\), by \(|C_i|\) 1-states, \(0 \le e < i,\: 0 \le f < |c_{e_e}|\)

add \(|C_i|\) state rows with \(\sum_{n=0}^{i}\, |C_n|\) 1-states each

\(s_{i_{j_{i_h}}} \leftarrow 0\)

\(s_{i_{h_{i_j}}} \leftarrow 0\)

\(s_{i_{j_{g_h}}} \leftarrow 0\)

\(s_{g_{h_{i_j}}} \leftarrow 0\)

See figure 3.1 for an algorithm to map a satoku matrix to a CNF formula.

start with empty CNF formula \(F\) (a conjunctive clause)

add an empty disjunctive clause \(C_i\) to \(F\)

add an unnegated variable \(v_{i_j}\) to clause \(C_i\)

to express the conclusion \(v_{i_{j}} \rightarrow \neg v_{i_{f}}\),

add the disjunctive clause \(\neg v_{i_{j}} \vee \neg v_{i_{f}}\) to \(|F|\)

add the disjunctive clause \(\neg v_{i_{j}} \vee \neg v_{e_{f}}\) to \(|F|\)

Arbitrary pixel blocks like “*HAPPYEASTER!<smile><egg><egg>*” can be
encoded in the upper right half of a satoku matrix in a simple manner
by flipping 1-states to 0 (see figure 4.1).

The satoku matrix in figure 4.1 can then be mapped to CNF formula (see figure 6.1). Since this formula is huge, only a reduced version is shown here in figure 4.2.

Mapping the CNF formula in figure 4.2 to an unconsolidated satoku matrix, effectively hides the encoded information (see figure 4.3).

Performing the requirement update (figure 1.3) to the satoku matrix in figure 4.3 results in a consolidated satoku matrix, which shows the restored original information (see figure 4.4).

Removing the at-least-1 clauses from the reduced CNF formula in figure 4.3 results in a set of 2-literal clauses (see figure 5.1). For the full formula in figure 6.1 without at-least-1 clauses see figure 7.1.

Producing a consolidated satoku matrix from the formula in figure 5.1 lacks any information whatsoever (see figure 5.2).

When the variables of the CNF formula in figure 5.1 are mapped via 2-literal clauses of the form \(( p \vee \neg p )\), only the conflict relationships between the clauses and variables become visible (see figure 5.3)

Only when the requirement update algorithm in figure 1.3 is applied to the unconsolidated satoku matrix in figure 5.3 the information reappears in the lower right mapped variable quadrant (see figure 5.4).

The mapped variable quadrant of the satoku matrix derived from the full CNF formula in figure 7.1 already hints strongly at the encoded message (see figure 5.5).

The original message can be restored by adding the at-least-1 clauses manually to the mapped variable quadrant from figure 5.4 and making exactly one mapped variable required in the lower right quadrant for each literal of the at-least-1 clauses (see figure 5.6).

Running the requirement update algorithm from figure 1.3 consolidates the satoku matrix from figure 5.6 and restores the original message in the lower right Quadrant (see figure 5.7).

Removing the mapped variables finally leaves an exact copy of the original message (see figure 5.8).