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 ${\mathsf {coNP}}^{{\mathsf {NP}}}$-hard and contained in $\mathsf {PSPACE}$ (and in $\mathrm {\Pi }^p_{2s}$ for staged systems with s stages). En route, we prove that unique shape verification problem in the 2HAM is ${\mathsf {coNP}}^{{\mathsf {NP}}}$-complete.

This research was supported in part by National Science Foundation Grants CCF-1117672 and CCF-1555626.

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 [1, 2], the q-tile model [6], and the 2HAM [3].

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 ${\mathsf {P}}\ne {\mathsf {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).

Additionally, a popular generalization of the 2HAM called the staged tile assembly model [7] has been shown to be capable of extremely efficient assembly across a range of parameters [4, 7,8,9, 14]. Does this power come from the increased complexity of verifying that systems assemble intended assemblies and shapes?

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

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

The ${\mathsf {coNP}}^{{\mathsf {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 $\mathsf {NP}$ or $\mathsf {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 $\varSigma$. Each pair of glues $g_1, g_2 \in \varSigma$ has a non-negative integer strength, denoted $\mathrm{str}(g_1, g_2)$. Every set $\varSigma$ contains a special null glue whose strength with every other glue is 0. If the glue strengths do not obey $\mathrm{str}(g_1,g_2) = 0$ for all $g_1 \ne g_2$, then the glues are flexible. Unless otherwise stated, we assume that glues are not flexible.

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 $\varvec{u} = \langle u_x, u_y \rangle \in {\mathbb {Z}}^2, A + \varvec{u}$ denotes the configuration $f \circ A$, 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 + \varvec{u}$ for some vector $\varvec{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$. The shape of an assembly ${\tilde{A}}$ is $\{\mathrm{dom}(A): A \in {\tilde{A}}\}$ where 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, \dots , k-1\}^2} (kx + i, ky + j) \in S'$.

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-stage b-bin mix graph M 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, \dots , 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}= \Big (\bigcup _{k:\ (m_{i-1,k},m_{i,j})\in M_{r,b}} P_{(R_{(i-1,k)},\tau _{i-1,k})}\Big )$.

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.

3 The 2HAM Unique Shape Verification Problem Is ${\mathsf {coNP}}^{{\mathsf {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 ${\mathsf {coNP}}^{{\mathsf {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 ${\mathsf {coNP}}^{{\mathsf {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 ${\mathsf {coNP}}^{{\mathsf {NP}}}$-hard.

Definition 2

( $\forall \exists \mathrm {SAT}$ ). Given a 3-$\mathsf {SAT}$ formula $\phi (x_1, x_2, \dots , x_k, x_{k+1}, \dots , x_n)$, is it true that for every assignment of $x_1, x_2, \dots , x_k$, there exists an assignment of $x_{k+1}, x_{k+2}, \dots , x_n$ such that $\phi (x_1, x_2, \dots , x_n)$ evaluates to T?

The $\forall \exists \mathrm {SAT}$ problem was shown to be ${\mathsf {coNP}}^{{\mathsf {NP}}}$-complete by Stockmeyer [13] (see [12] for further discussion).

Proof

The reduction is from $\forall \exists \mathrm {SAT}$. 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, \dots 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 and true-test assemblies with shape S, and possibly test assemblies. A test assembly is terminal if and only if there is no true assembly for it to attach to, i.e. the assignment of variables $x_1, \dots , x_k$ has no corresponding assignment of the variables $x_{k+1}, \dots , x_n$ such that $\phi (x_1, \dots , x_n)$ is “true”.

Fig. 1.

Steps of the 2HAM USV ${\mathsf {coNP}}^{{\mathsf {NP}}}$-hardness reduction.

$\mathsf {SAT}$ Assemblies. 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$ through $x_k$ can be combined with some assignment of the variables $x_{k+1}$ through $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 [11].

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$ to $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 [11]. 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. 1(c)). 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. 1(b)). 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. 1(d)). 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} \dots x_n$ such that $\phi (x_1, \dots , x_n)$ is “true”. Thus, the test assembly with this assignment of variables $x_1, \dots , 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 “yes”, every test assembly attaches to a true assembly and thus every terminal assembly (true-test assemblies and false assemblies) has shape S.

Theorem 2

The 2HAM USV problem is in ${\mathsf {coNP}}^{{\mathsf {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 $\mathsf {NP}$ subroutine to verify the second condition. The algorithm is executed by a $\mathsf {coNP}$ machine, implying that “false” is returned if any of the non-deterministic branches return “false”, and otherwise returns “true”.

4 Staged Unique Assembly Verification Is ${\mathsf {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?

Fig. 2.

(a) The tile set used in the staged $\mathsf {coNP}$-hardness reduction. (b) The subsets of tiles included in separated initial bins within the first stage of the system. (Color figure online)

Theorem 3

The staged UAV problem (for $\tau =2$ 4-stage systems) is $\mathsf {coNP}$-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$.

The Tileset. The tiles used in our construction are shown in Fig. 2(a). In particular, for each variable $x_i \in \{x_1, x_2, \dots , x_n\}$ and clause $c_j \in \{c_1, c_2, \dots , 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. 2(b)(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. 2(b)(ii–iii) are used if $x_i$ does not (and $\overline{x_i}$ does satisfy) clause $c_j$.

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)

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-deterministically via attaching $0-\mathrm {block}_{i,j}$ and $1-\mathrm {block}_{i,j}$ assemblies for each $i \in \{1, 2, \dots , 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.

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. 3(b)). 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. 3(a)). 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. 3(c)).

A satisfying assignment of $\phi$ corresponds to m rows attaching to form a complete “satisfying” assembly (Fig. 4(b)). 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. 4(a)). 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 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. 4(c) 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. 4(c) is uniquely assembled if an only if no such satisfying assembly exists.

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)

5 Staged Unique Assembly Verification Is ${\mathsf {coNP}}^{{\mathsf {NP}}}$-Hard

Theorem 4

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

Fig. 5.

The assemblies at respective stages for the ${\mathsf {coNP}}^{{\mathsf {NP}}}$-hardness reduction for the staged UAV problem. (Color figure online)

Proof

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

Stages 1–3: The $\mathsf {SAT}$ Assemblies. 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, \dots , 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.

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, \dots , 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, \dots , x_k$ with no satisfying assignment of the remaining variables $x_{k+1}, x_{k+2}, \dots , 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, \dots , 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”.

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 ${\mathsf {coNP}}^{{\mathsf {NP}}}$-hard.

Corollary 1

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

6 Staged $\mathsf {PSPACE}$ Containment

Here we prove that the staged UAV and USV problems are in $\mathsf {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. and 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 [13]. As a reminder, $\mathrm {\Sigma }^{\mathsf {P}}_{i+1} = {\mathsf {NP}}^{\mathrm {\Sigma }^{{\mathsf {P}}}_i}, \mathrm {\Pi }^{\mathsf {P}}_{i+1} = {\mathsf {coNP}}^{\mathrm {\Sigma }^{{\mathsf {P}}}_i}$, and $\mathrm {\Sigma }^{\mathsf {P}}_0 = \mathrm {\Pi }^{\mathsf {P}}_0 = {\mathsf {P}}$.

Lemma 1

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

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

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

Due to space limitations, the proof of this lemma is omitted.

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 }^{\mathsf {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|?

In the algorithm below, ${\mathcal {T}}_s$ and ${\mathcal {U}}_s$ are algorithms for the TIBV$_{s}$ and UIBV$_{s}$ problems, respectively.

The algorithm runs as a $\mathsf {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).

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 $\mathsf {PH}$, but every instance can be solved by an algorithm that runs at a fixed level ($\mathrm {\Pi }^{\mathsf {P}}_{2s}$) of the hierarchy. Since it is a well-known that ${\mathsf {PH}}{} \subseteq {\mathsf {PSPACE}}{}$, this gives the desired result:

Corollary 2

The staged UAV problem is in $\mathsf {PSPACE}$.

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 }^{\mathsf {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 }^{\mathsf {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|).

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

Corollary 3

The staged USV problem is in $\mathsf {PSPACE}$.

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 ${\mathsf {coNP}}^{{\mathsf {NP}}}$-hardness and $\mathsf {PSPACE}$ containment of the staged UAV and USV problems. We believe that the approach of differentiating between satisfying and non-satisfying 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 are $\mathsf {PSPACE}$-complete.

Conjecture 2

The stage-s UAV and stage-s USV problems are $\mathrm {\Pi }^p_{\varOmega (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 $\mathsf {coNP}$-complete, while the minimum tile set problem of finding the minimum number of tiles that uniquely assemble into a given shape is ${\mathsf {NP}}^{{\mathsf {NP}}}$-complete [2]. We now know that the 2HAM USV problem is ${\mathsf {coNP}}^{{\mathsf {NP}}}$-complete (Sect. 3); does the corresponding optimization problem also rise in the hierarchy?

Conjecture 3

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