[Jonathan Castello #27 wrote:](https://forum.azimuthproject.org/discussion/comment/17868/#Comment_17868)

> Matthew, can you elaborate on why reducing Petri net reachability to SAT would imply \\(\text{EXPSPACE} \subseteq \text{NP}\\)? Is Petri net reachability known to be EXPSPACE-complete? I don't think you're necessarily wrong, but the critical step is eluding me.

As I mentioned above, the [Cardoza, Lipton and Meyer (1976)](https://dl.acm.org/citation.cfm?id=803630) establish that reachability for *symmetric* Petri nets is \\(\textsf{EXPSPACE}\\)-complete.

I didn't know this when I wrote my argument yesterday, I had to look it up.

If we let \\(\textsf{PETRI-REACH}\\) be the class of problems reducible to Petri net reachability, then \\(\textsf{EXPSPACE} \subseteq \textsf{PETRI-REACH}\\)

> Approaching this similarly: We have an exponential lower bound on space for Petri net reachability. As you said, this necessarily imposes an exponential lower bound on time, since you can only write one cell per unit time (per tape). Suppose a reduction to SAT existed. If SAT had a subexponential algorithm, then we could defeat the exponential lower bound; so SAT, and by extension every NP-Complete problem, must not be solvable in subexponential time. Therefore, \\(\text{P} \ne \text{NP}\\).

This is good, but we can do better I believe.

Not only does \\(\textsf{PETRI-REACH} \subseteq \textsf{NP} \implies \textsf{NP} \neq \textsf{P}\\), but in fact we have the stronger result:

$$
\textsf{NP} \subsetneq \textsf{PETRI-REACH}
$$

**Proof.**

It's well known that \\(\textsf{NP} \subseteq \textsf{PSPACE}\\) (see, for instance [Arora and Barak (2007), ยง4.2, pg. 78](http://theory.cs.princeton.edu/complexity/book.pdf)).

We also know that \\(\mathsf{PSPACE} \subsetneq \mathsf{EXPSPACE}\\) from the [space hierarchy separation theorem](https://en.wikipedia.org/wiki/Space_hierarchy_theorem).

Finally we have \\(\mathsf{EXPSPACE} \subseteq \textsf{PETRI-REACH}\\) by [Cardoza et al. (1976)](https://dl.acm.org/citation.cfm?id=803630).

Hence \\(\textsf{NP} \subsetneq \textsf{PETRI-REACH}\\).

\\(\Box\\)