TE
TechEcho
Home24h TopNewestBestAskShowJobs
GitHubTwitter
Home

TechEcho

A tech news platform built with Next.js, providing global tech news and discussions.

GitHubTwitter

Home

HomeNewestBestAskShowJobs

Resources

HackerNews APIOriginal HackerNewsNext.js

© 2025 TechEcho. All rights reserved.

Sat solver on top of regex matcher

91 pointsby justinucdalmost 5 years ago

6 comments

Thorrezalmost 5 years ago
&gt; Another practical usage I&#x27;ve heard: match &quot;string&quot; or &#x27;string&#x27;, but not &quot;string&#x27;.<p>You don&#x27;t need backreferences for that:<p><pre><code> &#x27;[^&#x27;]*&#x27;|&quot;[^&quot;]*&quot;</code></pre>
评论 #23598550 未加载
评论 #23597828 未加载
评论 #23597938 未加载
PaulHoulealmost 5 years ago
That is quite literally a formal proof that &quot;regex+backreferences&quot; is NP-complete, since SAT is the index NP-complete problem.
评论 #23600941 未加载
评论 #23600431 未加载
评论 #23600486 未加载
awirthalmost 5 years ago
This reduction is really cool. I love reductions like this.<p>Is there a general consensus to use &quot;regular expression&quot; to refer to the actual regular ones and &quot;regex&quot; to refer to the non-regular variants?
评论 #23598035 未加载
评论 #23598639 未加载
评论 #23609464 未加载
评论 #23598078 未加载
评论 #23597843 未加载
评论 #23600353 未加载
评论 #23600187 未加载
sacado2almost 5 years ago
One of the cool features of SAT problems is that they always terminate (if you&#x27;re patient enough). Aren&#x27;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.
评论 #23599867 未加载
klyrsalmost 5 years ago
That &quot;popcnt1&quot; is also known as a 1-hot constraint.<p><a href="https:&#x2F;&#x2F;en.m.wikipedia.org&#x2F;wiki&#x2F;One-hot" rel="nofollow">https:&#x2F;&#x2F;en.m.wikipedia.org&#x2F;wiki&#x2F;One-hot</a>
punnerudalmost 5 years ago
time python3 solver.py fred.cnf<p>Took 9min and 10seconds on RPi 3 running Ubuntu 20.04. Consuming 100% CPU and 1% RAM (1024MB).
评论 #23601921 未加载