{'fraction_non_alphanumeric': 0.04088155003662028, 'fraction_numerical': 0.008955323257207538, 'mean_word_length': 3.7870916334661353, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 4, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 3, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Reachability Is NP-Complete Even for the Simplest Neural Networks

We investigate the complexity of the reachability problem for (deep) neural networks: does it compute valid output given some valid input? It was recently claimed that the problem is NP-complete for general neural networks and conjunctive input/output specifications. We repair some flaws in the original upper and lower bound proofs. We then show that NP-hardness already holds for restricted classes of simple specifications and neural networks with just one layer, as well as neural networks with minimal requirements on the occurring parameters.


Introduction
Deep learning has proved to be very successful for highly challenging or even otherwise intractable tasks in a broad range of applications such as image recognition [11] or natural language processing [5] but also safety-critical applications like autonomous driving [4], medical applications [12], or financial matters [2]. These naturally come with safety concerns and the need for certification methods. Recent such methods can be divided into (i) Adversarial Attack and Defense, (ii) Testing, and (iii) Formal Verification. A comprehensive survery about all three categories is given in [6].
The former two cannot guarantee the absence of errors. Formal verification of neural networks (NN) is a relatively new area of research which ensures completeness of the certification procedure. Recent work on sound and complete verification algorithms for NN are mostly concerned with efficient solutions to their reachability problem NNReach [1,3,8,13]: given an NN and symbolic specifications of valid inputs and outputs, decide whether there is some valid input such that the corresponding output is valid, too. This corresponds to the understanding of reachability in classical software verification: valid sets of inputs and outputs are specified and the question is whether there is a valid input that leads to a valid output. Put differently, the question is whether the set of valid outputs is reachable from the set of valid inputs. The difference to classical reachability problems in discrete state-based programs is that there reachability is a matter of lengths of a connection. In NN this is given by the number of layers, and it is rather the width of the continuous state space which may cause unreachability.
Solving NNReach is interesting for practical purposes. An efficient algorithm can be used to ensure that no input from some specified set of inputs is misclassified or that some undesired class of outputs is never reached. In applications like autonomous-driving, where classifiers based on neural networks are used to make critical decisions, such safeguards are indispensable.
However, all known algorithms for NNReach show the same drawback: a lack of scalability to networks of large size which, unfortunately, are featured typically in real-world applications [10]. This is not a big surprise as the problem is NP-complete. This result was proposed by Katz et al. [8] for NN with ReLU and identity activations, and later also by Ruan et al. [14]. While there is no reason to doubt the NP-completeness claim, the proofs are not stringent and contain flaws.
The argument for the upper bound in [8] misses the fact that real inputs are not necessarily polynomially bounded in size. In fact, guessing values in R is not even effective without a bound on the size of their representation. Such a bound is closely linked to the question whether such values can be approximated upto some precision. The proof by Katz et al. makes no argument for any bound on the representation of such values, let alone a polynomial one. 1 The arguments for the lower bound by a reduction from 3sat in [8] and [15] rely on a discretisation of real values to model Boolean values. This does not work for the signum function σ used by Ruan et al. as it is not congruent for sums: e.g. σ(−3) = σ(−1) but σ(2 + (−3)) = σ(2 + (−1)), showing that one cannot simply interpret any negative number as the Boolean value false etc. As a consequence, completeness of the construction fails as there are (real) solutions to NNReach which do not correspond to (discrete) satisfying 3sat assignments. Katz et al. seem to be aware of this and use a slightly more elaborate discretisation in their reduction, but unfortunately it still suffers from similar problems. 2 We start our investigations into the complexity of NNReach by fixing these issues in Sec. 3. We provide a different argument for membership in NP which shows that the need for nondeterminism is not to be sought in the input values but in the use of ReLU nodes. As a corollary we obtain polynomial decidability for NN with a bounded number of such nodes. We also address the issue of discretisation of real values in the lower bound proof, fixing the construction given by Katz et al. We do not address the one by Ruan et al. further, as this does not provide any further insights or new results.
We then observe that the reduction from 3sat constructs a very specific class of NNReach instances which we call C(3sat). NN from this class have a fixed amount of layers but scaling input and output dimension as well as layer size. This raises the question whether, in comparison to the networks from C(3sat), reducing the amount of layers or fixing dimensionality leads to a class of networks for which NNReach is efficiently solvable. In Sec. 4 we show that the answer to this is mostly negative: NP-hardness of NNReach holds for NN with just one layer and an output dimension of one. While this provides minimal requirements on the structure of NN for NNReach to be NP-hard, we also give minimal criteria on the weights and biases in NN for NP-hardness to hold. Thus, the computational difficulty of NNReach in the sense of NP-completeness is quite robust. The requirements on the structure or parameters of an NN that are needed for NP-hardness to occur are easily met in practical applications. Due to space restrictions, some technical proof details are deferred to the appendix.
We conclude in Sec. 5 with references to possible future work.

Preliminaries
Definition 1. A neural network (NN) N is a layered graph that represents a function of type IR n → IR m . The first layer l = 0 is called the input layer and consists of n nodes. The i-th node computes the output y 0i = x i where x i is the i-th input to the overall network. Thus, the output of the input layer (y 00 , . . . , y 0(n−1) ) is identical to the input of N .
A layer 1 ≤ l ≤ L − 2 is called hidden and consists of k nodes. Note that k must not be uniform across the hidden layers of N . Then, the i-th node of layer l computes the output y li = σ li ( j c (l−1) ji y (l−1)j + b li ) where j iterates over the output dimensions of the previous layer, c (l−1) ji are real constants which are called weights, b li is a real constant which is called bias and σ li is some (typically nonlinear) function called activation. The outputs of all nodes of layer l combined gives the output (y l0 , . . . , y l(k−1) ) of the hidden layer.
The last layer l = L − 1 is called the output layer and consists of m nodes. The i-th node computes an output y (L−1)i in the same way as a node in a hidden layer. The output of the output layer (y (L−1)0 , . . . , y (L−1)(m−1) ) is considered as the output of the network N .
The output of a neural network N under input x is denoted N (x). If a node in a layer l > 0 has less inputs than there are outputs in layer l − 1 then we assume that the unconsidered outputs of l − 1 are weighted with zero. We only consider networks where nodes in hidden layers have the identity or the ReLU function, and nodes in the output layer have the identity as activation. The ReLU function is defined as x → max(0, x). Nodes with ReLU or identity activation are called ReLU nodes or identity nodes, respectively. Given some input to the NN, we say that a ReLU node is active, resp. inactive if the input for its activation function is greater, resp. less than or equal to 0. We visualize an NN as a directed graph with weighted edges. An example is given in Fig. 1.
Our main interest lies in the validity of specifications over the output values of NN given specifications over their input values. These specifications are expressed as conjunctions of linear constraints on the input and output variables of a network.

Definition 2.
A specification ϕ for a given set of variables X is defined by the following grammar: where b, c are rational constants and x ∈ X is a variable.
We use t ≥ b and t = b as syntactic sugar for −t ≤ −b and t ≤ b ∧ −t ≤ −b. Furthermore, we use ⊤ for x + (−x) = 0 and ⊥ for x + (−x) = 1 where x is some variable. We call a specification ϕ simple if for all t ≤ b it holds that t = c · x for some rational constant c and variable x.
Definition 3. Specification ϕ(x 0 , . . . , x n−1 ) is true under x = (r 0 , . . . , r n−1 ) ∈ R n if each inequality in ϕ is satisfied in real arithmetic with each x i set to r i .
We write ϕ(x) for the application of x to the variables of ϕ. If there are less variables in ϕ than dimensions in x we ignore the additional values of x. If we consider a specification ϕ in context of a neural network N we call it an input or output specification and assume that the set of variables occurring in ϕ is a subset of the input respectively output variables of N .
Definition 4. The decision problem NNReach is the following: given a neural network N , input specification ϕ in (x 0 , . . . , x n−1 ) and output specification ϕ out (y 0 , . . . , y m−1 ), is there x ∈ IR n such that ϕ in (x) and ϕ out (N (x)) are true?

Membership in NP
The argument used by Katz et al. to show membership of NNReach in NP can be summarized as follows: nondeterministically guess an input vector x as a witness, compute the output N (x) of the network and check that ϕ in (x) ∧ ϕ out (N (x)) holds. It is indisputable that the computation and check of this procedure are polynomial in the size of N , ϕ in , ϕ out and the size of x. However, for inclusion in NP we also need the size of x to be polynomially bounded in the size of the instance given as (N, ϕ in , ϕ out ). There may be an argument for this, for instance based on the correspondence between size of x and required approximation precision for such values. However, we are not aware of such an argument, let alone a striking one, and there is also a simpler way of obtaining the upper bound.
The problem of solving a ReLU-linear program is: given Φ, decide whether there is a solution to it.
Any ReLU-linear program without ReLU-equalities is a linear program in the usual sense, and linear programs are known to be solvable in polynomial time [7]. Lemma 1. The problem of solving a ReLU-linear program is in NP.
Proof. Suppose a ReLU-linear program Φ with l ReLU-equalities is given. Existence of a solution can be decided as follows. Guess, for each ReLU-equation Let a = (a 0 , . . . , a l−1 ). Next, let Φ a result from Φ by replacing each χ k by the following (in-)equalities.
The following is not hard to see: (i) Using standard transformations, Φ a can be turned into a linear program of size linear in Φ. (ii) Any solution to Φ a is also a solution to Φ, (iii) If Φ has a solution, then there is a ∈ {0, 1} l such that Φ a has a solution. This can be created as follows. Let x be a solution to Φ. For each ReLU-equation χ k as above, let a k = 1 if the corresponding sum is non-negative, otherwise let a k = 0. Then x is also a solution for Φ a . Thus, ReLU-linear programs can be solved in nondeterministic polynomial time by guessing a, and then constructing the linear program Φ a and solving it.

⊓ ⊔
With this definition of a ReLU-linear program and the corresponding lemma at hand, we are set to prove NP-membership of NNReach.
ReLU-linear program Φ I contains the following (in-)equalities.
ϕ in and ϕ out (with each conjunct seen as one (in-)equality), -for each non-ReLU node v li computing j c The claim on the size of Φ I should be clear. Moreover, note that a solution x to I can be extended to an assignment x ′ of real values at every node of N , including values y for the output nodes of N s.t., in particular N (x) = y. Then x ′ is a solution to Φ I . Likewise, a solution to Φ I can be turned into a solution to I by projection to the input variables.
Hence, NNReach polynomially reduces to the problem of solving ReLUlinear programs which, by Lem. 1 is in NP.

⊓ ⊔
It is interesting to point out the role of witnesses for positive instances of the NNReach problem: it is tempting to regard values to the input nodes of the NN as potential witnesses as done by Katz et al. but, as mentioned before, for as long as there is no argument for their polynomial boundedness these are not suitable witnesses in an NP procedure. Instead, Thm. 1 above shows that an assignment to the ReLU nodes as being in-/active can serve as such a witness. This immediately yields a polynomial fragment of NNReach. Corollary 1. The reachability problem for NN with a bounded number of ReLU nodes is decidable in polynomial time.

NP-Hardness
Katz et al. try to build a polynomial-time reduction from 3sat to NNReach. The underlying idea is to encode the structure of a 3sat formula in a neural network and the existence of a satisfying assignment for this formula in the corresponding input-and output-specifications. Consider the 3sat instance with four propositional variables and three clauses, and let (N, ϕ in , ϕ out ) be the NNReach instance resulting from the mapping of ψ according to the reduction.
To understand the structure of N we make use of so-called gadgets, specified in Fig. 2. Each gadget is a compact NN and is used to describe a functional subcomponent of N . Using these gadgets, the network N is depicted in Fig. 3.
Ignoring the bool-gadgets for the moment, assume that input values are taken from {0, 1} instead of R. The function computed by N is described as follows. Each of the three or-gadgets together with their connected not-gadgets represent one of the clauses in ψ. From Fig. 2 we can infer that the not-gadgets negate their inputs and that the or-gadgets output 1 if at least one input is 1 and 0 otherwise. Hence, if an or-gadget outputs 1 then the current input, viewed as an assignment to the propositional variables in ψ, satisfies the corresponding clause. The and-gadget simply sums up all of its inputs and, thus, we get that y is equal to 3 iff each or-gadget outputs one. Therefore, with the output specification ϕ out := y = 3, we get a reduction from 3sat to NNReach, provided that input values are externally restricted to {0, 1}.
But NN are defined for all real-valued inputs, so we need further adjustments to make the reduction complete. First, note that it is impossible to write an input specification ϕ in (x) which is satisfied by x iff x ∈ {0, 1} n because {0, 1} n is not a hyperrectangle in R n but conjunctions of inequalities only specify hyperrectangles. This is where we make use of bool-gadgets. Let ε be a very small constant. A bool-gadget with input x and output z computes Note that no weights are depicted as these are specified inside the gadgets.
a bool-gadget to each input x i in N and using the simple specifications we would get a correct translation of ψ. Note that the constraint on y is no longer y = 3 as the valid inputs to N , determined by the bool-gadgets and their output constraints, are not exactly 0 or exactly 1. However, the claim about bool-gadgets is wrong. Consider a bool-gadget with very small ε such that it is safe to assume ε < 2ε < 1 − ε. Then, for x = 2ε we have z = 0, which contradicts the claim. In fact, it can be shown that for each ε ≤ 1 2 and each input x ∈ [0; 1] the output z is an element of [0; ε]. Clearly, this is not the intended property of these gadgets. But with some adjustments to the bool-gadgets we can make the reduction work.
A bool * -gadget is a neural network with functional form IR → IR shown in Fig. 2. It computes the function z = max 0, where x is the input variable and z is the output variable. For this bool * -gadget we can show a similar statement as it was intended for the bool-gadgets in the original proof. Proof. Note that z = max 0, From this we immediately get that z = 0 if x = 0 or x = 1, and z = 0 for all other values of x.
⊓ ⊔ Now, replacing all bool-gadgets with bool * -gadgets in the construction and using the simple specifications ϕ in = ⊤ and ϕ out = n−1 i=0 z i = 0 ∧ y = m for a 3sat-instance with n propositional variables and m clauses, we get a correct reduction from 3sat to NNReach.

Theorem 2. NNReach is NP-hard.
One could argue that the networks resulting from the reduction of 3sat are not typical feed-forward neural networks as they do not follow a layerwise structure. A reason for this is that some inputs are connected to not-gadgets where some are not and that the outputs z i are not in the same layer as the output y. This can of course be fixed by introducing additional dummy nodes.

NP-Hardness Holds in Very Restricted Cases Already
Let C(3sat) be the class of NNReach instances which are obtained as images under the reduction presented in the previous section. Note that the NN of C(3sat) are already quite restricted; they possess only a fixed number of layers. In this section we strengthen the NP-hardness result by constructing even simpler classes of NN for which NNReach is NP-hard already. Sect. 4.1 studies the possibility to make these NN structurally as simple as possible; Sect. 4.2 shows that requirements on weights and biases can be relaxed whilst retaining NPhardness.

Neural Networks of a Simple Structure
We consider NN with just one hidden layer of ReLU nodes and an output dimension of one. As before, we can establish a reduction from 3sat. Theorem 3. NNReach is NP-hard for NN with output dimension one, a single hidden layer and simple specifications.
Proof. Let ψ be a 3sat formula with n propositional variables X i and m clauses l j . We slightly modify the construction of a network N in the proof of Thm. 2. First, we remove the last identity node of all bool * -gadgets in N and directly connect the two outputs of their ReLU nodes to the and-gadget, weighted with 1. Additionally, we merge not-gadgets and or-gadgets in N . Consider the orgadget corresponding to some clause l j . The merged gadget has three inputs x j0 , x j1 , x j2 and computes max 0, 1 − 2 k=0 f j (x j k ) where f j (x j k ) = x j k if X j k occurs positively in l j and f j (x j k ) = 1 − x ij if it occurs negatively. It is straightforward to see that the output of such a gadget is 0 if at least one positively (resp. negatively) weighted input is 0, resp. 1, and that the output is 1 if all positively weighted inputs are 1 and all negatively weighted inputs are 0. These merged gadgets are connected with weight −1 to the and-gadget. Once done for all bool * -, not-and or-gadgets, the overall output y of N is given by Note that N has input dimension n, a single hidden layer of 2n + m ReLU nodes and output dimension 1. Now take the simple specifications ϕ in = n−1 i=0 x i ≥ 0 ∧ x i ≤ 1 and ϕ out = y = n 2 . We argue that the following holds for a solution to (N, ϕ in , ϕ out ): (i) all x i are either 0 or 1, and (ii) the output of each merged or-gadget is 0. To show (i), we assume the opposite, i.e. there is a solution with x k ∈ (0; 1) for some k. This implies that Therefore, this cannot be a solution for (N, ϕ in , ϕ out ) as it does not satisfy y = n 2 . To show (ii), assume there is a solution such that one merged or-gadget outputs a value different from 0. Then, − m−1 Again, this is a contradiction. Putting (i) and (ii) together, a solution for (N, ϕ in , ϕ out ) implies the existence of a model for ψ. For the opposite direction assume that ψ has a model I. Then, a solution for (N, ϕ in , ϕ out ) is given by In the previous section, especially in the arguments of Cor. 1, we pointed out that the occurrence of ReLU nodes is crucial for the NP-hardness of NNReach. Thus, it is tempting to assume that any major restriction to these nodes leads to efficiently solvable classes. Proof. We prove NP-hardness via a reduction from 3sat. The reduction works in the same way as in the proof of Thm. 2, but with the following adjustments. We replace the or-gadgets with simple identity-nodes, we do not include the andgadget, and we set the output specification to ϕ out = n−1 i=0 z i = 0 ∧ m i=0 y i ≥ 1, where y i is the output of the i-th identity-node replacing the former i-th orgadget, z i is the output of the i-th BOOL-gadget, n is the number of propositional variables and m the number of clauses in the considered 3sat-instance. Note that this is a simple specification and that the only ReLU nodes in this network are inside the bool * -gadgets, which have only one non-zero input. Now, if each z i = 0 then the value of an output y i is equivalent to the number of inputs equal to 1. The correctness of this reduction is argued int the exaxt same way as in in the original one.
⊓ ⊔ . . . Fig. 4. Gadgets used to show that NNReach is NP-hard if restricted to C ({−c, 0, d}) . A non-weighted outgoing edge of a gadget is connected to a weighted incoming one of another gadget in the actual construction or are considered as outputs of the overall neural networks.

Neural Networks with Simple Parameters
One could argue that the NP-hardness results in Thm. 2 and 3 are only partially applicable to real world problems as the constructed NN use very specific combinations of weights and biases, namely −1, 0, 1 2 and 1, which may be unlikely to occur in this exact combination in real-world applications. We show that NNReach is already NP-hard in cases where only very weak assumptions are made on the set of occurring weights and biases.
For P ⊆ Q let C(P ) be the class of NNReach instances whose NN only use weights and biases from P and simple specifications. We will show that NP-hardness already occurs when P contains three values: 0, some positive and some negative value. We make use of the same techniques as in Sec. 3 and assume that the general idea of gadgets and the reduction from 3sat to NNReach are known.
Definition 6. Let c, d ∈ Q >0 and ψ be a 3sat-formula with n propositional variables X i and m clauses l j . The network N −c,d,ψ is a network with 2n inputs, two for each X i , called x i and x i . We describe the structure of N −c,d,ψ using the gadgets from Fig. 4: -Each input x i is connected to both inputs of a disc-gadget and this gadget is connected with weight −c to a chain of five identity nodes interconnected with weight −c. We call the output of the last node of this chain z i . -Each pair x i and x i is connected to an eq 0 -gadget and this gadget is connected with weight −c to a chain of six identity nodes interconnected with weight −c. We call the output of the last node of this chain e i .
-Each input x i is connected to a norm-gadget. Analogously, each x i is connected to a norm-gadget. -If c ≥ 1 (resp. c < 1) then there are m or A -gadgets (resp. or B -gadgets), one for each l j s.t. if X i occurs positively in l j then the output of the normgadget connected to x i is connected and if X i occurs negatively the output of the norm-gadget conntected to x i is connected. -The outputs of all or A -gadgets respectively or B -gadgets are connected to a single and-gadget. We denote the output of this and-gadget with y.
Note that each N −c,d,ψ has eight layers and output dimension 2n + 1. Moreover, N −c,d,ψ ∈ C({−c, 0, d}). Next, we need to clarify some properties of the used gadgets. Proof. We start with property 3.1 and assume that the inputs x 0 , x 1 are equal. We can infer from the depiction in Fig. 4 that the output of a disc-gadget is given by d − c max(0, dx 0 ) − c max(0, −cx 1 ). At this point we make a case distinction. With these properties at hand, we are suited to prove our main statement of this section.
Clearly, (N −c,d,ψ , ϕ in , ϕ out ) can be constructed in time polynomial in the size of ψ. For the correctness of the construction assume that ψ has a model I. We claim that (N −c,d,ψ , ϕ in , ϕ out ) is solved with otherwise, and x i = −x i . Note that ϕ in is trivially satisfied. So apply these inputs to N −c,d,ψ . According to Lem. 3.1, all outputs z i are 0. It is easily verified that all outputs e i are 0 as well. Thus, it is left to argue that y = m · d 2 c 4 . Consider one of the or A|B -gadgets occurring in N −c,d,ψ , corresponding to a clause l j . Its inputs are given by the norm-and normgadgets connected to the inputs x i , resp. x i corresponding to the X i occurring in l j . According to Lem. 3.2 and 3 these inputs are either 0 or −dc. If l j is satisfied by I then there is at least one input to the or A|B -gadget that is equal to −dc. From the fact that ψ is satisfied by I and Lem. 3.4 it follows that each or A|B -gadget outputs dc 4 . Therefore, the output y of N −c,d,ψ is m · d 2 c 4 . This means that ϕ out is valid as well.
Consider now the converse direction. A solution for (N −c,d,ψ , ϕ in , ϕ out ) must yield that all x i are 1 c or − d c 2 and x i = x i as all z i and e i have to equal 0. Therefore, all m or A|B -gadgets have to output dc 4 as y must equal m · d 2 c 4 . This implies that each or A|B -gadget has at least one input that is −dc which in turn means that there is at least one indirectly connected If d = c and we allow for arbitrary specifications we can show that 0 as a value for weights or biases is unnecessary to keep the lower bound. Proof. This is done in the same way as the proof of Thm. 5 with some slight modifications. We only sketch this reduction by describing the differences compared to the instances (N −c,c,ψ , ϕ in , ϕ out ) resulting from the reduction used in Thm. 5.
We do not use eq 0 -gadgets in the network but add for each input x i the conjunct x i = −x i to the input specification ϕ in . This also means that we do not include n−1 i=0 e i = 0 in the output specification ϕ out . Consider the weights between the input and the first hidden layer. If the inputs x i and x i were originally weighted with zero we set the weights corresponding to x i and x i to be c. In combination with the input constraint x i = −x i this is equal to weighting x i and x i with zero. If x i (x i ) was originally weighted with c we have to set the weight of x i (x i ) to be −c. If it was weighted with −c we have to set the weight of its counterpart to be c. This leads to the case that all non-zero inputs of a node in the first hidden layer are doubled compared to the same inputs in a network N −c,c,ψ . Consider now the weights between two layers l and l + 1 with l > 0. For each node in l we add a node in the same layer with the same input weights. If the output of a node in layer l was originally weighted with zero then we weight it with c and the corresponding output of its copy with −c. If the output was originally weighted with weight c (−c) then we weight the output of the copy node with c (−c), too. As before, this doubles the input values at the nodes in layer l + 1, which means that compared to a network N −c,c,ψ the output value of our modified network is multiplied by 2 7 . Thus, we have to change the output constraint of y to be y = 2 7 (m · c 6 ). Note that these modifications give a network using only the weights −c and c.
To get rid of zero bias, we add the inputs x bias,1 , x bias,1 , . . . , x bias,7 , x bias,7 to the network and add the input constraints x bias,i = − i−1 j=0 1 2 j+1 c j and x bias,i = −x bias,i to ϕ in . Then, we set the bias of all nodes which originally had a zero bias to be c. For x bias,i with i > 1 we add a chain of i − 1 identity nodes each with bias c and interconnected with weight c and connect this chain with weight c to x bias,i and −c to x bias,i . All other weights are assumed to be zero which is realized using the same techniques as described in the previous paragraph. If a node in the first hidden layer originally had a zero bias we weight the input x bias,1 with c and x bias,i with −c. If the input specification holds then the bias plus these inputs sums up to zero. If a node in some layer l ∈ {2, . . . , 7} originally had a zero bias we weight the output of the last node of the chain corresponding to x bias,l and its copy with c. Again, if the input specification holds, the bias value of this node is nullified. This modification ensures that the network is from C({−c, c}).

Conclusion
We investigated the computational complexity of the reachability problem for NN with ReLU and identity activations. We revised the original proof of its NP-completeness, fixing flaws in both the upper and lower bound, and showed that the parameter driving NP-hardness is the number of ReLU nodes. Furthermore, we showed that NNReach is difficult for very restricted classes of small NN already, respectively that three parameters of different signum occurring as weights and biases suffice for NP-hardness. This indicates that finding non-trivial classes of NN with practical relevance and polynomial NNReach is unlikely. It remains to be seen whether NP-hardness can be strengthened, for instance for classes of NN with a single hidden layer and a maximum of two non-zero inputs to ReLU nodes, or only one arbitrary positive and only one arbitrary negative weight and bias value. However, possible results here are only of theoretical interest.
From a practical perspective, it would be interesting to see if pure ReLU networks, where every node in a hidden layer has a ReLU activation, lead to similar results as these are more common in practice. Also, investigating the fixed-parameter tractability of the problem more broadly could be promising. It remains to be seen whether there are parameters other than the number of ReLU nodes, like structural properties or dimensionality, whose fixing leads to polynomial decidability. This could yield efficiently solvable classes of NN that are also of practical interest.