On the Smallest Size of Internal Collage Systems

We call a nonterminal reachable if it appears as a node label of the grammar tree, and otherwise unreachable. Then, a collage system is internal if and only if every nonterminal is reachable. Our algorithm processes unreachable nonterminals $X$ in a top-down manner and modifies the collage system to represent $T$ without using $X$. When we get into an unreachable nonterminal $X$, all nonterminals above have been processed to be reachable, and therefore, $X$ is referred to only by truncation rules because referring to $X_i$ in a rule other than truncation rules implies that $X$ is reachable. Hence, removing $X$ from the collage system is equivalent to removing the truncation rules that refer to $X$. The process of removing these truncation rules depends on the following cases:

• $\mathrm{■}$

  Case 0: When the truncation rule can be replaced with an atomic rule.

• $\mathrm{■}$

  Case 1: When the truncation can be made from a single smaller nonterminal.

• $\mathrm{■}$

  Case 2: When the truncation can be made from more than two repeating nonterminals.

• $\mathrm{■}$

  Case 3: When the truncation can be made from two nonterminals.

Case 0 is the base case where $X\to a$ is an atomic rule. For any nonterminal $Q$ that truncates $X$, it means that $⟨Q⟩=a$ and it is obvious that the truncation rule can be replaced with $Q\to a$.

Suppose that we want to remove a truncation rule $Q\to X[b..e)$. Case 1 deals with the following situations:

• $\mathrm{■}$

  When $X\to YZ$ and the interval $[b..e)$ is included in either one of $[1..|⟨Y⟩|]$ or $[|⟨Y⟩|+1..|⟨Z⟩|]$.

• $\mathrm{■}$

  When $X\to Y^r$ and the interval $[b..e)$ is covered by a single $Y$, i.e., $[b..e)$ is included in $[(r^{\prime }-1)|⟨Y⟩|+1..r^{\prime }|⟨Y⟩|]$ for some $r^{\prime }\in [1..r]$.

• $\mathrm{■}$

  When $X\to Y[b^{\prime }..e^{\prime })$.

In either case, it is easy to replace the truncation rule $Q\to X[b..e)$ with a rule that truncates a smaller nonterminal $Y$ or $Z$. If the smaller nonterminal is unreachable, the added truncation rule will be processed later when we get into the nonterminal.

Case 2 deals with a truncation rule $Q\to X[b..e)$ that truncates unreachable nonterminal $X$ with repetition rule $X\to Y^r$ spanning more than two $Y$’s. In this case, $⟨Q⟩$ can be represented by $uvw$, where $u$ is a (potentially empty) suffix of $⟨Y⟩$, $v={⟨Y⟩}^{r^{\prime }}$ with $r^{\prime }\ge 1$ and $w$ is a (potentially empty) prefix of $⟨Y⟩$. We add a new nonterminal $U$ (resp. $W$) with a rule that truncates $Y$ to represent $u$ (resp. $w$) if $u$ (resp. $w$) is not the empty string. We also add a new nonterminal $V$ with repetition rule $V\to Y^{r^{\prime }}$ if $r^{\prime }>1$.⁴⁴4If $r^{\prime }=2$, the added rule is categorized to concatenation rules in our definition. Finally, we can represent $Q$ by concatenating at most three nonterminals for $u$, $v$ and $w$ using at most two concatenation rules. The process increases the size of the collage system by at most four because we create at most five rules and remove the original truncation rule $Q\to X[b..e)$. Note that $Y$ is reachable because $Q$ is reachable by inductive hypothesis and there is a path from $Q$ to $Y$ without truncation. Hence, added rules that truncate $Y$ do not need to be processed later.

Case 3 deals with rules that truncate an unreachable nonterminal $X$ with concatenation or repetition rule spanning exactly two nonterminals. We focus on the case with concatenation rule $X\to YZ$ as the case with repetition rule can be processed similarly. Let $A$ be the set of all rules that truncate $X$ and their truncated intervals are not included in $[1..|⟨Y⟩|]$ nor $[|⟨Y⟩|+1..|⟨X⟩|]$. Unlike other cases, we process all truncation rules in $A$ at once.

