10 ms·

Sat solver on top of regex matcher

91 points by justinucd 6y ago

Thorrez 6y ago
> Another practical usage I've heard: match "string" or 'string', but not "string'. You don't need backreferences for that: '[^']*'|"[^"]*"
- throw681158 6y ago
  Won't work if you're already in a string, or if there are escaped quotes in the string. Also won't work if you have two or more double quoted strings that both contain an apostrophe.
  - Leszek 6y ago
    Escaping isn't an intrinsic property of all quoted strings (e.g. single quoted strings in bash), but even so one can work around them without backreferences, by searching for anything that's not a quote or a backslash, _or_ any escaped character: /"([^"\\]|\\.)*"/ Now double that up with a single quote version if you wish. What you can't match without backreferences, however, is strings with customisable terminators, e.g. the behaviour in sed that whatever character you use after `s` is the regex terminator (it doesn't have to be `/`), or raw strings in C++.
  - Thorrez 6y ago
    Backreferences don't really help with those problems. > Won't work if you're already in a string This doesn't make sense. How can you search for a string if you're already in a string? I can't think of a realistic situation where that would be useful or even really possible. > or if there are escaped quotes in the string. Solvable: '(\'|\\|[^\'])*'|"(\"|\\|[^\"])*" > Also won't work if you have two or more double quoted strings that both contain an apostrophe. The regex in my previous comment already solves that. See: https://repl.it/repls/SolidCapitalProgram https://repl.it/repls/SolidCapitalProgram
    - sacado2 6y ago
      > This doesn't make sense. How can you search for a string if you're already in a string? I can't think of a realistic situation where that would be useful or even really possible. query = "select * from table where name like \"%foo\""
      - Thorrez 6y ago
        Interesting. Although in that situation I think it would be easier to find the outer string, then unescape it, then find the inner string. Although if you want to do it with pure regex, it can be done without backreferences too, although it would be exponentially large as you get more and more levels of nesting, whereas with backreferences I think it would only get quadratically large.
    - throw681158 6y ago
      Re: already in a string, one of the primary uses of regex is to search from point in a text editor. So, cursor is in a string and you want to find the next string. Regex won't work on its own, you generally need more semantic information to differentiate opening & closing quotes (unless you can use local context from that particular language to infer it). But more broadly, any situation where you search from a non-zero index has this problem. I'm surprised your example works in Python. Is that a property of Python's parser, or all regex matchers?
      - Thorrez 6y ago
        > Regex won't work on its own, you generally need more semantic information Yeah, I agree. My point was that regex won't work, regardless of if you have backreferences or not. So backreferences won't help. > But more broadly, any situation where you search from a non-zero index has this problem. I'm not sure I understand that. A lot of regex libraries let you specify a start index. It won't take into account data from before the start index though (regex doesn't really do that, regardless of backreferences). If your regex library doesn't support passing in a start index, you can just take a substring starting at that index, then search the substring. I don't think Python is really special. Python's findall() is just a convenience function that does a loop finding a match, then finding another match that starts after the first match, etc. Most languages provide a way to find the end point of the most recent match, and then you can just write the loop yourself to start the next search at that point.
  - bottled_poe 6y ago
    That wasn’t specified in the requirements
    - throw681158 6y ago
      Good point.
  - hansvm 6y ago
    As some other replies pointed out, there are straightforward modifications to handle all those scenarios if those are your requirements instead. A place where regex _does_ fail is in arbitrarily nested string interpolations (the key being _arbitrary_ nesting because with enough time anyone can come up with a convoluted enough regex to handle a bounded degree of recursion).
- quickthrower2 6y ago
  At some point you'd want to pull out a parser. Maybe 1 more step after this point.
- lifthrasiir 6y ago
  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.
  - hansvm 6y ago
    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.
    - lifthrasiir 6y ago
      Of course, but you are out of luck in terms of complexity. (Colloquial) regular expressions lack any kind of abstractions.
      - hansvm 6y ago
        Absolutely. I don't for a moment think they're the right tool for the job. They are fairly powerful in terms of what they're capable of parsing however (not enough for an arbitrary html document, but enough to handle the hairier situations in this thread that people thought they couldn't), and that does mean that a regular expression generator can handle all of those situations as well and potentially be much more readable. If I found myself writing code like this I'd still want to reach for a better parsing technology, but you can use other languages to add abstractions to regex. Here's a Python3.6+ example assuming any desired backslashes have already been applied: '|'.join(rf'{a}[^{b}]*{b}' for a,b in pairs)
awirth 6y ago
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?
- praptak 6y ago
  I don't think so. Usually you can tell from the context: # math and/or computer science texts? It's the regular ones. # pretty much elsewhere? It's the extended ones. # threads about parsing HTML with regular expressions? People using both and insisting their version is the only correct one.
- zokier 6y ago
  I think Raku (neé Perl 6) has been spearheading that distinction https://docs.raku.org/language/regexes https://docs.raku.org/language/regexes (see the intro paragraph)
