Sat solver on top of regex matcher • Hacker News Board

Re: Sat solver on top of regex matcher

#21

Post by gbacon » Mon, Jun 22, 2020, 2:09 PM UTC

awirth wrote: post #2

This reduction is really cool. I love reductions like this. Is there a general consensus to use "regular expression" to refer to the actual regular ones and "regex" to refer to the non-regular variants?

Yes, for at least ten years and likely much longer.

https://cstheory.stackexchange.com/q/448/362

Re: Sat solver on top of regex matcher

#22

Post by pradn » Mon, Jun 22, 2020, 2:18 PM UTC

PaulHoule wrote: post #19

That is quite literally a formal proof that "regex+backreferences" is NP-complete, since SAT is the index NP-complete problem.

I assume this result is already known in the literature?

Re: Sat solver on top of regex matcher

#23

Post by gbacon » Mon, Jun 22, 2020, 2:23 PM UTC

PaulHoule wrote: post #19

That is quite literally a formal proof that "regex+backreferences" is NP-complete, since SAT is the index NP-complete problem.

Proving that a problem is NP-complete requires proving that it is NP-hard and in NP. Reducing SAT to regex matching with backreferences does the former. The latter requires proving that any solution can be checked in polynomial time.

The author is also incorrect in stating However the author incorrectly states that only 3SAT problems are solvable. Proof that 3SAT is NP-hard does not exclude broader SAT.

Re: Sat solver on top of regex matcher

#24

Post by awirth » Mon, Jun 22, 2020, 2:30 PM UTC

gbacon wrote: post #21

awirth wrote: post #2

This reduction is really cool. I love reductions like this. Is there a general consensus to use "regular expression" to refer to the actual regular ones and "regex" to refer to the non-regular variants?

Yes, for at least ten years and likely much longer. https://cstheory.stackexchange.com/q/448/362

Interesting, I wasn't aware of the history.

Personally I make the distinction, but I've noticed many many people do not, hence the question.

Re: Sat solver on top of regex matcher

#25

Post by gbacon » Mon, Jun 22, 2020, 2:38 PM UTC

awirth wrote: post #24

gbacon wrote: post #21

Earlier quoted context omitted.

Yes, for at least ten years and likely much longer. https://cstheory.stackexchange.com/q/448/362

Interesting, I wasn't aware of the history. Personally I make the distinction, but I've noticed many many people do not, hence the question.

People without theoretical CS background probably think of regular expressions (or regexes for short) as just text-matching thingies that sometimes give you two problems and would look at you blankly if you mention the Chomsky hierarchy. When we don’t know there’s a distinction to be made, we go for economy of expression.

Re: Sat solver on top of regex matcher

#26

Post by klyrs » Mon, Jun 22, 2020, 2:48 PM UTC

pradn wrote: post #22

PaulHoule wrote: post #19

That is quite literally a formal proof that "regex+backreferences" is NP-complete, since SAT is the index NP-complete problem.

I assume this result is already known in the literature?

This doesn't show a date but archive.org has snapshots dating back to 2001

https://perl.plover.com/NPC/

Re: Sat solver on top of regex matcher

#27

Post by klyrs » Mon, Jun 22, 2020, 2:52 PM UTC

That "popcnt1" is also known as a 1-hot constraint.

https://en.m.wikipedia.org/wiki/One-hot

Re: Sat solver on top of regex matcher

#28

Post by dtech » Mon, Jun 22, 2020, 2:53 PM UTC

gbacon wrote: post #23

PaulHoule wrote: post #19

That is quite literally a formal proof that "regex+backreferences" is NP-complete, since SAT is the index NP-complete problem.

Proving that a problem is NP-complete requires proving that it is NP-hard and in NP. Reducing SAT to regex matching with backreferences does the former. The latter requires proving that any solution can be checked in polynomial time. The author is also incorrect in stating However the author incorrectly states that only 3SAT problems are solvable. Proof that 3SAT is NP-hard does not exclude broader SAT.

While not a formal proof, it is fairly obvious that verifying a match is in P. Just fill in the captured groups from the answer in the regex and see if it corresponds to the input text.

Every SAT problem can be converted into a 3-SAT problem so that's also not really an issue, they are both NPC

Re: Sat solver on top of regex matcher

#29

Post by simonebrunozzi » Mon, Jun 22, 2020, 2:58 PM UTC

PaulHoule wrote: post #19

That is quite literally a formal proof that "regex+backreferences" is NP-complete, since SAT is the index NP-complete problem.

This line is super smart, and yet, despite I should know a lot about regex and NP-complete, my head feels dizzy as I try to make full sense of it. A sign I'm getting old or dumb, perhaps :(

Jokes apart: I'd love for you to elaborate a bit more on this. I'm pretty sure I would benefit a lot from a more expanded, "dumber" explanation.

Re: Sat solver on top of regex matcher

#30

Post by hansvm » Mon, Jun 22, 2020, 3:40 PM UTC

lifthrasiir wrote: post #11

Thorrez wrote: post #3

> Another practical usage I've heard: match "string" or 'string', but not "string'. You don't need backreferences for that: '[^']*'|"[^"]*"

The common case of only two pairs of quotes is indeed regular, but if you want to support either all Unicode quotes (about 60 pairs of them) or C++11 raw string literals `R"delim(...)delim"` (intrinsically not regular) you are out of luck.

For any finite set of quotation character pairs you can get away with a strategy like `(left_char1)[^right_char1](right_char1)|(left_char2)[^right_char2](right_char2)|...`. Escape characters aren't much harder to accommodate.