Let $s$ (resp. $p$) be the length of the longest suffix (resp. prefix) truncated from $Y$ (resp. $Z$) by a truncation rule in $A$. We create a new nonterminal $S$ that truncates the suffix of length $s$ of $Y$ and $P$ that truncates the prefix of length $p$ of $Z$. Then, any truncation made by a rule in $A$ can be replaced with concatenation of a nonterminal that truncates $S$ (or $S$ itself) and a nonterminal that truncates $P$ (or $P$ itself). This increases the size of the collage system by at most two per truncation rule in $A$. Note that any nonterminal, including $S$ and $P$, created during the process is reachable through the nonterminals in the lefthand sides of $A$, which are reachable by inductive hypothesis. Also, $S$ and $P$ are the only nonterminals that are created in the process and may truncate unreachable nonterminals, which will be processed later.

Each modification to the collage system does not change the string it represents. Since all nonterminals added during the process are reachable, the collage system becomes internal when we go through the process of removing unreachable nonterminals in the original collage system.

The number of nonterminals in the collage system is increased by the process of removing a rule that truncates unreachable nonterminals by four in Case 2 and by two in Case 3. We have to take care of additional rules $S$ and $P$ created in Case 3 that may truncate unreachable nonterminals. The number of such additional truncation rules is bounded by $2(m-m_{\mathrm{𝗍𝗋}})$ in total, where $m_{\mathrm{𝗍𝗋}}$ is the number of truncation rules in the original collage system. Thus, the size of the resulting internal collage system is bounded by $m+4(2(m-m_{\mathrm{𝗍𝗋}})+m_{\mathrm{𝗍𝗋}})=9m-4m_{\mathrm{𝗍𝗋}}\le 9m$.

In every case, we can process a truncation rule in $O(1)$ time each. While the truncation rule is completely removed in Case 0, Case 2 and Case 3, what we do in Case 1 is just switching its reference nonterminal to smaller nonterminals in $O(1)$ time. This switching cost may add up to $O(m)$ until we finally remove it in Case 0, Case 2 or Case 3. Since we remove $O(m)$ truncation rules, the algorithm runs in $O(m^2)$ time. $◀$

It follows from Theorem 3 that $\widehat{c}(T)\le 9c(T)$. Together with the fact that $c(T)\le \widehat{c}(T)$, we get the following theorem:

Suppose that $T=F_1\mathrm{\cdots }{F}_h$ is the ICS-factorization of an internal collage system $G$. Let $L_i$ denote the $i$-th leaf of the grammar tree of $G$. We categorize a factor $F_k$ longer than $1$ and set integers $i_k$ and $j_k$ as follows.

• $\mathrm{■}$

  If $L_k$ is labeled with a nonterminal $X$, then $F_k$ is type-A. Since $L_k$ is not the leftmost node with label $X$, we can set integers so that $L_{i_k},L_{i_k+1},\mathrm{\dots },L_{j_k}$ are the leaves under the internal node with label $X$ to satisfy condition (i). The interval $[s_{i_k}..s_{j_k+1})$ in $I_1$ corresponds to the internal node $X$.

• $\mathrm{■}$

  If $L_k$ is the right child of a nonterminal $X$ with a repetition rule $X\to Y^r$, then $F_k$ is type-B. We can set integer $i_k$ so that $L_{i_k},L_{i_k+1},\mathrm{\dots },L_{k-1}$ are the leaves under the left child of $X$ to satisfy condition (i). The interval $[s_{i_k}..s_{j_k+1})$ in $I_2$ corresponds to the left child of $X$, while the interval $[s_{i_k}..s_{k+1})$ in $I_3$ corresponds to the internal node $X$.

• $\mathrm{■}$

  If $L_k$ is the child of a nonterminal $X$ with a truncation rule $X\to Y[b..e)$, then $F_k$ is type-C. We can set integers $i_k$ and $j_k$ so that $L_{i_k},L_{i_k+1},\mathrm{\dots },L_{j_k}$ are the leaves under the internal node with label $Y$ to satisfy condition (i). The interval $[s_{i_k}..s_{j_{k+1}})$ in $I_4$ corresponds to the internal node $Y$.

