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

donsbot.wordpress.com

35 points·unignorant··7 comments

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.

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.

I believe they're also used for verifying potential new compiler optimizations: http://blog.regehr.org/archives/247

Check out the SAT competition for state of the art solvers: http://www.satcompetition.org/

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.

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?

If you vote it up, won't it show up on your "saved threads"?

[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, for example: 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?

Reply on news.ycombinator.com