.. -*- coding: utf-8 -*- .. role:: sref(numref) .. role:: xref(numref) .. Copyright (C) 2025, Wolfgang Scherer, .. This file is part of HDP Sudoku. .. Permission is granted to copy, distribute and/or modify this document .. under the terms of the GNU Free Documentation License, Version 1.3 .. or any later version published by the Free Software Foundation; .. with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. .. A copy of the license is included in the section entitled "GNU .. Free Documentation License". .. inline comments (with du_comment_role) .. role:: rem(comment) .. role:: html(raw) :format: html .. role:: shx(code) :language: sh .. rst-class:: narrow xmedium xlarge xhuge xultra ################################################## :rem:`|||:sec:|||`\ Bit Counter ################################################## .. . (progn (forward-line 1) (snip-insert "rst_b.peek-a-boo" t t "rst") (insert "")) .. >>CODD See `the components of a doctoral dissertation and their order `_ .. >>CODD Dedication .. >>CODD Epigraph .. >>CODD Abstract 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*. .. \|:here:| .. >>CODD Introduction .. . ||:here:|| .. . |:here:| ================================================== :rem:`|||:sec:|||`\ Truth Table ================================================== For 3 input bits |A|, |B| and |C|, the outputs |S0| and |S1| shall reflect the number of 1 bits at the inputs as a binary number, where :math:`{S}_{{0}} = 2^0` and :math:`{S}_{{1}} = 2^1` . In :xref:`tab:Truth table for bit counter`, the definitions for the logical functions of |S0| and |S1| are shown. .. |0| replace:: **0** .. |1| replace:: **1** .. |A| replace:: :math:`A` .. |B| replace:: :math:`B` .. |C| replace:: :math:`C` .. |S0| replace:: :math:`S_0` .. |S1| replace:: :math:`S_1` .. |SM| replace:: :math:`\mathbb{S}` .. |SM0| replace:: :math:`\mathbb{S}_0` .. |SM1| replace:: :math:`\mathbb{S}_1` .. _`tab:Truth table for bit counter`: .. table:: Truth table for bit counter +-----+-----+-----+------+------+ | |A| | |B| | |C| | |S1| | |S0| | +=====+=====+=====+======+======+ | |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| | +-----+-----+-----+------+------+ ================================================== :rem:`|||:sec:|||`\ Processing |S0| ================================================== The conjunctive normal form (|CNF|) for |S0| is derived from truth table :xref:`tab:Truth table for bit counter` by constructing an |implicate|, which is a disjunctive clause that becomes false for each of the inputs, when the output is false: .. math:: :label: s0_cnf \begin{array}{rcl} S_0 & = & ( \hphantom{\neg}A \vee \hphantom{\neg}B \vee \hphantom{\neg}C ) \wedge{} \\ &&( \hphantom{\neg}A \vee \neg B \vee \neg C ) \wedge{} \\ &&( \neg A \vee \hphantom{\neg}B \vee \neg C ) \wedge{} \\ &&( \neg A \vee \neg B \vee \hphantom{\neg}C ) \end{array} Complementary Assignment (distributive expansion, multiplication) of :eq:`s0_cnf` delivers a special disjunctive normal form (|DNF|) containing all prime |implicant|\ s called the Blake canonical form (|BCF|) for |S0|: .. math:: :label: s0_bcf \begin{array}{rcl} S_0&=& ( \neg A \wedge \neg B \wedge \hphantom{\neg}C ) \vee{} \\ &&( \neg A \wedge \hphantom{\neg}B \wedge \neg C ) \vee{} \\ &&( \hphantom{\neg}A \wedge \neg B \wedge \neg C ) \vee{} \\ &&( \hphantom{\neg}A \wedge \hphantom{\neg}B \wedge \hphantom{\neg}C ) \end{array} Complementary Assignment of |BCF| :eq:`s0_bcf` delivers the set of prime |implicate|\ s for |S0|: .. math:: :label: s0_prime_implicates \begin{array}{rcl} S_0 & = & ( \neg A \vee \neg B \vee \hphantom{\neg}C ) \\ &&( \neg A \vee \hphantom{\neg}B \vee \neg C ) \wedge{} \\ &&( \hphantom{\neg}A \vee \neg B \vee \neg C ) \wedge{} \\ &&( \hphantom{\neg}A \vee \hphantom{\neg}B \vee \hphantom{\neg}C ) \wedge{} \end{array} Adding a clause for each variable to :eq:`s0_cnf` containing the variable and its negation delivers the extended |CNF| for mapping to a *satoku matrix*: .. math:: :label: s0_cnf_var \begin{array}{rcl} S_0 & = & ( \hphantom{\neg}A \vee \hphantom{\neg}B \vee \hphantom{\neg}C ) \wedge{} \\ &&( \hphantom{\neg}A \vee \neg B \vee \neg C ) \wedge{} \\ &&( \neg A \vee \hphantom{\neg}B \vee \neg C ) \wedge{} \\ &&( \neg A \vee \neg B \vee \hphantom{\neg}C ) \wedge{} \\ &&( \hphantom{\neg}A \vee \neg A ) \wedge{} \\ &&( \hphantom{\neg}B \vee \neg B ) \wedge{} \\ &&( \hphantom{\neg}C \vee \neg C ) \end{array} .. raw:: latex \pagebreak[4] A *satoku matrix* |SM| is based on an inverted symmetric |adjacency matrix|. In :xref:`fig:Satoku matrix SM0 for S0` the *satoku matrix* |SM0| is mapped from the extended |CNF| formula :eq:`s0_cnf_var` for |S0|, analogous to mapping a SAT problem to an independent set problem [MOUNT2012]_, pp. 92. The clauses are mapped to :math:`\color{green}{r_{0_{0_{0}}} \dots r_{3_{2_{3}}}}`, the variables are mapped to :math:`\color{blue}{r_{4_{0_{4}}} \dots r_{6_{1_{6}}}}`, The region at :math:`\color{red}{r_{0_{0_{4}}} \dots r_{3_{2_{6}}}}` reflects the originally required variables for each input |CNF|. .. _`fig:Satoku matrix SM0 for S0`: .. figure:: _static/bit-counter-s0.n.v-000-color.svg :alt: Satoku matrix |SM0| for |S0| :align: center :scale: 50% *Satoku matrix** |SM0| for |S0| .. raw:: latex \pagebreak[3] Since *state rows* :math:`s_{0_{0}}` and :math:`s_{1_{0}}` are *independent*, because *conflict relationship* :math:`\color{green}{s_{0_{0_{1_{0}}}} \neq 0}` and *conflict relationship* :math:`\color{blue}{s_{1_{0_{0_{0}}}} \neq 0}` and the relevant *conflict subsequences* :math:`\color{red}{r_{0_{0_{2}}} \dots r_{0_{0_{3}}}}` and :math:`\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* :math:`\color{green}{s_{0_{0_{1_{1}}}} := 0, s_{0_{0_{1_{2}}}} := 0}`, which makes *conflict relationship* :math:`\color{green}{s_{0_{0_{1_{0}}}}}` *required*, and setting *conflict relationships* :math:`\color{blue}{s_{1_{0_{0_{1}}}} := 0, s_{1_{0_{0_{2}}}} := 0}`, which makes *conflict relationship* :math:`\color{blue}{s_{1_{0_{0_{0}}}}}` *required*. (See :xref:`fig:State rows maths_0_0 and maths_1_0 joined in SM0`). .. _`fig:State rows maths_0_0 and maths_1_0 joined in SM0`: .. figure:: _static/bit-counter-s0.n.v-001-join-s00-s10-00-color.svg :alt: bit-counter-s0.n.v-001-join-s00-s10-00-color.svg :align: center :scale: 50% *State rows* :math:`s_{0_{0}}` and :math:`s_{1_{0}}` *joined* in |SM0| :rem:`_` .. raw:: latex \pagebreak[3] After *consolidating* the *satoku matrix* |SM0| by propagating the *conflict relationships* of *required* states, it presents *state rows* :math:`\color{green}{s_{0_{0}}}` and :math:`\color{blue}{s_{1_{0}}}` *joined* as shown in :xref:`fig:State rows maths_0_0 and maths_1_0 joined and consolidated in SM0`. Additional consequences from the advance decision were detected during *consolidation* in *state rows* :math:`\color{red}{s_{0_{1}}, s_{0_{2}}, s_{1_{1}}, s_{1_{2}}}`. .. _`fig:State rows maths_0_0 and maths_1_0 joined and consolidated in SM0`: .. figure:: _static/bit-counter-s0.n.v-001-join-s00-s10-01-color.svg :alt: bit-counter-s0.n.v-001-join-s00-s10-01-color.svg :align: center :scale: 50% *State rows* :math:`s_{0_{0}}` and :math:`s_{1_{0}}` *joined* and *consolidated* in |SM0| :rem:`_` .. raw:: latex \pagebreak[3] 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* |SM|. 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* :math:`\color{green}{s_{2_{0}}}` and :math:`\color{blue}{s_{3_{0}}}` are *independent* and their relevant *conflict subsequences* are equal, they can be *joined* by :math:`\color{red}{\mbox{making each other required}}` as shown in :xref:`fig:State rows maths_2_0 and maths_3_0 joined in SM0`. .. _`fig:State rows maths_2_0 and maths_3_0 joined in SM0`: .. figure:: _static/bit-counter-s0.n.v-002-join-s20-s30-00-color.svg :alt: bit-counter-s0.n.v-002-join-s20-s30-00-color.svg :align: center :scale: 50% *State rows* :math:`s_{2_{0}}` and :math:`s_{3_{0}}` *joined* in |SM0| :rem:`_` .. raw:: latex \pagebreak[4] *Conflict* propagation during *consolidation* has affected the entire *satoku matrix* |SM0| as shown in :xref:`fig:State rows maths_2_0 and maths_3_0 joined and consolidated in SM0`. *Cell* :math:`\color{green}{c_{0_{1}}}` shows that all *state rows* from *cell* :math:`c_{1_{1}}` are *required* and therefore *cell matrix row* :math:`\color{red}{c_{1}}` can be removed from the *satoku matrix*. The same holds for *cell row* :math:`\color{red}{c_{3}}` based on the *required* *conflict relationships* in *cell* :math:`\color{blue}{c_{2_{3}}}`. .. _`fig:State rows maths_2_0 and maths_3_0 joined and consolidated in SM0`: .. figure:: _static/bit-counter-s0.n.v-002-join-s20-s30-01-consolidated-color.svg :alt: bit-counter-s0.n.v-002-join-s20-s30-01-consolidated-color.svg :align: center :scale: 50% *State rows* :math:`s_{2_{0}}` and :math:`s_{3_{0}}` *joined* and *consolidated* in |SM0| :rem:`_` .. raw:: latex \pagebreak[3] In :xref:`fig:Redundancies removed from SM0` the redundant *cell matrix rows* are removed. Counting the *possible* *conflict relationships* in *cell* :math:`\color{red}{c_{0_{1}}}` reveals that *merging* both *cell matrix rows* :math:`{c_{0}}` and :math:`{c_{1}}` will only result in a maximum of 4 *state rows* in *cell matrix row* :math:`{c_{5}}`. *Cells* :math:`\color{green}{c_{5_{0}}}` and :math:`\color{blue}{c_{5_{1}}}` have been prepared to *require* all combinations of *state rows* allowed by :math:`\color{red}{c_{0_{1}}}`. .. _`fig:Redundancies removed from SM0`: .. figure:: _static/bit-counter-s0.n.v-003-red-00-color.svg :alt: bit-counter-s0.n.v-003-red-00-color.svg :align: center :scale: 50% Redundancies removed from |SM0| :rem:`_` .. raw:: latex \pagebreak[4] In :xref:`fig:Cell matrix rows mathc_0 and mathc_1 merged in SM0 BCF in cell matrix row mathc_5 maths_5_0 dots s_5_3` the *cell matrix rows* :math:`\color{green}{c_{0}}` and :math:`\color{blue}{c_{1}}` have been *merged* and *satoku matrix* |SM0| reveals a set of |implicant|\ s for |S0| in *cell matrix row* :math:`\color{red}{c_5}` at range :math:`\color{red}{r_{5_{0_{2}}} \dots r_{5_{3_{4}}}}`. It is further possible to remove the *cell matrix rows* :math:`\color{green}{c_{0}}` and :math:`\color{blue}{c_{1}}` from *satoku matrix* |SM0| since they are fully *absorbed* by *cells* :math:`\color{orange}{c_{5_{0}}}` and :math:`\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* :math:`\color{orange}{c_{6_{5}}}`. .. _`fig:Cell matrix rows mathc_0 and mathc_1 merged in SM0 BCF in cell matrix row mathc_5 maths_5_0 dots s_5_3`: .. figure:: _static/bit-counter-s0.n.v-004-merge-c0-c1-00-color.svg :alt: bit-counter-s0.n.v-004-merge-c0-c1-00-color.svg :align: center :scale: 50% *Cell matrix rows* :math:`c_{0}` and :math:`c_{1}` *merged* in |SM0|, implicants at range :math:`r_{5_{0_{2}}} \dots r_{5_{3_{4}}}` :rem:`_` .. raw:: latex \pagebreak[3] In :xref:`fig:Cell matrix rows mathc_0 and mathc_1 removed and mathc_3 permuted in mathc_4 BCF at range mathr_4_0_0 dots r_4_3_2 in SM0`, *cell matrix rows* :math:`c_{0}'` and :math:`c_{1}'` have been removed from *satoku matrix* |SM0|. *Consolidation* has generated a *state row* permutation of *cell matrix row* :math:`\color{green}{c_{3}}` in *cell matrix row* :math:`\color{blue}{c_{4}}`. The set of conjuctions defined at range :math:`\color{magenta}{r_{4_{0_{0}}} \dots r_{4_{3_{2}}}}` is now identical to the |BCF| for |S0| in :eq:`s0_bcf`. .. _`fig:Cell matrix rows mathc_0 and mathc_1 removed and mathc_3 permuted in mathc_4 BCF at range mathr_4_0_0 dots r_4_3_2 in SM0`: .. figure:: _static/bit-counter-s0.n.v-005-permute-c5-00-color.svg :alt: bit-counter-s0.n.v-005-permute-c5-00-color.svg :align: center :scale: 50% *Cell matrix rows* :math:`c_{0}'` and :math:`c_{1}'` removed, :math:`c_{3}` permuted into :math:`c_{4}`, |BCF| at range :math:`r_{4_{0_{0}}} \dots r_{4_{3_{2}}}` in |SM0| .. raw:: latex \pagebreak[3] ================================================== :rem:`|||:sec:|||`\ Processing |S1| ================================================== .. . |:here:| The conjunctive normal form (|CNF|) for |S1| is derived from truth table :xref:`tab:Truth table for bit counter`: .. math:: :label: s1_cnf \begin{array}{rcl} S_1 & = & ( \hphantom{\neg}A \vee \hphantom{\neg}B \vee \hphantom{\neg}C ) \wedge{} \\ &&( \hphantom{\neg}A \vee \hphantom{\neg}B \vee \neg C ) \wedge{} \\ &&( \hphantom{\neg}A \vee \neg B \vee \hphantom{\neg}C ) \wedge{} \\ &&( \neg A \vee \hphantom{\neg}B \vee \hphantom{\neg}C ) \end{array} Complementary Assignment (distributive expansion, multiplication) of :eq:`s1_cnf` delivers a special disjunctive normal form (|DNF|) containing all prime |implicant|\ s called the Blake canonical form (|BCF|) for |S1|: .. math:: :label: s1_bcf \begin{array}{rcl} S_1&=& ( \hphantom{\neg}B \wedge \hphantom{\neg}C ) \vee{} \\ &&( \hphantom{\neg}A \wedge \hphantom{\neg}C ) \vee{} \\ &&( \hphantom{\neg}A \wedge \hphantom{\neg}B ) \end{array} Complementary Assignment of |BCF| :eq:`s1_bcf` delivers the set of prime |implicate|\ s for |S1|: .. math:: :label: s1_prime_implicates \begin{array}{rcl} S_1&=& ( \hphantom{\neg}B \vee \hphantom{\neg}C ) \wedge{} \\ &&( \hphantom{\neg}A \vee \hphantom{\neg}C ) \wedge{} \\ &&( \hphantom{\neg}A \vee \hphantom{\neg}B ) \end{array} Adding a clause for each variable to :eq:`s1_cnf` containing the variable and its negation delivers the extended |CNF| for mapping to a *satoku matrix*: .. math:: :label: s1_cnf_var \begin{array}{rcl} ( \hphantom{\neg}A \vee \hphantom{\neg}B \vee \hphantom{\neg}C ) \wedge{} \\ &&( \hphantom{\neg}A \vee \hphantom{\neg}B \vee \neg C ) \wedge{} \\ &&( \hphantom{\neg}A \vee \neg B \vee \hphantom{\neg}C ) \wedge{} \\ &&( \neg A \vee \hphantom{\neg}B \vee \hphantom{\neg}C ) \\ &&( \hphantom{\neg}A \vee \neg A ) \wedge{} \\ &&( \hphantom{\neg}B \vee \neg B ) \wedge{} \\ &&( \hphantom{\neg}C \vee \neg C ) \end{array} .. raw:: latex \pagebreak[3] In :xref:`Fig:Satoku matrix SM1 for S1` the *satoku matrix* |SM1| is mapped from the |CNF| formula :eq:`s1_cnf_var` for |S1|. .. _`fig:Satoku matrix SM1 for S1`: .. figure:: _static/bit-counter-s1.n.v-000.svg :alt: Satoku matrix |SM1| for |S1| :align: center :scale: 50% *Satoku matrix* |SM1| for |S1| :rem:`_` .. raw:: latex \pagebreak[3] In :xref:`fig:Identify mathmboxMCCRr_0_0_3 for expansion`, *Cell row* :math:`\color{red}{r_{0_{0_3}}}` is a *minor conflict* *cell row*, :math:`\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* :math:`\color{red}{s_{0_{0}}}` with *state row* :math:`\color{green}{s_{3_{1}}}`, which is prepared in *cell rows* :math:`\color{red}{r_{7_{0_{0}}}}` and :math:`\color{green}{r_{7_{0_{3}}}}`, and by *merging* *state row* :math:`\color{red}{s_{0_{0}}}` with *state row* :math:`\color{blue}{s_{3_{2}}}`, which is prepared in *cell rows* :math:`\color{red}{r_{7_{1_{0}}}}` and :math:`\color{blue}{r_{7_{1_{3}}}}`. *Cell row* :math:`\color{red}{r_{7_{2_{0}}}}` expresses the fact that alternatively :math:`\color{red}{s_{0_{1}}}` or :math:`\color{red}{s_{0_{2}}}` can become *required*. .. _`fig:Identify mathmboxMCCRr_0_0_3 for expansion`: .. figure:: _static/bit-counter-s1.n.v-001-mccr-00-color.svg :alt: bit-counter-s1.n.v-001-mccr-00-color.svg :align: center :scale: 50% Identify :math:`\mbox{MCCR}(r_{0_{0_3}})` for expansion in |SM1|. :rem:`_` .. raw:: latex \pagebreak[4] The expansion of *minor conflict* *cell rows* :math:`\color{red}{r_{0_{0_3}}}`, :math:`\color{green}{r_{0_{1_2}}}`, and :math:`\color{blue}{r_{0_{2_1}}}` is shown in :xref:`fig:mathmboxMCCRr_0_0_3 mathmboxMCCRr_0_1_2 mathmboxMCCRr_0_2_1 expanded` at *cells matrix rows* :math:`\color{red}{c_{7}}`, :math:`\color{green}{c_{8}}`, and :math:`\color{blue}{c_{9}}`. *Cell* :math:`\color{magenta}{c_{7_{8}}}` signifies, that *cell matrix rows* :math:`\color{red}{c_{7}}` and :math:`\color{green}{c_{8}}` can be *reduced* to a single *cell matrix row* with 5 *state rows*. .. _`fig:mathmboxMCCRr_0_0_3 mathmboxMCCRr_0_1_2 mathmboxMCCRr_0_2_1 expanded`: .. figure:: _static/bit-counter-s1.n.v-001-mccr-01-color.svg :alt: bit-counter-s1.n.v-001-mccr-01-color.svg :align: center :scale: 50% :math:`\mbox{MCCR}(r_{0_{0_3}})`, :math:`\mbox{MCCR}(r_{0_{1_2}})`, :math:`\mbox{MCCR}(r_{0_{2_1}})` expanded in |SM1| :rem:`_` .. raw:: latex \pagebreak[3] In :xref:`fig:Identify conflict subsequences s_10_0 s_10_2 and absorbed cell matrix rows c_0 c_7 c_8 in SM1` the relevant *conflict subsequences* of *state rows* :math:`\color{green}{s_{{10}_{0}}}` and :math:`\color{blue}{s_{{10}_{2}}}` are identifed as equal, and therefore *state row* :math:`\color{blue}{s_{{10}_{2}}}` can be removed. Further, *cells* :math:`\color{red}{c_{{10}_{0}}}`, :math:`\color{red}{c_{{10}_{7}}}` and :math:`\color{red}{c_{{10}_{8}}}` signify that *cell matrix rows* :math:`\color{red}{c_{{0}}}`, :math:`\color{red}{c_{{7}}}` and :math:`\color{red}{c_{{8}}}` are *absorbed* and can be removed from |SM1|. .. _`fig:Identify conflict subsequences s_10_0 s_10_2 and absorbed cell matrix rows c_0 c_7 c_8 in SM1`: .. figure:: _static/bit-counter-s1.n.v-002-merge-sub-red-00-color.svg :alt: bit-counter-s1.n.v-002-merge-sub-red-00-color.svg :align: center :scale: 45% Identify *conflict subsequences* :math:`{s_{{10}_{0}}}`, :math:`{s_{{10}_{2}}}` and *absorbed* *cell matrix rows* :math:`{c_{{0}}}`, :math:`{c_{{7}}}`, :math:`{c_{{8}}}` in |SM1| :rem:`_` .. raw:: latex \pagebreak[3] .. figure:: _static/bit-counter-s1.n.v-002-merge-sub-red-01-color.svg :alt: bit-counter-s1.n.v-002-merge-sub-red-01-color.svg :align: center :scale: 50% bit-counter-s1.n.v-002-merge-sub-red-01.svg :rem:`_` .. raw:: latex \pagebreak[3] .. figure:: _static/bit-counter-s1.n.v-002-merge-sub-red-02-color.svg :alt: bit-counter-s1.n.v-002-merge-sub-red-02-color.svg :align: center :scale: 50% bit-counter-s1.n.v-002-merge-sub-red-02.svg :rem:`_` .. raw:: latex \pagebreak[3] .. figure:: _static/bit-counter-s1.n.v-002-merge-sub-red-03-color.svg :alt: bit-counter-s1.n.v-002-merge-sub-red-03-color.svg :align: center :scale: 50% bit-counter-s1.n.v-002-merge-sub-red-03.svg :rem:`_` .. In :xref:`Fig:Processed satoku matrix SM1 for S1 BCF in cell matrix row mathc_5 maths_5_0 dots s_5_2` *satoku matrix* |SM1| reveals the |BCF| for |S1| in *cell matrix row* :math:`c_5` (:math:`r_{5_{0_{2}}} \dots r_{5_{2_{4}}}`). .. _`fig:Processed satoku matrix SM1 for S1 BCF in cell matrix row mathc_5 maths_5_0 dots s_5_2`: .. figure:: _static/bit-counter-s1.n.v-001-mccr-10-remove-3-state-redundancies-color.svg :alt: Processed satoku matrix |SM1| for |S1| :align: center :scale: 50% Processed *satoku matrix* |SM1| for |S1|, |BCF| in *cell matrix row* :math:`c_5` (:math:`r_{5_{0_{2}}} \dots r_{5_{2_{4}}}`) .. raw:: latex \newpage .. >>CODD Chapter .. >>CODD Conclusion .. >>CODD Appendix A .. . |:here:| ================================================== :rem:`|||:sec:|||`\ Alternative Resolution of |S0| ================================================== .. figure:: _static/bit-counter-s0.n.v-010-mmcr-00.svg :alt: bit-counter-s0.n.v-010-mmcr-00.svg :align: center :scale: 50% bit-counter-s0.n.v-010-mmcr-00.svg :rem:`_` .. raw:: latex \pagebreak[3] .. figure:: _static/bit-counter-s0.n.v-010-mmcr-01.svg :alt: bit-counter-s0.n.v-010-mmcr-01.svg :align: center :scale: 50% bit-counter-s0.n.v-010-mmcr-01.svg :rem:`_` .. raw:: latex \pagebreak[4] .. figure:: _static/bit-counter-s0.n.v-010-mmcr-02.svg :alt: bit-counter-s0.n.v-010-mmcr-02.svg :align: center :scale: 40% bit-counter-s0.n.v-010-mmcr-02.svg :rem:`_` .. raw:: latex \pagebreak[3] .. figure:: _static/bit-counter-s0.n.v-010-mmcr-03.svg :alt: bit-counter-s0.n.v-010-mmcr-03.svg :align: center :scale: 40% bit-counter-s0.n.v-010-mmcr-03.svg :rem:`_` .. raw:: latex \pagebreak[4] .. figure:: _static/bit-counter-s0.n.v-010-mmcr-04.svg :alt: bit-counter-s0.n.v-010-mmcr-04.svg :align: center :scale: 50% bit-counter-s0.n.v-010-mmcr-04.svg :rem:`_` .. raw:: latex \pagebreak[3] .. figure:: _static/bit-counter-s0.n.v-010-mmcr-05.svg :alt: bit-counter-s0.n.v-010-mmcr-05.svg :align: center :scale: 50% bit-counter-s0.n.v-010-mmcr-05.svg :rem:`_` .. raw:: latex \pagebreak[4] .. figure:: _static/bit-counter-s0.n.v-010-mmcr-06.svg :alt: bit-counter-s0.n.v-010-mmcr-06.svg :align: center :scale: 50% bit-counter-s0.n.v-010-mmcr-06.svg :rem:`_` .. raw:: latex \pagebreak[3] .. figure:: _static/bit-counter-s0.n.v-010-mmcr-07.svg :alt: bit-counter-s0.n.v-010-mmcr-07.svg :align: center :scale: 50% bit-counter-s0.n.v-010-mmcr-07.svg :rem:`_` .. raw:: latex \pagebreak[4] .. figure:: _static/bit-counter-s0.n.v-010-mmcr-08.svg :alt: bit-counter-s0.n.v-010-mmcr-08.svg :align: center :scale: 50% bit-counter-s0.n.v-010-mmcr-08.svg :rem:`_` .. raw:: latex \pagebreak[3] .. figure:: _static/bit-counter-s0.n.v-010-mmcr-09.svg :alt: bit-counter-s0.n.v-010-mmcr-09.svg :align: center :scale: 50% bit-counter-s0.n.v-010-mmcr-09.svg :rem:`_` .. raw:: latex \pagebreak[3] .. \||:here:|| .. >>CODD Notes .. ================================================== .. :rem:`|||:sec:|||`\ Footnotes .. ================================================== :html:`
` .. \[#] .. \|:info:| put local references here .. \|:info:| put local definitions here .. include:: doc_defs.inc .. include:: abbrev_defs.inc .. include:: doc_defs_combined.inc .. .. \||<-snap->|| doc_standalone .. include:: doc/doc_defs_secret.inc .. \||<-snap->|| doc_standalone .. \||<-snap->|| not_doc_standalone .. include:: doc_defs_secret.inc .. \||<-snap->|| not_doc_standalone .. _`Wolfgang Scherer`: wolfgang.scherer@gmx.de