As seen above, every interval in $I$ corresponds to a node of the grammar tree, and hence, it is compatible with tree structures. Also, the interval of a type-B factor corresponds to a leaf node labeled with $Y^{r-1}$, which implies that it is not in $I$. Finally, we prove condition (iv). For any factor $F_k$ longer than $1$, we have set $i_k$ and $j_k$ so that $F_k$ is derived from a nonterminal that refers to smaller nonterminals deriving $F_{i_k}\mathrm{\cdots }{F}_{j_k}$. Since $G$ does not have a reference loop of nonterminals, there is no reference loop of factors, too. Hence, we can assign integer $D_k$ to $F_k$ so that $D_k$ is larger than integers $\{D_{i_k},\mathrm{\dots },D_{j_k}\}$ assigned to factors it refers to. Assigning $0$ to a factor of length $1$, we see that condition (iv) holds.

Given that every factor $F_k$ longer than $1$ is categorized into types to satisfy conditions (i), (ii), (iii) and (iv). We can define a reference structure of factors according to condition (i). Referring to a type-B factor alone is avoided by condition (iii), and it is guaranteed by condition (iv) that there is no reference loop of factors. By condition (ii), $I$ can identify the intervals corresponding to nodes of a tree, which are sufficient to define a reference structure of nonterminals. Although not all nodes are identified, we can fill missing internal nodes by adding concatenation rules to build an internal collage system for the ICS-factorization. $◀$

We modify the MAX-SAT formulation in [4] for RLSLPs to encode valid ICS-factorizations of smallest internal collage systems based on Lemma 6. We say that an ICS-factor longer than $1$ refers to the substring $T[s_{i_k}..s_{j_{k+1}})$ defined in Lemma 6 for each type. Let us call an integer $D_k$ satisfying condition (iii) of Lemma 6 the reference depth of factor $F_k$ or the characters covered by $F_k$. Note that a type-C factor may refer to a string to the right while type-A and type-B factors always refer to a substring to the left, which adds some complication to our formulation compared to the previous one for RLSLPs. We will encode reference depths to ensure that there is no reference loop.

In the next paragraph, we will define several Boolean variables with multiple parameters in subscripts. For any variable $x$ with some missing subscripts specified by “$\circ$”, let $⟦x⟧$ denote the set of (possibly tuples of) feasible subscripts to fill the missing part(s). For example, $⟦{\mathrm{𝑟𝑒𝑓}}_{\circ \leftarrow \circ ,\circ }^{\mathrm{A}}⟧=\{(i^{\prime },i,\mathrm{\ell })\mid i\in [1..n-1],\mathrm{\ell }\in [2..n-i+1],i^{\prime }\in [1..i-\mathrm{\ell }],T[i^{\prime }..i^{\prime }+\mathrm{\ell })=T[i..i+\mathrm{\ell })\}$, and for some fixed $i$ and $\mathrm{\ell }$, $⟦{\mathrm{𝑟𝑒𝑓}}_{\circ \leftarrow i,\mathrm{\ell }}^{\mathrm{A}}⟧=\{i^{\prime }\mid (i^{\prime },i,\mathrm{\ell })\in ⟦{\mathrm{𝑟𝑒𝑓}}_{\circ \leftarrow \circ ,\circ }^{\mathrm{A}}⟧\}$. We also use “$\bullet$” to represent anonymous (arbitrary) subscripts, which are filtered out when used in $⟦x⟧$. For example, $⟦{\mathrm{𝑟𝑒𝑓}}_{\bullet \leftarrow \circ ,\circ }^{\mathrm{A}}⟧=\{(i,\mathrm{\ell })\mid (i^{\prime },i,\mathrm{\ell })\in ⟦{\mathrm{𝑟𝑒𝑓}}_{\circ \leftarrow \circ ,\circ }^{\mathrm{A}}⟧\}$.

