3 ms·

>> 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 elabora

>> 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"

sacado2 6y ago
Am I missing something? I read it the other way: all CNF instances can be rewritten as regexp + backreferences, meaning re + backreferences are at least as general that SAT, not at most as. Meaning, they could be higher in the polynomial hierarchy.
- ColinWright 6y ago
  As always, with all these things, there's a non-zero chance that I've mis-spoken myself somewhere. I'm going to "think out loud" on this so people can follow the thought processes. > I read it the other way: OK ... > all CNF instances can be rewritten as regexp + backreferences, By CNF you are referring to instances of the SAT problem. So yes, if you have an instance of the SAT problem, it can be re-written as an instance of regex+backtrack. > meaning re + backreferences are at least as general that SAT, Yes, the regex+backtrack problem is at least as hard as the SAT problem. > ... not at most as. Where did I say that? Here's a stripped-down summary of my comment: * SAT is NP-Hard. * Now someone has shown that they can solve SAT problems by using regex+backtrack. (That's the linked article) * Thus regex+backtrack is at least as hard as every NP problem. * SAT is NP, so it's NPC * regex+backtrack can be seen to be in NP. * So regex-backtrack is NPC. So rewording that: * The linked article shows regex+backtrack >= SAT. * Independently we observe that checking an alleged regex+backtrack solution is a polynomial task, therefore regex+backtrack is in NP. * SAT is in NPC, therefore regex+backtrack <= SAT (because regex+backtrack is in NP). * Thus regex+backtrack = SAT (for some definition of "=") So, I think you must have misread something ... I think everything I've written is correct as stands.
  - sacado2 6y ago
    > we observe that checking an alleged regex+backtrack solution is a polynomial task That's the point I missed at first. That's good news, because I was pretty sure perl regex were accidentally Turing complete, I don't know why.
    - ColinWright 6y ago
      Cool. This sort of thing can be really tough to follow because it's all deeply intertwungle. Glad I got it right. Cheers!

sacado2 6y ago

Am I missing something? I read it the other way: all CNF instances can be rewritten as regexp + backreferences, meaning re + backreferences are at least as general that SAT, not at most as. Meaning, they could be higher in the polynomial hierarchy.

ColinWright 6y ago
As always, with all these things, there's a non-zero chance that I've mis-spoken myself somewhere. I'm going to "think out loud" on this so people can follow the thought processes. > I read it the other way: OK ... > all CNF instances can be rewritten as regexp + backreferences, By CNF you are referring to instances of the SAT problem. So yes, if you have an instance of the SAT problem, it can be re-written as an instance of regex+backtrack. > meaning re + backreferences are at least as general that SAT, Yes, the regex+backtrack problem is at least as hard as the SAT problem. > ... not at most as. Where did I say that? Here's a stripped-down summary of my comment: * SAT is NP-Hard. * Now someone has shown that they can solve SAT problems by using regex+backtrack. (That's the linked article) * Thus regex+backtrack is at least as hard as every NP problem. * SAT is NP, so it's NPC * regex+backtrack can be seen to be in NP. * So regex-backtrack is NPC. So rewording that: * The linked article shows regex+backtrack >= SAT. * Independently we observe that checking an alleged regex+backtrack solution is a polynomial task, therefore regex+backtrack is in NP. * SAT is in NPC, therefore regex+backtrack <= SAT (because regex+backtrack is in NP). * Thus regex+backtrack = SAT (for some definition of "=") So, I think you must have misread something ... I think everything I've written is correct as stands.
- sacado2 6y ago
  > we observe that checking an alleged regex+backtrack solution is a polynomial task That's the point I missed at first. That's good news, because I was pretty sure perl regex were accidentally Turing complete, I don't know why.
  - ColinWright 6y ago
    Cool. This sort of thing can be really tough to follow because it's all deeply intertwungle. Glad I got it right. Cheers!