.. -*- coding: utf-8 -*- .. role:: sref(numref) .. role:: xref(numref) .. Copyright (C) 2023, Wolfgang Scherer, .. This file is part of Satoku Matrix Oreganography. .. 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 .. >>CODD Introduction .. .. \||<-snap->|| not_doc_slides ================================================== :rem:`|||:sec:|||`\ Introduction ================================================== .. \||<-snap->|| not_doc_slides .. >>CODD Chapter ================================================== :rem:`|||:sec:|||`\ Satoku Matrix ================================================== A satoku matrix is an inverted adjacency matrix preserving clause boundary information for implementing a requirement update algorithm (see :xref:`fig:requirement update algorithm`). A satoku matrix :math:`\mathbb{S}` is formally defined as a sequence of *cell-matrix rows* :math:`c_{i},\; 0 \le i < |\mathbb{S}|`, where a :math:`\mbox{\it cell-matrix row}` :math:`c_i` consists of *cells* :math:`c_{i_g},\: 0 \le g < |\mathbb{S}|`. A *cell* :math:`c_{i_g}` consists of *cell rows* :math:`r_{i_{j_g}},\; 0 \le j < |c_{i_g}|`, where a *cell row* :math:`r_{i_{j_g}}` consists of *states* :math:`s_{i_{j_{g_h}}},\; 0 \le h < |r_{i_{j_g}}|`. A *state* :math:`s_{i_{j_{g_h}}}` represents a *conflict relationship* CFR with the *state* :math:`s_{g_{h_{i_j}}}`, where a *conflict relationship* is either :math:`\mbox{\it possible} = 1` or :math:`\mbox{\it impossible} = 0`. A *state row* :math:`s_{i_j},\; 0 \le j < |c_{i_i}|` is the sequence of *cell rows* :math:`r_{i_{j_g}}`. The index scheme is summarized in :xref:`tab:Satoku Matrix Index Scheme`. .. _`tab:Satoku Matrix Index Scheme`: .. table:: Satoku Matrix Index Scheme +----------------------------------------------+ | .. image:: _static/sm-index-scheme-table.png | | | +----------------------------------------------+ For better readability, if a *cell row* :math:`r_{i_{j_g}}` contains more than one 1-state, all 1-states in :math:`r_{i_{j_g}}` are represented by a dash (`-`) (see :xref:`fig:Satoku Matrix Index Scheme Example`). .. _`fig:Satoku Matrix Index Scheme Example`: .. figure:: _static/sm-index-scheme-example.png :scale: 50% Satoku Matrix Index Scheme Example .. raw:: latex \newpage Merging a sequence of *state rows* :math:`S` into a *state row* :math:`s_{i_j}`, denoted as :math:`\mathbf{Mrg}(s_{i_j}, S)`, is defined by the algorithm in :xref:`fig:Merge State Rows S Into State Row s_i_j`. It returns the number of :math:`1 \rightarrow 0` transitions performed. .. _`fig:Merge State Rows S Into State Row s_i_j`: .. figctr:: Merge State Rows :math:`S` Into State Row :math:`s_{i_j}` | **def** :math:`\mathbf{Mrg}(s_{i_j}, S)`: | :math:`\mathsf{transitions} \leftarrow 0` | **for each** state row :math:`s_{g_h} \in S`: | **for each** state :math:`s_{i_{j_{e_f}}},\; 0 \le e < |\mathbb{S}|,\: 0 \le f < |r_{i_{j_e}}|`: | **if** :math:`s_{i_{j_{e_f}}} \neq 0` **and** :math:`s_{g_{h_{e_f}}} = 0`: | :math:`s_{i_{j_{e_f}}}' = 0,\; \def\pluseq{\mathrel{+}\mathrel{\mkern-2mu}=} \mathsf{transitions}\pluseq 1` | **if** :math:`s_{e_{f_{i_j}}} \neq 0`: | :math:`s_{e_{f_{i_j}}}' = 0,\; \def\pluseq{\mathrel{+}\mathrel{\mkern-2mu}=} \mathsf{transitions}\pluseq 1` | **return** :math:`\mathsf{transitions}` The requirement update algorithm in :xref:`fig:requirement update algorithm` distributes conflict relationships into all *cell rows* which have a single 1-state. After applying the requirement update algorithm, the satoku matrix :math:`\mathbb{S}` is called *consolidated*. .. _`fig:requirement update algorithm`: .. figctr:: Requirement Update Algorithm | :math:`\mathsf{transitions} \leftarrow 1` | **while** :math:`\mathsf{transitions} > 0`: | :math:`\mathsf{transitions} \leftarrow 0` | **for each** state row :math:`s_{i_j}`: | **for each** cell row :math:`r_{i_{j_g}},\; i \neq g`: | **if** there is only a single 1-state :math:`s_{i_{j_{g_h}}} = 1,\: \sum_{f=0}^{|r_{i_{j_g}}|-1}\,s_{i_{j_{g_f}}} = 1`: | :math:`\def\pluseq{\mathrel{+}\mathrel{\mkern-2mu}=} \mathsf{transitions}\pluseq \mathbf{Mrg}(s_{i_j}, s_{g_h})` *// merge state row* :math:`s_{g_h}` *into state row* :math:`s_{i_j}` The consolidated version of the Satoku Matrix Index Scheme Example from :xref:`fig:Satoku Matrix Index Scheme Example` is shown in :xref:`fig:Consolidated Satoku Matrix Index Scheme Example`. Notably :math:`s_{0_{2_{3_1}}}` triggered a merge of :math:`s_{3_1}` into :math:`s_{0_2}`. This led to state :math:`s_{3_{1_{1_2}}}` causing :math:`1 \rightarrow 0` transitions of state :math:`s_{0_{2_{1_2}}}` and state :math:`s_{1_{2_{0_2}}}`. .. _`fig:Consolidated Satoku Matrix Index Scheme Example`: .. figure:: _static/sm-index-scheme-example-consolidated.mtx.png :scale: 50% Consolidated Satoku Matrix Index Scheme Example .. raw:: latex \newpage ============================================================ :rem:`|||:sec:|||`\ Mapping a CNF Formula to a Satoku Matrix ============================================================ A CNF formula :math:`F` is a conjunction of :math:`m` disjunctive clauses :math:`C_i` each containing :math:`k_i` literals :math:`l_j`, where a literal :math:`l_j` is a negated or unnegated boolean variable: .. math:: \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 :math:`F` to a satoku matrix :math:`\mathbb{S}` with the algorithm in :xref:`fig:Mapping a CNF Formula to a Satoku Matrix` results in an *unconsolidated* satoku matrix :math:`\mathbb{S}`. .. _`fig:Mapping a CNF Formula to a Satoku Matrix`: .. figctr:: Mapping a CNF Formula to a Satoku Matrix | **for each** clause :math:`C_i` of CNF formula :math:`F,\; 0 \le i < |F|`: | extend each state row :math:`s_{e_f}`, by :math:`|C_i|` 1-states, :math:`0 \le e < i,\: 0 \le f < |c_{e_e}|` | add :math:`|C_i|` state rows with :math:`\sum_{n=0}^{i}\, |C_n|` 1-states each | *// process at-most-1 constraints* | **for each** cell row :math:`r_{i_{j_i}},\; 0 \le j < |C_i|-1`: | **for each** state :math:`s_{i_{j_{i_h}}},\; j < h < |C_i|`: | :math:`s_{i_{j_{i_h}}} \leftarrow 0` | :math:`s_{i_{h_{i_j}}} \leftarrow 0` | *// process conflict relationships* | **for each** state row :math:`s_{i_j},\; 0 \le i < |F|,\: 0 \le j < |C_i|`: | **for each** cell row :math:`r_{i_{j_g}},\; i < g < |F|`: | **for each** state :math:`s_{i_{j_{g_h}}},\; 0 \le h < |C_g|`: | **if** :math:`C_{i_j} \wedge C_{g_h} = 0`: | :math:`s_{i_{j_{g_h}}} \leftarrow 0` | :math:`s_{g_{h_{i_j}}} \leftarrow 0` .. raw:: latex \newpage ============================================================ :rem:`|||:sec:|||`\ Mapping a Satoku Matrix to a CNF Formula ============================================================ See :xref:`fig:Mapping a Satoku Matrix to a CNF Formula` for an algorithm to map a satoku matrix to a CNF formula. .. _`fig:Mapping a Satoku Matrix to a CNF Formula`: .. figctr:: Mapping a Satoku Matrix to a CNF Formula | start with empty CNF formula :math:`F` (a conjunctive clause) | **for each** cell :math:`c_{i_i},\; 0 \le i < |\mathbb{S}|`: | add an empty disjunctive clause :math:`C_i` to :math:`F` | **for each** cell row :math:`r_{i_{j_i}},\; 0 \le j < |c_{i_i}|`: | add an unnegated variable :math:`v_{i_j}` to clause :math:`C_i` | **for each** state row :math:`s_{i_j},\; 0 \le i < |\mathbb{S}|,\: 0 \le j < |c_{i_i}|`: | **with** cell row :math:`r_{i_{j_i}}`: | **for each** state :math:`s_{i_{j_{i_f}}},\; j < f < |r_{i_{j_i}}|`: | **if** :math:`s_{i_{j_{i_f}}} = 0`: | to express the conclusion :math:`v_{i_{j}} \rightarrow \neg v_{i_{f}}`, | add the disjunctive clause :math:`\neg v_{i_{j}} \vee \neg v_{i_{f}}` to :math:`|F|` | **for each** cell row :math:`r_{i_{j_e}},\; i < e < |\mathbb{S}|`: | **for each** state :math:`s_{i_{j_{e_f}}},\; 0 \le f < |r_{i_{j_e}}|`: | **if** :math:`s_{i_{j_{e_f}}} = 0`: | add the disjunctive clause :math:`\neg v_{i_{j}} \vee \neg v_{e_{f}}` to :math:`|F|` .. raw:: latex \newpage ================================================== :rem:`|||:sec:|||`\ Initial Information Encoding ================================================== Arbitrary pixel blocks like "*HAPPYEASTER!*" can be encoded in the upper right half of a satoku matrix in a simple manner by flipping 1-states to 0 (see :xref:`fig:Text Encoded in a Satoku Matrix`). .. _`fig:Text Encoded in a Satoku Matrix`: .. figure:: _static/oreganography-000.mtx.png :scale: 50% Text Encoded in a Satoku Matrix The satoku matrix in :xref:`fig:Text Encoded in a Satoku Matrix` can then be mapped to CNF formula (see :xref:`fig:Satoku Matrix Mapped to CNF Formula`). Since this formula is huge, only a reduced version is shown here in :xref:`fig:Reduced CNF Formula of Mapped Satoku Matrix`. .. _`fig:Reduced CNF Formula of Mapped Satoku Matrix`: .. figure:: _static/oreganography-encoded-cut.frm.png :scale: 75% Reduced CNF Formula of Mapped Satoku Matrix .. raw:: latex \newpage Mapping the CNF formula in :xref:`fig:Reduced CNF Formula of Mapped Satoku Matrix` to an unconsolidated satoku matrix, effectively hides the encoded information (see :xref:`fig:Reduced CNF Formula Mapped to Unconsolidated Satoku Matrix`). .. _`fig:Reduced CNF Formula Mapped to Unconsolidated Satoku Matrix`: .. figure:: _static/oreganography-encoded-cut.n-000.mtx.png :scale: 39% Reduced CNF Formula Mapped to Unconsolidated Satoku Matrix .. raw:: latex \newpage Performing the requirement update (:xref:`fig:requirement update algorithm`) to the satoku matrix in :xref:`fig:Reduced CNF Formula Mapped to Unconsolidated Satoku Matrix` results in a consolidated satoku matrix, which shows the restored original information (see :xref:`fig:Consolidated Satoku Matrix for Reduced CNF Formula`). .. _`fig:Consolidated Satoku Matrix for Reduced CNF Formula`: .. figure:: _static/oreganography-encoded-cut.n-001.mtx.png :scale: 44% Consolidated Satoku Matrix for Reduced CNF Formula .. raw:: latex \newpage ================================================== :rem:`|||:sec:|||`\ Advanced Information Hiding ================================================== Removing the at-least-1 clauses from the reduced CNF formula in :xref:`fig:Reduced CNF Formula Mapped to Unconsolidated Satoku Matrix` results in a set of 2-literal clauses (see :xref:`fig:Reduced CNF Formula Without At-Least-1 Clauses`). For the full formula in :xref:`fig:Satoku Matrix Mapped to CNF Formula` without at-least-1 clauses see :xref:`fig:CNF formula without at-least-1 clauses`. .. _`fig:Reduced CNF Formula Without At-Least-1 Clauses`: .. figure:: _static/oreganography-encoded-no-min-1-cut.frm.png :scale: 75% Reduced CNF Formula Without At-Least-1 Clauses .. raw:: latex %% \newpage Producing a consolidated satoku matrix from the formula in :xref:`fig:Reduced CNF Formula Without At-Least-1 Clauses` lacks any information whatsoever (see :xref:`fig:Consolidated Satoku Matrix for Reduced CNF Formula Without At-Least-1 Clauses`). .. _`fig:Consolidated Satoku Matrix for Reduced CNF Formula Without At-Least-1 Clauses`: .. figure:: _static/oreganography-encoded-no-min-1-cut-000.mtx.png :scale: 45% Consolidated Satoku Matrix for Reduced CNF Formula Without At-Least-1 Clauses .. raw:: latex \newpage When the variables of the CNF formula in :xref:`fig:Reduced CNF Formula Without At-Least-1 Clauses` are mapped via 2-literal clauses of the form :math:`( p \vee \neg p )`, only the conflict relationships between the clauses and variables become visible (see :xref:`fig:Unconsolidated Satoku Matrix of Reduced CNF With Mapped Variables`) .. _`fig:Unconsolidated Satoku Matrix of Reduced CNF With Mapped Variables`: .. figure:: _static/oreganography-encoded-no-min-1-cut.n.v-000.mtx.png :scale: 35% Unconsolidated Satoku Matrix of Reduced CNF With Mapped Variables .. raw:: latex \newpage Only when the requirement update algorithm in :xref:`fig:requirement update algorithm` is applied to the unconsolidated satoku matrix in :xref:`fig:Unconsolidated Satoku Matrix of Reduced CNF With Mapped Variables` the information reappears in the lower right mapped variable quadrant (see :xref:`fig:Consolidated Satoku Matrix of Reduced CNF With Mapped Variables`). .. _`fig:Consolidated Satoku Matrix of Reduced CNF With Mapped Variables`: .. figure:: _static/oreganography-encoded-no-min-1-cut.v-000.mtx.png :scale: 33% Consolidated Satoku Matrix of Reduced CNF With Mapped Variables .. raw:: latex \newpage The mapped variable quadrant of the satoku matrix derived from the full CNF formula in :xref:`fig:CNF formula without at-least-1 clauses` already hints strongly at the encoded message (see :xref:`fig:Mapped Variable Quadrant of Full CNF Formula Without At-Least-1 Clauses`). .. _`fig:Mapped Variable Quadrant of Full CNF Formula Without At-Least-1 Clauses`: .. figure:: _static/oreganography-encoded-no-min-1-only.v-000.mtx.png :scale: 31% Mapped Variable Quadrant of Full CNF Formula Without At-Least-1 Clauses .. raw:: latex \newpage The original message can be restored by adding the at-least-1 clauses manually to the mapped variable quadrant from :xref:`fig:Consolidated Satoku Matrix of Reduced CNF With Mapped Variables` and making exactly one mapped variable required in the lower right quadrant for each literal of the at-least-1 clauses (see :xref:`fig:At-Least-1 Clauses Manually Added to Mapped Variable Quadrant`). .. _`fig:At-Least-1 Clauses Manually Added to Mapped Variable Quadrant`: .. figure:: _static/oreganography-encoded-no-min-1-cut-only-v-reconstruct-000.mtx.png :scale: 43% At-Least-1 Clauses Manually Added to Mapped Variable Quadrant .. raw:: latex \newpage Running the requirement update algorithm from :xref:`fig:requirement update algorithm` consolidates the satoku matrix from :xref:`fig:At-Least-1 Clauses Manually Added to Mapped Variable Quadrant` and restores the original message in the lower right Quadrant (see :xref:`fig:Requirement Update Restores Original Message`). .. _`fig:Requirement Update Restores Original Message`: .. figure:: _static/oreganography-encoded-no-min-1-cut-only-v-reconstruct-001.mtx.png :scale: 43% Requirement Update Restores Original Message .. raw:: latex \newpage Removing the mapped variables finally leaves an exact copy of the original message (see :xref:`fig:Removing Mapped Variables Leaves Exact Copy of Original Message`). .. _`fig:Removing Mapped Variables Leaves Exact Copy of Original Message`: .. figure:: _static/oreganography-encoded-no-min-1-only-v-reconstruct-002.mtx.png :scale: 50% Removing Mapped Variables Leaves Exact Copy of Original Message .. >>CODD Conclusion .. >>CODD Appendix A .. raw:: latex \newpage %% \appendix %% \counterwithin{figure}{chapter} %% \counterwithin{table}{chapter} %% \counterwithin{literalblock}{chapter} %% \counterwithin{figure}{section} %% \counterwithin{table}{section} %% \counterwithin{literalblock}{section} ======================================================== :rem:`|||:sec:|||`\ Satoku Matrix Mapped to CNF Formula ======================================================== .. _`fig:Satoku Matrix Mapped to CNF Formula`: .. figure:: _static/oreganography-encoded.frm.png :scale: 50% Satoku Matrix Mapped to CNF Formula .. raw:: latex \newpage ========================================================== :rem:`|||:sec:|||`\ CNF Formula Without At-Least-1 Clauses ========================================================== .. _`fig:CNF formula without at-least-1 clauses`: .. figure:: _static/oreganography-encoded-no-min-1.frm.png :scale: 50% CNF formula without at-least-1 clauses .. \|: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