For a given text $T[1..n]$ of length $n$, we define Boolean variables as follows to encode Lemma 6.

• $\mathrm{■}$

  $f_{i,\mathrm{\ell }}$ for $i\in [1..n]$ and $\mathrm{\ell }\in [1..n+1-i]$: $f_{i,\mathrm{\ell }}=1$ iff $T[i..i+\mathrm{\ell })$ is an ICS-factor.

• $\mathrm{■}$

  $p_i$ for $i\in [1..n+1]$: For $i\ne n+1$, $p_i=1$ iff $i$ is the starting position of an ICS-factor. $p_{n+1}$ exists for technical reasons. We set $p_1=p_{n+1}=1$.

• $\mathrm{■}$

  ${\mathrm{𝑟𝑒𝑓}}_{i^{\prime }\leftarrow i,\mathrm{\ell }}^{\mathrm{A}}$ for $i\in [1..n-1]$, $\mathrm{\ell }\in [2..n-i+1]$ and $i^{\prime }\in [1..i-\mathrm{\ell }]$ s.t. $T[i^{\prime }..i^{\prime }+\mathrm{\ell })=T[i..i+\mathrm{\ell })$: ${\mathrm{𝑟𝑒𝑓}}_{i^{\prime }\leftarrow i,\mathrm{\ell }}^{\mathrm{A}}=1$ iff $T[i..i+\mathrm{\ell })$ is a type-A factor that refers to $T[i^{\prime }..i^{\prime }+\mathrm{\ell })$.

• $\mathrm{■}$

  ${\mathrm{𝑟𝑒𝑓}}_{i^{\prime }\leftarrow i,\mathrm{\ell }}^{\mathrm{B}}$ for $i\in [1..n-1]$, $\mathrm{\ell }\in [2..n-i+1]$ and $i^{\prime }\in [i-\mathrm{\ell }+1..i-1]$ s.t. $T[i^{\prime }..i^{\prime }+\mathrm{\ell })=T[i..i+\mathrm{\ell })$ and $i-i^{\prime }$ divides $\mathrm{\ell }$: ${\mathrm{𝑟𝑒𝑓}}_{i^{\prime }\leftarrow i,\mathrm{\ell }}^{\mathrm{B}}=1$ iff $T[i..i+\mathrm{\ell })$ is a type-B factor that refers to $T[i^{\prime }..i)$ to repeat it.

• $\mathrm{■}$

  ${\mathrm{𝑟𝑒𝑓}}_{i^{\prime },{\mathrm{\ell }}^{\prime }\leftarrow i,\mathrm{\ell }}^{\mathrm{C}}$ for $i,i^{\prime }\in [1..n-2]$, $\mathrm{\ell }\in [2..n-i+1]$, ${\mathrm{\ell }}^{\prime }\in [2..n-i^{\prime }+1]$ and $[i..i+\mathrm{\ell })\cap [i^{\prime }..i^{\prime }+{\mathrm{\ell }}^{\prime })=\mathrm{\varnothing }$ s.t. $T[i..i+\mathrm{\ell })$ is a substring of $T[i^{\prime }..i^{\prime }+{\mathrm{\ell }}^{\prime })$: ${\mathrm{𝑟𝑒𝑓}}_{i^{\prime },{\mathrm{\ell }}^{\prime }\leftarrow i,\mathrm{\ell }}^{\mathrm{C}}=1$ iff $T[i..i+\mathrm{\ell })$ is a type-C factor that refers to $T[i^{\prime }..i^{\prime }+{\mathrm{\ell }}^{\prime })$ to truncate it.