- chubot 6y ago
  I wouldn't say so, but I use the term "regular language" if I mean the mathematical concept.
  - robinhouston 6y ago
    I don’t think it’s pedantic to say that a regular language is not the same thing as a regular expression. The difference between syntax and semantics is real and important.
    - chubot 6y ago
      (late reply) Right that's what I'm saying. Who said it was pedantic? :)
  - gnulinux 6y ago
    But a "regular language" is not the same as "regular expression" as mathematical concepts.
sacado2 6y ago
One of the cool features of SAT problems is that they always terminate (if you're patient enough). Aren't regex, especially with backreferences, Turing-complete though? If so, they could be caught in an infinite loop, meaning they are more general than the SAT problem.
- dmichulke 6y ago
  Programming languages are more general than the problems they solve. (= feature, not bug) Still, yes, you can mess up your "add 1 to the input" program and make it run infinitely.
  - sacado2 6y ago
    Yeah, I meant it the other way, if those regexps are Turing-complete, not all of them have an equivalent CNF representation, contrarily to what the article seems to state in its first paragraph (and title). That being said, regexps were not initially meant to be "programming languages", so I'm not sure about the "feature, not bug" part. I'd rather have a notation that would let me solve, for instance, the "HTML tag matching" problem and would be guaranteed to always terminate, than one that also lets me implement Conway's game of life.
punnerud 6y ago
time python3 solver.py fred.cnf Took 9min and 10seconds on RPi 3 running Ubuntu 20.04. Consuming 100% CPU and 1% RAM (1024MB).
- nurettin 6y ago
  This is actually amazing. My python programs rarely run at 100% cpu, whereas C++ binaries are usually up there. Always thought python's inefficiency causes the drop in cpu utilization.
  - ygra 6y ago
    Python's regex implementation is probably not written in Python, so while it's trying to match, no Python code runs; it's all /C(++)?/.
  - nromiun 6y ago
    I don't know about how efficient it is but I have always been able to peg all cores with the multiprocessing module. Even something useless like "x * x" is more then enough for 800%.
PaulHoule 6y ago
That is quite literally a formal proof that "regex+backreferences" is NP-complete, since SAT is the index NP-complete problem.
- pradn 6y ago
  I assume this result is already known in the literature?
  - klyrs 6y ago
    This doesn't show a date but archive.org has snapshots dating back to 2001 https://perl.plover.com/NPC/ https://perl.plover.com/NPC/
- gbacon 6y ago
  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.
  - dtech 6y ago
    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
- simonebrunozzi 6y ago
  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.
klyrs 6y ago
That "popcnt1" is also known as a 1-hot constraint. https://en.m.wikipedia.org/wiki/One-hot https://en.m.wikipedia.org/wiki/One-hot

91 points by justinucd 6y ago

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

throw681158 6y ago
Won't work if you're already in a string, or if there are escaped quotes in the string. Also won't work if you have two or more double quoted strings that both contain an apostrophe.
- Leszek 6y ago
  Escaping isn't an intrinsic property of all quoted strings (e.g. single quoted strings in bash), but even so one can work around them without backreferences, by searching for anything that's not a quote or a backslash, _or_ any escaped character: /"([^"\\]|\\.)*"/ Now double that up with a single quote version if you wish. What you can't match without backreferences, however, is strings with customisable terminators, e.g. the behaviour in sed that whatever character you use after `s` is the regex terminator (it doesn't have to be `/`), or raw strings in C++.
- Thorrez 6y ago
  Backreferences don't really help with those problems. > Won't work if you're already in a string This doesn't make sense. How can you search for a string if you're already in a string? I can't think of a realistic situation where that would be useful or even really possible. > or if there are escaped quotes in the string. Solvable: '(\'|\\|[^\'])*'|"(\"|\\|[^\"])*" > Also won't work if you have two or more double quoted strings that both contain an apostrophe. The regex in my previous comment already solves that. See: https://repl.it/repls/SolidCapitalProgram https://repl.it/repls/SolidCapitalProgram
  - sacado2 6y ago
    > This doesn't make sense. How can you search for a string if you're already in a string? I can't think of a realistic situation where that would be useful or even really possible. query = "select * from table where name like \"%foo\""
    - Thorrez 6y ago
      Interesting. Although in that situation I think it would be easier to find the outer string, then unescape it, then find the inner string. Although if you want to do it with pure regex, it can be done without backreferences too, although it would be exponentially large as you get more and more levels of nesting, whereas with backreferences I think it would only get quadratically large.
  - throw681158 6y ago
    Re: already in a string, one of the primary uses of regex is to search from point in a text editor. So, cursor is in a string and you want to find the next string. Regex won't work on its own, you generally need more semantic information to differentiate opening & closing quotes (unless you can use local context from that particular language to infer it). But more broadly, any situation where you search from a non-zero index has this problem. I'm surprised your example works in Python. Is that a property of Python's parser, or all regex matchers?
    - Thorrez 6y ago
      > Regex won't work on its own, you generally need more semantic information Yeah, I agree. My point was that regex won't work, regardless of if you have backreferences or not. So backreferences won't help. > But more broadly, any situation where you search from a non-zero index has this problem. I'm not sure I understand that. A lot of regex libraries let you specify a start index. It won't take into account data from before the start index though (regex doesn't really do that, regardless of backreferences). If your regex library doesn't support passing in a start index, you can just take a substring starting at that index, then search the substring. I don't think Python is really special. Python's findall() is just a convenience function that does a loop finding a match, then finding another match that starts after the first match, etc. Most languages provide a way to find the end point of the most recent match, and then you can just write the loop yourself to start the next search at that point.
