A bit counter for 3 bits is presented as an example for determining the Blake normal form (sum of prime implicants) of a logical formula in conjunctive normal form using the satoku matrix.
For 3 input bits \(A\), \(B\) and \(C\), the outputs \(S_0\) and \(S_1\) shall reflect the number of 1 bits at the inputs as a binary number, where \({S}_{{0}} = 2^0\) and \({S}_{{1}} = 2^1\) .
In table 2.1, the definitions for the logical functions of \(S_0\) and \(S_1\) are shown.
| \(A\) | \(B\) | \(C\) | \(S_1\) | \(S_0\) |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 0 |
| 0 | 0 | 1 | 0 | 1 |
| 0 | 1 | 0 | 0 | 1 |
| 0 | 1 | 1 | 1 | 0 |
| 1 | 0 | 0 | 0 | 1 |
| 1 | 0 | 1 | 1 | 0 |
| 1 | 1 | 0 | 1 | 0 |
| 1 | 1 | 1 | 1 | 1 |
The conjunctive normal form (CNF) for \(S_0\) is derived from truth table table 2.1 by constructing an implicate, which is a disjunctive clause that becomes false for each of the inputs, when the output is false:
Complementary Assignment (distributive expansion, multiplication) of (2.1) delivers a special disjunctive normal form (DNF) containing all prime implicants called the Blake canonical form (BCF) for \(S_0\):
Complementary Assignment of BCF (2.2) delivers the set of prime implicates for \(S_0\):
Adding a clause for each variable to (2.1) containing the variable and its negation delivers the extended CNF for mapping to a satoku matrix:
A satoku matrix \(\mathbb{S}\) is based on an inverted symmetric adjacency matrix.
In figure 2.1 the satoku matrix \(\mathbb{S}_0\) is mapped from the extended CNF formula (2.4) for \(S_0\), analogous to mapping a SAT problem to an independent set problem [MOUNT2012], pp. 92.
The clauses are mapped to \(\color{green}{r_{0_{0_{0}}} \dots r_{3_{2_{3}}}}\), the variables are mapped to \(\color{blue}{r_{4_{0_{4}}} \dots r_{6_{1_{6}}}}\), The region at \(\color{red}{r_{0_{0_{4}}} \dots r_{3_{2_{6}}}}\) reflects the originally required variables for each input CNF.
figure 2.1 Satoku matrix* \(\mathbb{S}_0\) for \(S_0\)
Since state rows \(s_{0_{0}}\) and \(s_{1_{0}}\) are independent, because conflict relationship \(\color{green}{s_{0_{0_{1_{0}}}} \neq 0}\) and conflict relationship \(\color{blue}{s_{1_{0_{0_{0}}}} \neq 0}\) and the relevant conflict subsequences \(\color{red}{r_{0_{0_{2}}} \dots r_{0_{0_{3}}}}\) and \(\color{red}{r_{1_{0_{2}}} \dots r_{1_{0_{3}}}}\) are equal, they can be joined by making each other required, i.e setting conflict relationships \(\color{green}{s_{0_{0_{1_{1}}}} := 0, s_{0_{0_{1_{2}}}} := 0}\), which makes conflict relationship \(\color{green}{s_{0_{0_{1_{0}}}}}\) required, and setting conflict relationships \(\color{blue}{s_{1_{0_{0_{1}}}} := 0, s_{1_{0_{0_{2}}}} := 0}\), which makes conflict relationship \(\color{blue}{s_{1_{0_{0_{0}}}}}\) required. (See figure 2.2).
figure 2.2 State rows \(s_{0_{0}}\) and \(s_{1_{0}}\) joined in \(\mathbb{S}_0\)
After consolidating the satoku matrix \(\mathbb{S}_0\) by propagating the conflict relationships of required states, it presents state rows \(\color{green}{s_{0_{0}}}\) and \(\color{blue}{s_{1_{0}}}\) joined as shown in figure 2.3.
Additional consequences from the advance decision were detected during consolidation in state rows \(\color{red}{s_{0_{1}}, s_{0_{2}}, s_{1_{1}}, s_{1_{2}}}\).
figure 2.3 State rows \(s_{0_{0}}\) and \(s_{1_{0}}\) joined and consolidated in \(\mathbb{S}_0\)
This technique is an arbitrary (but not random!) advance decision to select a state when another state is selected and vice versa. The decision has no consequence on the satisfiability of the problem, since both states are equal at the time of the advance decision. Note, that these advance decisions can only be made in a consolidated satoku matrix \(\mathbb{S}\). Therefore, it is not valid to join more than 2 states at a time.
Also note, that assignments to variables have no strong connection to selections from a clause. I.e., just because one literal of a clause becomes true, it does not preclude any other literal of the clause becoming true. Further, the advance decision does not affect the current global state of any variables.
Since state rows \(\color{green}{s_{2_{0}}}\) and \(\color{blue}{s_{3_{0}}}\) are independent and their relevant conflict subsequences are equal, they can be joined by \(\color{red}{\mbox{making each other required}}\) as shown in figure 2.4.
figure 2.4 State rows \(s_{2_{0}}\) and \(s_{3_{0}}\) joined in \(\mathbb{S}_0\)
Conflict propagation during consolidation has affected the entire satoku matrix \(\mathbb{S}_0\) as shown in figure 2.5. Cell \(\color{green}{c_{0_{1}}}\) shows that all state rows from cell \(c_{1_{1}}\) are required and therefore cell matrix row \(\color{red}{c_{1}}\) can be removed from the satoku matrix. The same holds for cell row \(\color{red}{c_{3}}\) based on the required conflict relationships in cell \(\color{blue}{c_{2_{3}}}\).
figure 2.5 State rows \(s_{2_{0}}\) and \(s_{3_{0}}\) joined and consolidated in \(\mathbb{S}_0\)
In figure 2.6 the redundant cell matrix rows are removed.
Counting the possible conflict relationships in cell \(\color{red}{c_{0_{1}}}\) reveals that merging both cell matrix rows \({c_{0}}\) and \({c_{1}}\) will only result in a maximum of 4 state rows in cell matrix row \({c_{5}}\).
Cells \(\color{green}{c_{5_{0}}}\) and \(\color{blue}{c_{5_{1}}}\) have been prepared to require all combinations of state rows allowed by \(\color{red}{c_{0_{1}}}\).
figure 2.6 Redundancies removed from \(\mathbb{S}_0\)
In figure 2.7 the cell matrix rows \(\color{green}{c_{0}}\) and \(\color{blue}{c_{1}}\) have been merged and satoku matrix \(\mathbb{S}_0\) reveals a set of implicants for \(S_0\) in cell matrix row \(\color{red}{c_5}\) at range \(\color{red}{r_{5_{0_{2}}} \dots r_{5_{3_{4}}}}\). It is further possible to remove the cell matrix rows \(\color{green}{c_{0}}\) and \(\color{blue}{c_{1}}\) from satoku matrix \(\mathbb{S}_0\) since they are fully absorbed by cells \(\color{orange}{c_{5_{0}}}\) and \(\color{orange}{c_{5_{1}}}\). This results in a net decrease of the matrix size. Finally, a state row permutation has been prepared in cell \(\color{orange}{c_{6_{5}}}\).
figure 2.7 Cell matrix rows \(c_{0}\) and \(c_{1}\) merged in \(\mathbb{S}_0\), implicants at range \(r_{5_{0_{2}}} \dots r_{5_{3_{4}}}\)
In figure 2.8, cell matrix rows \(c_{0}'\) and \(c_{1}'\) have been removed from satoku matrix \(\mathbb{S}_0\). Consolidation has generated a state row permutation of cell matrix row \(\color{green}{c_{3}}\) in cell matrix row \(\color{blue}{c_{4}}\). The set of conjuctions defined at range \(\color{magenta}{r_{4_{0_{0}}} \dots r_{4_{3_{2}}}}\) is now identical to the BCF for \(S_0\) in (2.2).
figure 2.8 Cell matrix rows \(c_{0}'\) and \(c_{1}'\) removed, \(c_{3}\) permuted into \(c_{4}\), BCF at range \(r_{4_{0_{0}}} \dots r_{4_{3_{2}}}\) in \(\mathbb{S}_0\)
The conjunctive normal form (CNF) for \(S_1\) is derived from truth table table 2.1:
Complementary Assignment (distributive expansion, multiplication) of (2.5) delivers a special disjunctive normal form (DNF) containing all prime implicants called the Blake canonical form (BCF) for \(S_1\):
Complementary Assignment of BCF (2.6) delivers the set of prime implicates for \(S_1\):
Adding a clause for each variable to (2.5) containing the variable and its negation delivers the extended CNF for mapping to a satoku matrix:
In figure 2.9 the satoku matrix \(\mathbb{S}_1\) is mapped from the CNF formula (2.8) for \(S_1\).
figure 2.9 Satoku matrix \(\mathbb{S}_1\) for \(S_1\)
In figure 2.10, Cell row \(\color{red}{r_{0_{0_3}}}\) is a minor conflict cell row, \(\mbox{MCCR}(r_{i_{j_g}})\equiv |\mbox{P}(r_{i_{j_g}})| = 2\), containing 2 possible conflict relationships. The consequences can be inspected by merging state row \(\color{red}{s_{0_{0}}}\) with state row \(\color{green}{s_{3_{1}}}\), which is prepared in cell rows \(\color{red}{r_{7_{0_{0}}}}\) and \(\color{green}{r_{7_{0_{3}}}}\), and by merging state row \(\color{red}{s_{0_{0}}}\) with state row \(\color{blue}{s_{3_{2}}}\), which is prepared in cell rows \(\color{red}{r_{7_{1_{0}}}}\) and \(\color{blue}{r_{7_{1_{3}}}}\). Cell row \(\color{red}{r_{7_{2_{0}}}}\) expresses the fact that alternatively \(\color{red}{s_{0_{1}}}\) or \(\color{red}{s_{0_{2}}}\) can become required.
figure 2.10 Identify \(\mbox{MCCR}(r_{0_{0_3}})\) for expansion in \(\mathbb{S}_1\).
The expansion of minor conflict cell rows \(\color{red}{r_{0_{0_3}}}\), \(\color{green}{r_{0_{1_2}}}\), and \(\color{blue}{r_{0_{2_1}}}\) is shown in figure 2.11 at cells matrix rows \(\color{red}{c_{7}}\), \(\color{green}{c_{8}}\), and \(\color{blue}{c_{9}}\). Cell \(\color{magenta}{c_{7_{8}}}\) signifies, that cell matrix rows \(\color{red}{c_{7}}\) and \(\color{green}{c_{8}}\) can be reduced to a single cell matrix row with 5 state rows.
figure 2.11 \(\mbox{MCCR}(r_{0_{0_3}})\), \(\mbox{MCCR}(r_{0_{1_2}})\), \(\mbox{MCCR}(r_{0_{2_1}})\) expanded in \(\mathbb{S}_1\)
In figure 2.12 the relevant conflict subsequences of state rows \(\color{green}{s_{{10}_{0}}}\) and \(\color{blue}{s_{{10}_{2}}}\) are identifed as equal, and therefore state row \(\color{blue}{s_{{10}_{2}}}\) can be removed. Further, cells \(\color{red}{c_{{10}_{0}}}\), \(\color{red}{c_{{10}_{7}}}\) and \(\color{red}{c_{{10}_{8}}}\) signify that cell matrix rows \(\color{red}{c_{{0}}}\), \(\color{red}{c_{{7}}}\) and \(\color{red}{c_{{8}}}\) are absorbed and can be removed from \(\mathbb{S}_1\).
figure 2.12 Identify conflict subsequences \({s_{{10}_{0}}}\), \({s_{{10}_{2}}}\) and absorbed cell matrix rows \({c_{{0}}}\), \({c_{{7}}}\), \({c_{{8}}}\) in \(\mathbb{S}_1\)
figure 2.13 bit-counter-s1.n.v-002-merge-sub-red-01.svg
figure 2.14 bit-counter-s1.n.v-002-merge-sub-red-02.svg
figure 2.15 bit-counter-s1.n.v-002-merge-sub-red-03.svg
figure 2.16 bit-counter-s0.n.v-010-mmcr-00.svg
figure 2.17 bit-counter-s0.n.v-010-mmcr-01.svg
figure 2.18 bit-counter-s0.n.v-010-mmcr-02.svg
figure 2.19 bit-counter-s0.n.v-010-mmcr-03.svg
figure 2.20 bit-counter-s0.n.v-010-mmcr-04.svg
figure 2.21 bit-counter-s0.n.v-010-mmcr-05.svg
figure 2.22 bit-counter-s0.n.v-010-mmcr-06.svg
figure 2.23 bit-counter-s0.n.v-010-mmcr-07.svg
figure 2.24 bit-counter-s0.n.v-010-mmcr-08.svg
figure 2.25 bit-counter-s0.n.v-010-mmcr-09.svg