• $\mathrm{■}$

  ${\mathrm{𝑑𝑟𝑒𝑓}}_{i^{\prime },{\mathrm{\ell }}^{\prime }\leftarrow i}$ for $(i^{\prime },i,\mathrm{\ell })\in ⟦{\mathrm{𝑟𝑒𝑓}}_{\circ \leftarrow \circ ,\circ }^{\mathrm{A}}⟧$ with ${\mathrm{\ell }}^{\prime }=\mathrm{\ell }$, $(i^{\prime },i)\in ⟦{\mathrm{𝑟𝑒𝑓}}_{\circ \leftarrow \circ ,\bullet }^{\mathrm{B}}⟧$ with ${\mathrm{\ell }}^{\prime }=i-i^{\prime }$, or $(i^{\prime },{\mathrm{\ell }}^{\prime },i)\in ⟦{\mathrm{𝑟𝑒𝑓}}_{\circ ,\circ \leftarrow \circ ,\bullet }^{\mathrm{C}}⟧$: ${\mathrm{𝑑𝑟𝑒𝑓}}_{i^{\prime },{\mathrm{\ell }}^{\prime }\leftarrow i}=1$ iff there is an ICS-factor that starts at $i$ and refers to $T[i^{\prime }..i^{\prime }+{\mathrm{\ell }}^{\prime })$.

• $\mathrm{■}$

  $q_{i^{\prime },{\mathrm{\ell }}^{\prime }}$ for $(i^{\prime },{\mathrm{\ell }}^{\prime })\in ⟦{\mathrm{𝑑𝑟𝑒𝑓}}_{\circ ,\circ \leftarrow \bullet }⟧$ or $(i^{\prime },i,\mathrm{\ell })\in ⟦{\mathrm{𝑟𝑒𝑓}}_{\circ \leftarrow \circ ,\circ }^{\mathrm{B}}⟧$ with ${\mathrm{\ell }}^{\prime }=\mathrm{\ell }+i-i^{\prime }$: $q_{i^{\prime },{\mathrm{\ell }}^{\prime }}=1$ iff $[i^{\prime }..i^{\prime }+{\mathrm{\ell }}^{\prime })$ is in the set $I$ defined in Lemma 6.

• $\mathrm{■}$

  ${\mathrm{𝑑𝑒𝑝𝑡ℎ}}_{i,\mathrm{\ell },d}$ for $i\in [1..n]$, $\mathrm{\ell }\in [1..n+1-i]$ and $d\in [0..n]$: ${\mathrm{𝑑𝑒𝑝𝑡ℎ}}_{i,\mathrm{\ell },d}=1$ iff $d$ is less than or equal to the maximum reference depth of characters in $T[i..i+\mathrm{\ell })$.

We next define constraints that the above variables must satisfy.

Since the factors and their starting positions must be consistent, we have:

If $T[i..i+\mathrm{\ell })$ with $\mathrm{\ell }>1$ cannot be a candidate of type-A, type-B nor type-C factor, $f_{i,\mathrm{\ell }}$ must be false, i.e.,

If $T[i..i+\mathrm{\ell })$ is a type-A factor, there exists $i^{\prime }\in {\mathrm{𝑟𝑒𝑓}}_{\circ \leftarrow i,\mathrm{\ell }}^{\mathrm{A}}$ s.t. ${\mathrm{𝑟𝑒𝑓}}_{i^{\prime }\leftarrow i,\mathrm{\ell }}^{\mathrm{A}}$ is true. If $T[i..i+\mathrm{\ell })$ is a type-B factor, there exists $i^{\prime }\in {\mathrm{𝑟𝑒𝑓}}_{\circ \leftarrow i,\mathrm{\ell }}^{\mathrm{B}}$ s.t. ${\mathrm{𝑟𝑒𝑓}}_{i^{\prime }\leftarrow i,\mathrm{\ell }}^{\mathrm{B}}$ is true. If $T[i..i+\mathrm{\ell })$ is a type-C factor, there exists $(i^{\prime },{\mathrm{\ell }}^{\prime })\in {\mathrm{𝑟𝑒𝑓}}_{\circ ,\circ \leftarrow i,\mathrm{\ell }}^{\mathrm{C}}$ s.t. ${\mathrm{𝑟𝑒𝑓}}_{i^{\prime },{\mathrm{\ell }}^{\prime }\leftarrow i,\mathrm{\ell }}^{\mathrm{C}}$ is true. Conversely, if one of the variables of the form ${\mathrm{𝑟𝑒𝑓}}_{i^{\prime }\leftarrow i,\mathrm{\ell }}^{\mathrm{A}}$, ${\mathrm{𝑟𝑒𝑓}}_{i^{\prime }\leftarrow i,\mathrm{\ell }}^{\mathrm{B}}$ or ${\mathrm{𝑟𝑒𝑓}}_{i^{\prime },{\mathrm{\ell }}^{\prime }\leftarrow i,\mathrm{\ell }}^{\mathrm{C}}$ is true, $T[i..i+\mathrm{\ell })$ must be a factor. This can be encoded as

