>> That is quite literally a formal proof that "regex+backreferences" is NP-complete, since SAT is the index NP-complete problem.
> I'd love for you to elaborate a bit more on this.
I'm not the original poster, but I'll have a go.
SAT is NP-Hard. In other words, any literally any NP problem can be efficiently[0] converted to SAT, and any solution can then be efficiently[0] converted back to a solution to the original.
Example: Think of the problem of factoring integers. Someone gives you an integer to factor, with a little work you can create a SAT instance, solve that, and then read off the factorisation of the original integer. SAT is, in some real sense, at least has hard as INT.
So there is a proof that SAT is at least as hard as every NP problem. That's what we call "NP-Hard".
Now someone has shown that they can solve SAT problems by using regex_backtrack. That means that every NP problem can be converted to SAT, then converted to regex+backtrack, solved, and the solution to the original read out from the result.
Thus regex+backtrack is at least as hard as every NP problem.
Now in the case of SAT, it itself is NP. So the combination of being NP and being NP-Hard is called "NP-Complete", or NPC. So SAT is an example of a problem that's NPC.
What has not been shown (I think) is that regex+backtrack is in NP. Showing that a solution to regex+backtrack implies a solution to SAT shows that regex+backtrack is NP-Hard.
If the linked article also shows that regex+backtrack is NP, then it is therefore NPC. But we can see that regex+backtrack is in NP, because verifying an alleged match is a polynomial time operation.
So regex-backtrack is NPC.
+--------------------+
| |
NP-Hard -> | |
| ,------------. |
\ / \ /
X NP-Complete X
/ \ / \
/ `------------' \
NP -> | |
| |
. +------------+ ,
\ | Polynomial | /
`--+------------+--'
[0] For a technical definition of "efficient"