4 ms·

Painless NP-complete problems: an embedded DSL for SMT solving

35 points by unignorant 16y ago

Bootvis 16y ago
I have nothing insightful to say about this topic but I'll comment anyway and ask: Is there a way to bookmark threads without commenting?
- deleted 16y ago
  [deleted]
- tptacek 16y ago
  If you vote it up, won't it show up on your "saved threads"?
- dexen 16y ago
  [off-topic as well] There is that `saved stories' link in your profiles, that lists all the stories you upvoted. It links to http://news.ycombinator.com/saved?id=YOUR_NICKNAME http://news.ycombinator.com/saved?id=YOUR_NICKNAME, for example: http://news.ycombinator.com/saved?id=Bootvis http://news.ycombinator.com/saved?id=Bootvis is the link for you. I believe the actual intent of ``upvote == bookmark'' was to encourage users to upvote mostly stuff they actually believe worthy returning to, or saving for friends. Somebody out there correct me on that belief, please?
tptacek 16y ago
Anybody on HN actually doing a product that needs sat solvers? They're currently in vogue in software security; they solve search and reachability problems on modeled instruction streams.
- long 16y ago
  It's not a product, but I've been doing some research that involves Bayesian inference. One recently developed technique (called weighted model counting) converts inference problems into SAT problems and the group I work with has been thinking about implementing this technique. A lot of really smart people have worked on SAT, so a viable start to solving an NP-complete problem (e.g. traveling salesman in airline scheduling) is reduction to SAT.
- mayank 16y ago
  I believe they're also used for verifying potential new compiler optimizations: http://blog.regehr.org/archives/247 http://blog.regehr.org/archives/247 Check out the SAT competition for state of the art solvers: http://www.satcompetition.org/ http://www.satcompetition.org/
  - jules 16y ago
    They can also be used to do the actual optimizations. For example most formulations of the register allocation problem are NP-complete. SMT formulas can be used as a very powerful abstract domain in abstract interpretation.

35 points by unignorant 16y ago

I have nothing insightful to say about this topic but I'll comment anyway and ask: Is there a way to bookmark threads without commenting?

deleted 16y ago
[deleted]
tptacek 16y ago
If you vote it up, won't it show up on your "saved threads"?
dexen 16y ago
[off-topic as well] There is that `saved stories' link in your profiles, that lists all the stories you upvoted. It links to http://news.ycombinator.com/saved?id=YOUR_NICKNAME http://news.ycombinator.com/saved?id=YOUR_NICKNAME, for example: http://news.ycombinator.com/saved?id=Bootvis http://news.ycombinator.com/saved?id=Bootvis is the link for you. I believe the actual intent of ``upvote == bookmark'' was to encourage users to upvote mostly stuff they actually believe worthy returning to, or saving for friends. Somebody out there correct me on that belief, please?

tptacek 16y ago

Anybody on HN actually doing a product that needs sat solvers? They're currently in vogue in software security; they solve search and reachability problems on modeled instruction streams.

long 16y ago
It's not a product, but I've been doing some research that involves Bayesian inference. One recently developed technique (called weighted model counting) converts inference problems into SAT problems and the group I work with has been thinking about implementing this technique. A lot of really smart people have worked on SAT, so a viable start to solving an NP-complete problem (e.g. traveling salesman in airline scheduling) is reduction to SAT.
mayank 16y ago
I believe they're also used for verifying potential new compiler optimizations: http://blog.regehr.org/archives/247 http://blog.regehr.org/archives/247 Check out the SAT competition for state of the art solvers: http://www.satcompetition.org/ http://www.satcompetition.org/
- jules 16y ago
  They can also be used to do the actual optimizations. For example most formulations of the register allocation problem are NP-complete. SMT formulas can be used as a very powerful abstract domain in abstract interpretation.