For a fixed substring $T[i..i+\mathrm{\ell })$, at most one variable of the form ${\mathrm{𝑟𝑒𝑓}}_{i^{\prime }\leftarrow i,\mathrm{\ell }}^{\mathrm{A}}$, ${\mathrm{𝑟𝑒𝑓}}_{i^{\prime }\leftarrow i,\mathrm{\ell }}^{\mathrm{B}}$ or ${\mathrm{𝑟𝑒𝑓}}_{i^{\prime },{\mathrm{\ell }}^{\prime }\leftarrow i,\mathrm{\ell }}^{\mathrm{C}}$ is allowed to indicate that $T[i..i+\mathrm{\ell })$ is a factor. Thus, we require

Constraint 4 for a fixed $(i,\mathrm{\ell })$ can be encoded in size of $|⟦{\mathrm{𝑟𝑒𝑓}}_{\circ \leftarrow i,\mathrm{\ell }}^{\mathrm{A}}⟧\cup ⟦{\mathrm{𝑟𝑒𝑓}}_{\circ \leftarrow i,\mathrm{\ell }}^{\mathrm{B}}⟧\cup ⟦{\mathrm{𝑟𝑒𝑓}}_{\circ ,\circ \leftarrow i,\mathrm{\ell }}^{\mathrm{C}}⟧|=O(n^2)$ using an efficient encoding for this kind of “at-most” constraints [15].

If ${\mathrm{𝑑𝑟𝑒𝑓}}_{i^{\prime },{\mathrm{\ell }}^{\prime }\leftarrow i}$ is true, then there is a factor that refers to $T[i^{\prime }..i^{\prime }+{\mathrm{\ell }}^{\prime })$ and vice versa.

We let $q_{i^{\prime },\mathrm{\ell }}$ summarize the information on whether $T[i^{\prime }..i^{\prime }+{\mathrm{\ell }}^{\prime })$ corresponds to a node implied by ${\mathrm{𝑟𝑒𝑓}}_{\bullet \leftarrow \bullet ,\bullet }^{\mathrm{A}}$, ${\mathrm{𝑟𝑒𝑓}}_{\bullet \leftarrow \bullet ,\bullet }^{\mathrm{B}}$ and ${\mathrm{𝑟𝑒𝑓}}_{\bullet ,\bullet \leftarrow \bullet ,\bullet }^{\mathrm{C}}$:

If $q_{i^{\prime },{\mathrm{\ell }}^{\prime }}$ is true, then $i^{\prime }$ must be the starting position of an ICS-factor.

If $q_{i^{\prime },{\mathrm{\ell }}^{\prime }}$ is true, then $T[i^{\prime }..i^{\prime }+{\mathrm{\ell }}^{\prime })$ must not be a type-B factor:

The set of intervals indicated by $q_{\bullet ,\bullet }$ must be compatible with tree structures. In other words, for any two substrings $T[i_1^{\prime }..i_1^{\prime }+{\mathrm{\ell }}_1^{\prime })$ and $T[i_2^{\prime }..i_2^{\prime }+{\mathrm{\ell }}_2^{\prime })$ with , at most one of $T[i_1^{\prime }..i_1^{\prime }+{\mathrm{\ell }}_1^{\prime })$ and $T[i_2^{\prime }..i_2^{\prime }+{\mathrm{\ell }}_2^{\prime })$ can correspond to a node of the grammar tree. Thus, we require that

Since the reference depth of a character is at least 0, ${\mathrm{𝑑𝑒𝑝𝑡ℎ}}_{i,1,0}$ is always true:

