Verification in staged tile self-assembly

Abstract

We prove the unique assembly and unique shape verification problems, benchmark measures of self-assembly model power, are $\textsf {coNP}^{\textsf {NP}}$-hard and contained in PSPACE (and in $\mathrm {\Pi }^\textsf {P}_{2s}$ for staged systems with s stages). En route, we prove that unique shape verification problem in the 2HAM is $\textsf {coNP}^{\textsf {NP}}$-complete.

1 Introduction

Here we consider the complexity of two standard problems in tile self-assembly: deciding whether a system uniquely assembles a given assembly or shape. These so-called unique assembly and unique shape verification problems are benchmark problems in tile assembly, and have been studied in a variety of models, including the aTAM (Adleman et al. 2002; Bryans et al. 2013), the q-tile model (Cheng et al. 2005), and the 2HAM (Cannon et al. 2013).

The unique assembly and unique shape verification problems ask whether a system behaves as expected: does a given system yield a unique given assembly or assemblies of a given unique shape? The distinct rules by which assemblies form in various tile assembly models yield the potential for such problems to have varying complexity. For instance, assuming $\textsf {P}\ne \textsf {NP}$, the unique assembly verification problem is known to be a strictly easier problem in the aTAM than in the 2HAM.

However, several open questions remain. For instance, such a separation between the aTAM and 2HAM for the unique shape verification problem had not been known. Here we prove such a separation (see Table 1).

Table 1 Known and new results on the unique assembly and unique shape verification problems

Additionally, a popular generalization of the 2HAM called the staged tile assembly model (Demaine et al. 2008) has been shown to be capable of extremely efficient assembly across a range of parameters (Chalk et al. 2016; Demaine et al. 2008, 2011, 2015; Winslow 2015). Does this power come from the increased complexity of verifying that systems assemble intended assemblies and shapes?

We achieve progress on these questions, proving a separation between the 2HAM and staged model for the unique assembly verification problem ($\textsf {coNP}$-complete versus $\textsf {coNP}^{\textsf {NP}}$-hard) utilizing a promising technique that may lead to proving a stronger separation for the unique shape verification problem ($\textsf {coNP}^{\textsf {NP}}$-complete versus a conjectured PSPACE-complete).

The $\textsf {coNP}^{\textsf {NP}}$-hardness results are also interesting as the first, to our knowledge, verification problems in irreversible tile assembly that are decidable but not contained in NP or coNP.

2 The staged assembly model

Tiles A tile is a non-rotatable unit square with each edge labeled with a glue from a set $\Sigma$. Each pair of glues $g_1, g_2 \in \Sigma$ has a non-negative integer strength, denoted $\mathrm{str}(g_1, g_2)$. Every set $\Sigma$ contains a special null glue whose strength with every other glue is 0.

Configurations, assemblies, and shapes A configuration is a partial function $A : \mathbb {Z}^2 \rightarrow T$ for some set of tiles T, i.e., an arrangement of tiles on a square grid. For a configuration A and vector $\mathbf {u} = \langle u_x, u_y \rangle \in \mathbb {Z}^2$, $A + \mathbf {u}$ denotes the configuration $A \circ f$, where $f(x, y) = (x + u_x, y + u_y)$. For two configurations A and B, B is a translation of A, written $B \simeq A$, provided that $B = A + \mathbf {u}$ for some vector $\mathbf {u}$. For a configuration A, the assembly of A is the set $\tilde{A} = \{ B : B \simeq A \}$. An assembly $\tilde{A}$ is a subassembly of an assembly $\tilde{B}$, denoted $\tilde{A} \sqsubseteq \tilde{B}$, provided that there exists an $A\in \tilde{A}$ and $B\in \tilde{B}$ such that $A \subseteq B$.

Bond graphs and stability For a configuration A, define the bond graph$G_A$ to be the weighted grid graph in which each element of $\mathrm{dom}(A)$ is a vertex, and the weight of the edge between a pair of tiles is equal to the strength of the coincident glue pair. A configuration is $\tau$-stable for $\tau \in \mathbb {N}$ if every edge cut of $G_A$ has strength at least $\tau$, and is $\tau$-unstable otherwise. Similarly, an assembly is $\tau$-stable provided the configurations it contains are $\tau$-stable. Assemblies $\tilde{A}$ and $\tilde{B}$ are $\tau$-combinable into an assembly $\tilde{C}$ provided there exist $A \in \tilde{A}$, $B \in \tilde{B}$, and $C \in \tilde{C}$ such that $A \bigcup B = C$, $\mathrm{dom(A)} \bigcap \mathrm{dom(B)} = \emptyset$, and $\tilde{C}$ is $\tau$-stable.

Two-handed assembly and bins We define the assembly process via bins. A bin is an ordered tuple $(S,\tau )$ where S is a set of initial assemblies and $\tau \in \mathbb {N}$ is the temperature. In this work, $\tau$ is always equal to 2 for upper bounds, and at most some constant for lower bounds. For a bin $(S, \tau )$, the set of produced assemblies $P'_{(S,\tau )}$ is defined recursively as follows:

• 1. $S \subseteq P'_{(S,\tau )}$.

• 2. If $A,B \in P'_{(S,\tau )}$ are $\tau$-combinable into C, then $C \in P'_{(S,\tau )}$.

A produced assembly is terminal provided it is not $\tau$-combinable with any other producible assembly, and the set of all terminal assemblies of a bin $(S,\tau )$ is denoted $P_{(S,\tau )}$. That is, $P'_{(S,\tau )}$ represents the set of all possible assemblies that can assemble from the initial set S, whereas $P_{(S,\tau )}$ represents only the set of assemblies that cannot grow any further.

The assemblies in $P_{(S,\tau )}$ are uniquely produced iff for each $x \in P'_{(S, \tau )}$ there exists a corresponding $y \in P_{(S,\tau )}$ such that $x \sqsubseteq y$. Unique production implies that every producible assembly can be repeatedly combined with others to form an assembly in $P_{(S,\tau )}$.

Staged assembly systems An r-stageb-bin mix graphM is an acyclic r-partite digraph consisting of rb vertices $m_{i,j}$ for $1 \le i \le r$ and $1\le j \le b$, and edges of the form $(m_{i,j}, m_{i+1,j'})$ for some $i, j, j'$. A staged assembly system is a 3-tuple $\langle M_{r,b}, \{T_1, T_2, \ldots , T_b\}, \tau \rangle$ where $M_{r,b}$ is an r-stage b-bin mix graph, $T_i$ is a set of tile types, and $\tau \in \mathbb {N}$ is the temperature. Given a staged assembly system, for each $1\le i \le r$, $1\le j \le b$, a corresponding bin $(R_{i,j}, \tau )$ is defined as follows:

• 1. $R_{1,j}= T_j$ (this is a bin in the first stage);

• 2. For $i\ge 2$, $\displaystyle R_{i,j}= \left (\bigcup _{k:\ (m_{i-1,k},m_{i,j})\in M_{r,b}} P_{(R_{(i-1,k)},\tau )}\right )$.

Thus, bins in stage 1 are tile sets $T_j$, and each bin in any subsequent stage receives an initial set of assemblies consisting of the terminally produced assemblies from a subset of the bins in the previous stage as dictated by the edges of the mix graph.¹ The output of a staged system is the union of the set of terminal assemblies of the bins in the final stage.² The output of a staged system is uniquely produced provided each bin in the staged system uniquely produces its terminal assemblies.

Shapes The shape of an assembly $\tilde{A}$ is $\{ \mathrm{dom}(A) : A \in \tilde{A}\}$ where $\mathrm{dom}$ is the domain of a configuration. A shape $S'$ is a scaled version of shape S provided that for some $k \in \mathbb {N}$ and $D \in S$, $\bigcup _{(x, y) \in D} \bigcup _{(i, j) \in \{0, 1, \ldots , k-1\}^2} (kx + i, ky + j) \in S'$.

3 The 2HAM unique shape verification problem is $\textsf {coNP}^{\textsf {NP}}$-complete

This section serves as a warm-up for the format and techniques used in later sections. We begin by proving the 2HAM USV problem is in $\textsf {coNP}^{\textsf {NP}}$ by providing a (non-deterministic) algorithm for the problem that can be executed on such a machine. This is followed by a reduction from a $\mathsf {SAT}$-like problem complete for $\textsf {coNP}^{\textsf {NP}}$ ($\forall \exists \mathrm {SAT}$).

Definition 1

(2HAM unique shape verification (2HAM USV) problem) Given a 2HAM system $\varGamma$ and shape S, does every terminal assembly of $\varGamma$ have shape S?

Theorem 1

The 2HAM USV problem (for$\tau =2$systems) is$\textsf {coNP}^{\textsf {NP}}$-hard.

Definition 2

($\forall \exists \mathrm {SAT}$) Given a 3-$\mathsf {SAT}$ formula

$\phi (x_1, x_2, \ldots , x_k, x_{k+1}, \ldots , x_n)$, is it true that for every assignment of $x_1, x_2, \ldots , x_k$, there exists an assignment of $x_{k+1}, x_{k+2}, \ldots , x_n$ such that $\phi (x_1, x_2, \ldots , x_n)$ is satisfied?

The $\forall \exists \mathrm {SAT}$ problem was shown to be $\textsf {coNP}^{\textsf {NP}}$-complete by Stockmeyer (1976) [see Schaefer and Umans (2002) for further discussion].

Proof

The reduction is from $\forall \exists \mathrm {SAT}$; the reduction will yield a 2HAM system with multiple terminal assemblies if and only if the $\forall \exists \mathrm {SAT}$ instance has an assignment of $x_1,\ldots ,x_k$ with no satisfying assignment of $x_{k+1},\ldots ,x_n$. Roughly speaking, the system output by the reduction behaves as follows. First, a distinct assembly encoding each possible assignment of the variables of the $\forall \exists \mathrm {SAT}$ instance is assembled. Further growth “tags” each assembly as either a true or false assembly, based upon the truth value of the input 3-$\mathsf {SAT}$ formula $\phi$ for the variable assignment encoded by the assembly.

False assemblies further grow into a slightly larger target shape S. A separate set of test assemblies are created, one for each variable assignment of the variables $x_1, \ldots x_k$. Each test assembly attaches to any true assembly with the same assignment of these variables to form an assembly with shape S—the same shape as false assemblies.

Terminal assemblies then consist of false assemblies (corresponding to non-satisfying assignments), true test assemblies with shape S (corresponding to satisfying assignments with specific assignments of $x_1,\ldots ,x_k$), and possibly test assemblies (corresponding to specific assignments of $x_1,\ldots ,x_k$ with no satisfying assignment of $x_{k+1},\ldots ,x_n$). So there is a terminal test assembly if and only if there is some assignment of $x_1,\ldots ,x_k$ with no satisfying assignment of $x_{k+1},\ldots ,x_n$, i.e. the solution to the $\forall \exists \mathrm {SAT}$ instance is false.

Fig. 1

Steps of the 2HAM USV $\textsf {coNP}^{\textsf {NP}}$-hardness reduction. a Assemblies encoding all possible variable assignments are assembled. b Test assemblies encoding all possible assignments of $x_1,\ldots ,x_k$ are assembled. c Non-satisfying variable assignments grow into reject assemblies that forbid attachment of test assemblies. d Satisfying variable assignments grow into accept assemblies permitting attachment of the test assembly corresponding to the specific assignment of $x_1,\ldots ,x_k$. The terminal shape S of the system is seen in (c) and (d). If the solution to the $\forall \exists \mathrm {SAT}$ instance is false, one or more test assemblies (with shape other than S) will also be terminal

SATassemblies Consider a given input formula C and input value k for the $\forall \exists \mathrm {SAT}$ problem. From this input we design a corresponding 2HAM system $\varGamma = (T,2)$ and shape S such that the terminal assemblies of $\varGamma$ share a common shape S if and only if the $\forall \exists \mathrm {SAT}$ instance is “true”, i.e. each assignment of the variables $x_1,\ldots ,x_k$ can be combined with some assignment of the variables $x_{k+1},\ldots ,x_m$ such that the 3-$\mathsf {SAT}$ instance is satisfied.

The system has temperature 2, and the tile set T of the system output by the reduction is sketched in Fig. 1. The first subset of tiles is a minor modification of the commonly used 3-$\mathsf {SAT}$ solving system from Lagoudakis and Labean (1999).

For each variable $x_i$, the system has two tile subsets. These collections assemble into $1\times 4$ assemblies with exposed north and south glues representing the values “0” and “1”, respectively, encoding the assignment of a specific variable to true or false. These $1 \times 4$ assemblies further assemble into $1 \times 4n$ assemblies encoding complete assignments of the variables $x_1,\ldots ,x_n$. The non-deterministic assembly process of 2HAM implies that such an assembly for every possible variable assignment will be assembled.

An additional column is attached to this bar of height equal to m, the number of clauses in the formula C (Fig. 1). An additional set of tiles are added that evaluate the 3-$\mathsf {SAT}$ formula $\phi$ based upon the variable assignments encoded by the initial $1 \times 4n$ assembly following the approach of Lagoudakis and Labean (1999). These tiles place a tile in the upper right corner of the resulting assembly with exposed glue labeled “T” or “F”, indicating the truth value of $\phi$ based upon the variable assignments.

The resulting assemblies are categorized as true and false assemblies. Additional tiles are added so that every false assembly further grows, extending the left 4k columns (corresponding to the variables $x_1$ to $x_k$) southward by 3 rows, and the remaining right $4(n-k)$ columns southward by 1 row (Fig. 1c). The resulting shape is the shape S output by the reduction, i.e. the only shape assembled by the system if the solution to the $\forall \exists \mathrm {SAT}$ instance is “true”.

Test assemblies Additional tiles are also added so that true assemblies also grow southward, but extending the left 4k columns by various amounts based upon each variable assignment. The result is a sequence of geometric “bumps and dents” that encode the truth values of these variables.

A set of test assemblies with complementary geometry for each possible assignment of variables $x_1$ through $x_k$ are assembled (Fig. 1b). Test assemblies use two strength-1 glues that cooperatively attach to any true assembly with a matching assignment of variables $x_1$ through $x_k$ (Fig. 1d). The assembly formed by a test assembly attaching to a true assembly has shape S: the same shape as a false assembly.

Terminal assemblies If the solution to the $\forall \exists \mathrm {SAT}$ instance is “false”, there is some truth assignment for variables $x_1 \ldots x_k$ with no corresponding assignment of the variables $x_{k+1} \ldots x_n$ such that $\phi (x_1, \ldots , x_n)$ is “true”. Thus, the test assembly with this assignment of variables $x_1, \ldots , x_k$ has no compatible true assembly to attach to, and this test assembly is a terminal assembly of $\varGamma$ with shape not equal to S.

On the other hand, if the solution to the $\forall \exists \mathrm {SAT}$ instance is “true”, every test assembly attaches to a true assembly and thus every terminal assembly (true-test assemblies and false assemblies) has shape S. $\square$

Theorem 2

The 2HAM USV problem is in$\textsf {coNP}^{\textsf {NP}}$.

Proof

The solution to an instance $(\varGamma , S)$ of the 2HAM USV problem is “true” if and only if:

• 1. Every producible assembly of $\varGamma$ has size at most |S|.

• 2. Every assembly of size at most |S| and without shape S is not a terminal assembly.

Algorithm 1 solves the 2HAM USV problem by verifying each of these conditions, using an NP subroutine to verify the second condition. The algorithm is executed by a coNP machine, implying that “false” is returned if any of the non-deterministic branches return “false”, and otherwise returns “true”.$\square$

4 Staged unique assembly verification is $\textsf {coNP}$-hard

Definition 3

(Staged unique assembly verification (Staged UAV) problem) Given a staged system $\varGamma$ and an assembly A, does $\varGamma$ uniquely assemble A?

Theorem 3

The staged UAV problem (for 4-stage systems at$\tau =2$) iscoNP-hard.

Proof

The reduction is from 3-$\mathsf {SAT}$, outputting a staged system $\varGamma$ and assembly A such that the 3-$\mathsf {SAT}$ instance is satisfiable if and only if A is not the unique terminal assembly of $\varGamma$. We reduce from 3-SAT: Given a 3-SAT formula $\phi$, we design a staged assembly system and an assembly A such that $\phi$ is not satisfied if and only if A is uniquely assembled by $\varGamma$.

Fig. 2

a The tile set used in the staged coNP-hardness reduction. b The subsets of tiles included in separated initial bins within the first stage of the system

The tileset The tiles used in our construction are shown in Fig. 2a. In particular, for each variable $x_i \in \{x_1, x_2, \ldots , x_n\}$ and clause $c_j \in \{c_1, c_2, \ldots , c_m\}$ in $\phi$, there is a block of tiles labeled $a_{i,j},b_{i,j},c_{i,j},d_{i,j},e_{i,j},f_{i,j},g_{i,j}$. The set of tile types for each block is denoted $\mathrm {block}_{i, j}$.

The strength-2 ($\tau =2$) glues connecting adjacent tiles are unique with respect to adjacent tiles, and are unlabelled in the figures for clarity. Note that for each block (i, j), the top four tiles of the block occupy the same locations as the bottom four tiles of block $(i,j+1)$. Finally, the tileset includes a length 4m chain of green tiles, with each green tile sharing a strength-2 glue with its neighbors, along with four light-grey tiles which together attach to the green assembly.

Stage 1: variable assignments The specific formula $\phi$ is encoded within the output staged system via the initial choice of tiles placed into a O(1)-sized collection of stage-1 bins. For each variable $x_i$ and clause $c_j$ combination, we select two subsets of the $\mathrm {block}_{i,j}$ tileset. The first subset encodes a variable choice of “false” for $x_i$. The tile sets in Fig. 2b(i) and (iv) are used if $x_i$ satisfies (and $\overline{x_i}$ does not satisfy) clause $c_j$, respectively. Similarly, the tile sets in Fig. 2b(ii–iii) are used if $x_i$ does not (and $\overline{x_i}$ does satisfy) clause $c_j$.

Beyond utilizing two types of $\mathrm {block}_{i,j}$ tile sets, tile sets are further distinguished between odd and even values of i and j. In total, 16 distinct bins (satisfied or not, negated or not, odd or even i, odd or even j) are used.

We include the grey and green tiles of Fig. 2(a) separately in two additional bins. An additional four bins are used in the construction to maintain a set of single copies of all tiles used within the system. Separating these tile subsets into four bins ensures that the tiles do no interact (until mixed with other assemblies at a later stage).

Stage 2: assembling rows In stage 2 we combine all $\mathrm {block}_{i,j}$ assemblies for even j into one bin, and all $\mathrm {block}_{i,j}$ assemblies for odd j into a second bin. Within each bin and for each value j, rows encoding each possible variable assignment assemble non-determistically via attaching $0-\mathrm {block}_{i,j}$ and $1-\mathrm {block}_{i,j}$ assemblies for each $i \in \{1, 2, \ldots , n\}$. We refer to these assemblies as $\mathrm {row}_j$ assemblies. There are $2^n$ such assemblies for each j-one per variable assignment. Example $\mathrm {row}_j$ assemblies are shown in Fig. 3.

Fig. 3

In stage 2, rows non-deterministically form encoding each of the $2^n$ possible variable assignments. In stage 3 the rows are combined allowing for geometrically compatible, sequential rows with exposed red glue to attach. a Combinable rows. b Geometrically incompatible rows. c Rows with no glues for attachment. (Color figure online)

Stage 3: combining rows with shared assignments and satisfied clauses Stage 3 is where the real action happens. All $\mathrm {row}_j$ assemblies are combined, along with the green and grey assemblies of Fig. 2.

Consider the possible assembly of a $\mathrm {row}_j$ and a $\mathrm {row}_{j+1}$ assembly. If the two respective rows encode distinct variable assignments, geometric incompatibility prohibits any possible connection (Fig. 3b). If the rows encode the same truth assignment, then the rows may attach if any of the $\mathrm {row}_{j}$ variable pieces expose the extended tip via the red $\tau =2$ strength glues (Fig. 3a). Such an attachment indicates that the variable assignment of both rows satisfies $c_j$. If the variable assignment encoding does not satisfy $c_j$, no extended tip exists and the rows cannot attach (Fig. 3c).

Fig. 4

a Non-satisfying variable assignments will not be able to grow from row 0 to row m. b Assemblies encoding satisfying variable assignments will allow for complete assemblies with all rows, allowing for a green assembly to attach. c The target assembly A given as output of the reduction. (Color figure online)

A satisfying assignment of $\phi$ corresponds to m rows attaching to form a complete “satisfying” assembly (Fig. 4b). The green assembly attaches cooperatively to such assemblies using the $\mathrm {row}_m$ assembly glue and a glue from the grey tiles, which attach uniquely to $\mathrm {row}_0$. The attachment of a green assembly verifies that all rows are present and the variable assignment satisfies $\phi$.

A second copy of the green assembly attaches to any assembly containing $\mathrm {row}_0$, regardless of whether all rows are present or not (Fig. 4a). In a separate bin, the green assembly tiles and grey assemblies are combined, yielding a combined grey-green product (for mixing in stage 4).

Stage 4: merging assignments In stage 4, the set of all $\mathrm {block}_{i,j}$ individual tiles are added to the assemblies constructed in stage 3 as well as the the grey-green assembly produced in the previous stage. Note that the green assembly is not an input assembly to this mixing.

Since all $\mathrm {block}_{i,j}$ assemblies are included, each terminal assembly from stage 3 may grow into the unique terminal assembly shown in Fig. 4c with one exception: assemblies from stage 3 encoding satisfying variable assignments. These assemblies have one additional copy of the green bar assembly attached. Therefore, the assembly of Fig. 4c is uniquely assembled if an only if no such satisfying assembly exists. $\square$

5 Staged unique assembly verification is $\textsf {coNP}^{\textsf {NP}}$-hard

Theorem 4

The staged UAV problem (for$\tau =2$7-stage systems) is$\textsf {coNP}^{\textsf {NP}}$-hard.

Proof

We reduce from $\forall \exists \mathrm {SAT}$ by combining ideas from the reductions of Theorems 1 and 3.

Stages 1–3: theSATassemblies The first 3 stages follows those of the reduction in Theorem 3 but without the inclusion of the green assembly and light grey tiles. The result is a collection of assemblies encoding satisfying variable assignments with all m rows, as well as partial assemblies of less than m rows encoding non-satisfying assignments. For clarity, the bottom half of the $j=0$ blocks for values $i>k$ are removed, exposing the “geometric teeth” only for the first k variables.

Stages 1–3: the test assemblies Additionally, in a separate set of bins, we non-deterministically generate a set of test assemblies. The test assemblies are similar to row assemblies and generated in a similar fashion. An example test assembly is shown in Fig. 5 (Stages 1–4). A test assembly for each of the $2^k$ possible truth assignments of $x_1, x_2, \ldots , x_k$ is grown, and a green bar assembly is attached to the side of each test assembly.

Stage 4: the magic happens The $\mathsf {SAT}$ assemblies and test assemblies are combined in a bin. Test assemblies attach to $\mathsf {SAT}$ assesmblies encoding satisfying variable assignments by utilizing cooperative bonding based on the two strength-1 green glues on the green assembly. $\mathsf {SAT}$assemblies encoding non-satisfying assignments must each lack the topmost or bottommost row, and therefore cannot attach to a test assembly.

Fig. 5

The assemblies at respective stages for the $\textsf {coNP}^{\textsf {NP}}$-hardness reduction for the staged UAV problem

Due to the geometric interlocking teeth from the test assembly and the bottom of $\mathsf {SAT}$ assemblies, test assemblies may only attach to $\mathsf {SAT}$ assemblies that encode the same variable assignment (of variables $x_1, x_2,$$\ldots ,$$x_k$). Stages 1–4 of Fig. 5 show an example test assembly and a attaching $\mathsf {SAT}$ assembly.

Note that if there exists a truth assignment for $x_1, x_2,$$\ldots$$, x_k$ with no satisfying assignment of the remaining variables $x_{k+1}, x_{k+2},$$\ldots$$, x_n$, then the corresponding test assembly does not attach to any$\mathsf {SAT}$ assembly and is a terminal assembly of this bin. On the other had, if every assignment of the variables $x_1, x_2,$$\ldots$$, x_k$ has at least one satisfying assignment of the remaining variables, i.e. the solution $\forall \exists \mathrm {SAT}$ instance is “true”, then there are no terminal test assemblies of this bin

Stage 5: tagging non-satisfying assignments In Stage 5, we add preassembled duples which attach to the bottom of any assembly containing row 0 and encodes a non-satisfying variable assignment. This attachment ensures that in subsequent stages, these assemblies will be geometrically incompatible with any remaining test assemblies from Stage 4.

It is possible that some duples have no non-satisfying $\mathsf {SAT}$ assembly to attach to. As a solution, an additional height-1 assembly of the row-0 assembly that “absorbs” each duple is added at this stage. The subsequent stages enable these, as well as all other $\mathsf {SAT}$ assemblies, to grow into a single common (potentially) unique assembly.

Stage 6: attaching test assemblies The result of Stage 5 is mixed with an assembly consisting of:

• The light-grey bar of the test assemblies.

• A second complete layer of dark grey tiles.

• The green bar.

This assembly attaches to any non-satisfying $\mathsf {SAT}$ assembly that includes row 0, ensuring that all assemblies containing row 0 now have a version of the test assembly attached (Stage 6 in Fig. 5).

Stage 7: merging In the final stage, every individual tile of the target assembly (seen in Stage 7 of Fig. 5) is added to the result of Stage 6, with the exception of the green tiles and the tiles in rows 1 through 5 of the $\mathsf {SAT}$ assemblies.

These tiles complete each $\mathsf {SAT}$ assembly in the assembly in Fig. 5 (Stage 7). Morever, the height-1 assembly used to absorb duples from Stage 5 grows into the assembly from Fig. 5 (Stage 7). However, because of the lack of tiles from rows 1 through 5, any leftover test assembly from Stage 4 remains terminal.

Thus the target assembly is the unique terminal assembly of the system if and only if the solution to the $\forall \exists \mathrm {SAT}$ instance is “yes”. $\square$

Observe that every staged system output by the reduction has the property that if it does not have a unique terminal assembly, then it also does not have a unique terminal shape. Thus the same reduction suffices to prove that the staged USV problem is $\textsf {coNP}^{\textsf {NP}}$-hard.

Corollary 1

The staged USV problem is$\textsf {coNP}^{\textsf {NP}}$-hard.

6 Staged PSPACE containment

Here we prove that the staged UAV and USV problems are in PSPACE. Parameterized versions of the results are also obtained; these prove that both problems restricted to systems with any fixed number of stages lie in the polynomial hierarchy. Both results are obtained via upper bounds on the complexities of the following three problems:

Definition 4

(Stage-s producible-in-bin verification (PIBV$_{s}$) problem) Given a staged system $\varGamma$, a bin b in stage s of $\varGamma$, an assembly A, and an integer n:

• 1. is A a producible assembly of b?

• 2. and does every producible assembly of every bin in stage $s-1$ of $\varGamma$ have size at most n?

Definition 5

(Stage-s undersized-in-bin verification (UIBV$_{s}$) problem) Given a staged system $\varGamma$, a bin b in stage s of $\varGamma$, and an integer n:

• 1. does every producible assembly of b have size at most n?

• 2. and does every producible assembly of every bin in stage $s-1$ of $\varGamma$ have size at most n?

Definition 6

(Stage-s terminal-in-bin verification (TIBV$_{s}$) problem) Given a staged system $\varGamma$, a bin b in stage s of $\varGamma$, an assembly A, and an integer n:

• 1. is A a terminal assembly of b?

• 2. and does every producible assembly of b have size at most n?

• 3. and does every producible assembly of every bin in stage $s-1$ of $\varGamma$ have size at most n?

The statements and proofs of the following results use terminology related to the polynomial hierarchy. For an introduction to the polynomial hierarchy, see Stockmeyer (1976). As a reminder, $\mathrm {\Sigma }^\textsf {P}_{i+1} = \textsf {NP}^{\mathrm {\Sigma }^{\textsf {P}}_i}$, $\mathrm {\Pi }^\textsf {P}_{i+1} = \textsf {coNP}^{\mathrm {\Sigma }^{\textsf {P}}_i}$, and $\mathrm {\Sigma }^\textsf {P}_0 = \mathrm {\Pi }^\textsf {P}_0 = \textsf {P}$.

Lemma 1

For all$s \in \mathbb {N}$:

• The PIBV$_{s}$ problem is in$\mathrm {\Sigma }^\textsf {P}_{2s-2}$.

• The UIBV$_{s}$ and TIBV$_{s}$ problems are in$\mathrm {\Pi }^\textsf {P}_{2s-1}$.

Proof

The proof is by induction on s. We begin by proving that PIBV$_{1}$$\in \mathrm {\Sigma }^\textsf {P}_{2s-2} = \textsf {P}$ and UIBV$_{1}$, TIBV$_{1}$$\in \mathrm {\Pi }^\textsf {P}_{2s-1} = \textsf {coNP}$ (the base case). Then we provide recursive algorithms of the correct complexity for PIBV$_{s}$, UIBV$_{s}$, and TIBV$_{s}$, assuming that such algorithms exist for PIBV$_{s-1}$, UIBV$_{s-1}$, and TIBV$_{s-1}$ (the inductive step).

Algorithms for the PIBV$_{1}$, UIBV$_{1}$, and TIBV$_{1}$problems All three problems contain, as a subproblem, “does every producible assembly of every bin in stage $s-1$ of $\varGamma$ have size at most n?”. The answer to this is trivially yes—so only the complexity of the other subproblems needs consideration.

Theorem 3.2 of Doty (2014) states that there exists a polynomial-time algorithm for PIBV$_{1}$. The UIBV$_{1}$ problem can be solved by a coNP machine via non-deterministically selecting an assembly of size in (n, 2n] consisting of tile types input into bin b and returning “no” if the assembly is producible (the machine returns “no” if any non-deterministic branch returns “no”). The TIBV$_{1}$ problem can be solved by a coNP machine by (1) returning “no” if A is not producible, (2) returning “no” if a second assembly (non-deterministically selected) is producible and attaches to A, (3) returning “yes” otherwise.

An algorithm for the PIBV$_{s}$problem We now assume from now on that there exist algorithms $\mathcal {P}_{s-1}$, $\mathcal {U}_{s-1}$, and $\mathcal {T}_{s-1}$ for the PIBV$_{s-1}$, UIBV$_{s-1}$, and TIBV$_{s-1}$ problems in $\mathrm {\Sigma }^\textsf {P}_{2s-4}$, $\mathrm {\Pi }^\textsf {P}_{2s-3}$, and $\mathrm {\Pi }^\textsf {P}_{2s-3}$, respectively, by the inductive hypothesis.

The algorithm runs as an NP machine (making calls to other machines). Lines 5–9 non-deterministically compute an assembly process for A in bin b. Line 10 non-deterministically assigns the initial assemblies of this process to input bins, and lines 11–15 check that the input assemblies are indeed terminal assemblies of these assigned bins. Lines 16–20 check that the condition of subproblem 2 is satisfied.

The complexity of the algorithm is NP with polynomially many calls to algorithms in $\mathrm {\Pi }^\textsf {P}_{2s-3}$. That is, $\textsf {NP}^{\mathrm {\Pi }^\textsf {P}_{2s-3}} = \textsf {NP}^{\mathrm {\Sigma }^\textsf {P}_{2s-3}} = \mathrm {\Sigma }^\textsf {P}_{2s-2}$.

An algorithm for the UIBV$_{s}$problem Since we have already proved that there exists a $\mathrm {\Sigma }^\textsf {P}_{2s-2}$ algorithm $\mathcal {P}_s$, we assume this as well.

The algorithm runs as a coNP machine, returning “no” unless every non-deterministic branch returns “yes”. Lines 2–5 solve subproblem 1, while lines 6–10 address subproblem 2.

The complexity of the algorithm is then coNP with two calls to algorithms in $\mathrm {\Sigma }^\textsf {P}_{2s-2}$. That is, $\textsf {coNP}^{\mathrm {\Sigma }^\textsf {P}_{2s-2}} = \mathrm {\Pi }^\textsf {P}_{2s-1}$.

An algorithm for the TIBV$_{s}$problem Since we have already proved that there exists a $\mathrm {\Pi }^\textsf {P}_{2s-1}$ algorithm $\mathcal {U}_s$, we assume this as well.

The algorithm runs as a coNP machine, returning “no” unless every non-deterministic branch returns “yes”. Lines 2–8 verify that A is a terminal assembly of bin b (subproblem 1): A is not a terminal assembly if and only if (1) A is not producible (lines 2–4), or (2) another producible assembly B can attach to A (lines 5–8).

The complexity of the algorithm needs a slightly careful analysis. Lines 2–8 can be seen as a coNP algorithm with two calls to algorithms in $\mathrm {\Sigma }^\textsf {P}_{2s-2}$, i.e. a $\textsf {coNP}^{\mathrm {\Sigma }^\textsf {P}_{2s-2}} = \mathrm {\Pi }^\textsf {P}_{2s-1}$ algorithm. Then the entire algorithm is a P algorithm with a call to a $\mathrm {\Pi }^\textsf {P}_{2s-1}$ algorithm (lines 2–8) and another call to a $\mathrm {\Pi }^\textsf {P}_{2s-1}$ algorithm (line 9). That is, a $\textsf {P}^{\mathrm {\Pi }^\textsf {P}_{2s-1}} = \mathrm {\Pi }^\textsf {P}_{2s-1}$ algorithm.

A remark on the reoccurring subproblem All three problems have the subproblem “does every producible assembly of every bin in stage $s-1$ of $\varGamma$ have size at most n?” Removing this subproblem from the TIBV$_{s}$ problem makes the problem undecidable, since arbitrarily large assemblies (carrying out unbounded computation) may attach to A. Seen from another perspective, line 5 of $\mathcal {T}_s$ is only correct because we may assume that any attaching assembly B has size at most n. The PIBV$_{s}$ and UIBV$_{s}$ problems are also similarly undecidable when the subproblem is removed.

In a system with a unique terminal assembly/shape, no producible assembly of any bin has size exceeding that of the unique terminal assembly/shape. Thus adding such a subproblem does not change the answer to staged UAV/USV problem instances (a “no” with the added subproblem implies a “no” without it as well). $\square$

With this algorithmic machinery in place, we move to the first main result:

Definition 7

(Stage-s unique assembly verification (Stage-s UAV) problem) Given a staged system $\varGamma$ with s stages and an assembly A, is A the unique terminal assembly of $\varGamma$?

Theorem 5

The stage-s UAV problem is in$\mathrm {\Pi }^\textsf {P}_{2s}$.

Proof

We give an algorithm for the stage-s UAV problem. The stage-s UAV problem may be restated as:

• 1. is every assembly B with $|B| \le |A|$ and $B \ne A$ not a terminal assembly of any bin in stage s?

• 2. and does every producible assembly of every bin in stage $s-1$ of $\varGamma$ have size at most |A|?

The algorithm runs as a coNP machine, returning “no” unless every non-deterministic branch returns “yes”. Lines 2–7 solve subproblem 1, while lines 8–10 solve subproblem 2. $\square$

Every staged system has some number of stages $s \in \mathbb {N}$, but there is no limit to the number of stages a staged system may have. Thus the staged UAV problem is not contained in any level of PH, but every instance can be solved by an algorithm that runs at a fixed level ($\mathrm {\Pi }^\textsf {P}_{2s}$) of the hierarchy. Since it is well-known that $\textsf {PH}{} \subseteq \textsf {PSPACE}{}$, this gives the desired result:

Corollary 2

The staged UAV problem is inPSPACE.

Next, we move to shape verification:

Definition 8

(Stage-s unique shape verification (Stage-s USV) problem) Given a staged system $\varGamma$ with s stages and a shape S, is S the unique terminal shape of $\varGamma$?

Theorem 6

The stage-s USV problem is in$\mathrm {\Pi }^\textsf {P}_{2s}$.

Proof

The stage-s USV problem can be restated as:

• 1. is every assembly B with $|B| \le |S|$ and shape not equal to S not a terminal assembly of any bin in stage s?

• 2. and does every producible assembly of every bin in stage $s-1$ of $\varGamma$ have size at most |S|?

Notice that the subproblems only differ from those of the stage-s UAV problem in that S replaces A and “equal shape” replaces “equals”. Thus the algorithm differs from the $\mathrm {\Pi }^\textsf {P}_{2s}$ algorithm for the stage-s UAV problem on only line 5 (replace “$A \ne B$” with “shape not equal to S”) and line 8 (replace |A| with |S|). $\square$

As for the UAV problem, since the stage-s USV problem is in PH for each $s \in \mathbb {N}$, the USV problem is in PSPACE.

Corollary 3

The staged USV problem is inPSPACE.

7 Open problems

The most direct problem left open by this work is closing the gap in the bottom row of Table 1 between the $\textsf {coNP}^{\textsf {NP}}$-hardness and PSPACE containment of the staged UAV and USV problems. We believe that the approach of differentiating between satisfying and non-satisying assignments, then checking for the existence of various partial assignments (the $\forall$ portion of $\forall \exists \mathrm {SAT}$) can be generalized to achieve hardness for any number of quantifier alternations, using a number of stages proportional to the number of alternations:

Conjecture 1

The staged UAV and USV problems arePSPACE-complete.

Conjecture 2

The stage-s UAV and stage-s USV problems are$\mathrm {\Pi }^p_{\Omega (s)}$-hard.

The UAV and USV problems considered in this work are two variants of the generic challenge of verification; considering the same problems limited to temperature-1 systems or with different inputs is also interesting:

Problem 1

What are the complexities of the staged UAV and USV problems restricted to temperature-1 systems?

Problem 2

What is the complexity (in any model) of the following UAV-like problem: given a system $\varGamma$ and an integer n, does $\varGamma$ have a unique terminal assembly of size at most n?

Finally, the results and techniques presented here might find use in the study of other problems in staged and two-handed self-assembly, such as tile minimization. The aTAM USV problem is coNP-complete, while the minimum tile set problem of finding the minimum number of tiles that uniquely assemble into a given shape is $\textsf {NP}^{\textsf {NP}}$-complete (Bryans et al. 2013). We now know that the 2HAM USV problem is $\textsf {coNP}^{\textsf {NP}}$-complete (Sect. 3); does the corresponding optimization problem also rise in the hierarchy?

Conjecture 3

The 2HAM minimum tile set problem is$\textsf {NP}^{\textsf {NP}^{\textsf {NP}}}$-complete.