- bottled_poe 6y ago
  That wasn’t specified in the requirements
  - throw681158 6y ago
    Good point.
- hansvm 6y ago
  As some other replies pointed out, there are straightforward modifications to handle all those scenarios if those are your requirements instead. A place where regex _does_ fail is in arbitrarily nested string interpolations (the key being _arbitrary_ nesting because with enough time anyone can come up with a convoluted enough regex to handle a bounded degree of recursion).
quickthrower2 6y ago
At some point you'd want to pull out a parser. Maybe 1 more step after this point.
lifthrasiir 6y ago
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.
- hansvm 6y ago
  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.
  - lifthrasiir 6y ago
    Of course, but you are out of luck in terms of complexity. (Colloquial) regular expressions lack any kind of abstractions.
    - hansvm 6y ago
      Absolutely. I don't for a moment think they're the right tool for the job. They are fairly powerful in terms of what they're capable of parsing however (not enough for an arbitrary html document, but enough to handle the hairier situations in this thread that people thought they couldn't), and that does mean that a regular expression generator can handle all of those situations as well and potentially be much more readable. If I found myself writing code like this I'd still want to reach for a better parsing technology, but you can use other languages to add abstractions to regex. Here's a Python3.6+ example assuming any desired backslashes have already been applied: '|'.join(rf'{a}[^{b}]*{b}' for a,b in pairs)

awirth 6y ago

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?

praptak 6y ago
I don't think so. Usually you can tell from the context: # math and/or computer science texts? It's the regular ones. # pretty much elsewhere? It's the extended ones. # threads about parsing HTML with regular expressions? People using both and insisting their version is the only correct one.
zokier 6y ago
I think Raku (neé Perl 6) has been spearheading that distinction https://docs.raku.org/language/regexes https://docs.raku.org/language/regexes (see the intro paragraph)
chubot 6y ago
I wouldn't say so, but I use the term "regular language" if I mean the mathematical concept.
- robinhouston 6y ago
  I don’t think it’s pedantic to say that a regular language is not the same thing as a regular expression. The difference between syntax and semantics is real and important.
  - chubot 6y ago
    (late reply) Right that's what I'm saying. Who said it was pedantic? :)
- gnulinux 6y ago
  But a "regular language" is not the same as "regular expression" as mathematical concepts.

sacado2 6y ago

One of the cool features of SAT problems is that they always terminate (if you're patient enough). Aren't regex, especially with backreferences, Turing-complete though? If so, they could be caught in an infinite loop, meaning they are more general than the SAT problem.

dmichulke 6y ago
Programming languages are more general than the problems they solve. (= feature, not bug) Still, yes, you can mess up your "add 1 to the input" program and make it run infinitely.
- sacado2 6y ago
  Yeah, I meant it the other way, if those regexps are Turing-complete, not all of them have an equivalent CNF representation, contrarily to what the article seems to state in its first paragraph (and title). That being said, regexps were not initially meant to be "programming languages", so I'm not sure about the "feature, not bug" part. I'd rather have a notation that would let me solve, for instance, the "HTML tag matching" problem and would be guaranteed to always terminate, than one that also lets me implement Conway's game of life.

punnerud 6y ago

time python3 solver.py fred.cnf Took 9min and 10seconds on RPi 3 running Ubuntu 20.04. Consuming 100% CPU and 1% RAM (1024MB).

nurettin 6y ago
This is actually amazing. My python programs rarely run at 100% cpu, whereas C++ binaries are usually up there. Always thought python's inefficiency causes the drop in cpu utilization.
- ygra 6y ago
  Python's regex implementation is probably not written in Python, so while it's trying to match, no Python code runs; it's all /C(++)?/.
- nromiun 6y ago
  I don't know about how efficient it is but I have always been able to peg all cores with the multiprocessing module. Even something useless like "x * x" is more then enough for 800%.

PaulHoule 6y ago

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

pradn 6y ago
I assume this result is already known in the literature?
- klyrs 6y ago
  This doesn't show a date but archive.org has snapshots dating back to 2001 https://perl.plover.com/NPC/ https://perl.plover.com/NPC/
gbacon 6y ago
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.
- dtech 6y ago
  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
simonebrunozzi 6y ago
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.

klyrs 6y ago

That "popcnt1" is also known as a 1-hot constraint. https://en.m.wikipedia.org/wiki/One-hot https://en.m.wikipedia.org/wiki/One-hot