If the reference depth of a character is at least $d$, then it is also at least $d-1$:

The reference depths of characters in the same factor are the same:

The reference depth of a substring is the maximum of the reference depths of characters in the substring:

If an ICS-factor starting at $i$ refers to substring $T[i^{\prime }..i^{\prime }+\mathrm{\ell })$, the reference depth of $T[i]$ is larger than the reference depth of $T[i^{\prime }..i^{\prime }+\mathrm{\ell })$, which is encoded as

From the above SAT formulation, we get the following theorem:

We prove the correctness of our SAT formulation presented in this section for ICS-factorizations. On the one hand, given an internal collage system, it is clear that a truth assignment to Boolean variables based on the definition will satisfy all constraints. On the other hand, given $T$ and a truth assignment satisfying the constraints, we can deduce a factorization to satisfy the conditions (i), (ii), (iii) and (iv) of Lemma 6. First, the truth assignments of $p_i$ and Constraint (1) give a factorization of $T$ where we regard $T[i..i+\mathrm{\ell })$ as a factor if and only if $f_{i,\mathrm{\ell }}=1$. If $f_{i,\mathrm{\ell }}=1$ with $\mathrm{\ell }>1$, the type of factor $T[i..i+\mathrm{\ell })$ and its reference to satisfy condition (i) are specified by the truth assignments of ${\mathrm{𝑟𝑒𝑓}}_{\bullet \leftarrow \bullet ,\bullet }^{\mathrm{A}}$, ${\mathrm{𝑟𝑒𝑓}}_{\bullet \leftarrow \bullet ,\bullet }^{\mathrm{B}}$ and ${\mathrm{𝑟𝑒𝑓}}_{\bullet ,\bullet \leftarrow \bullet ,\bullet }^{\mathrm{C}}$, which are suitably controlled by Constraints (2), (3) and (4). By Constraint (5), the information about the starting position of a factor and its reference is collected in variables ${\mathrm{𝑑𝑟𝑒𝑓}}_{\bullet ,\bullet \leftarrow \bullet }$. By Constraint (6), the truth assignments of $q_{\bullet ,\bullet }$ give the set $I$ of intervals of Lemma 6. The starting position of every interval of $I$ must be the starting position of an ICS-factor, which is enforced by Constraint (7). Condition (iii) is fulfilled by Constraint (8). Constraint (9) ensures that $I$ is compatible with tree structures to satisfy condition (ii). Finally, condition (iv) is ensured by Constraints (10), (11), (12), (13) and (14) using ${\mathrm{𝑑𝑟𝑒𝑓}}_{\bullet ,\bullet \leftarrow \bullet }$ and ${\mathrm{𝑑𝑒𝑝𝑡ℎ}}_{\bullet ,\bullet ,\bullet }$.

By Proposition 2, the size $m$ of an internal collage system corresponding to an ICS-factorization is $m=h+m_{\mathrm{𝗍𝗋}}+\sigma -1$, where $h$ is the number of factors, $m_{\mathrm{𝗍𝗋}}$ is the number of truncation rules, and $\sigma$ is the number of distinct characters in $T$. Since $\sigma$ is fixed, $m$ is minimized if $h+m_{\mathrm{𝗍𝗋}}$ is minimized. This can be encoded in MAX-SAT by introducing the set of soft clauses consisting of $\neg p_{\bullet }$ and $\neg {\mathrm{𝑟𝑒𝑓}}_{\bullet ,\bullet \leftarrow \bullet ,\bullet }^{\mathrm{C}}$ because satisfying these soft clauses as many as possible leads to minimizing $h+m_{\mathrm{𝗍𝗋}}$.

In total, we have $O(n^4)$ Boolean variables dominated by ${\mathrm{𝑟𝑒𝑓}}_{\bullet ,\bullet \leftarrow \bullet ,\bullet }^{\mathrm{C}}$. The total size of the resulting MAX-SAT formulation is $O(n^4)$, dominated by Constraints (3), (4), (5), (6), (9), (13) and (14) where there are four free parameters each of which take $O(n)$ different values. $◀$