4 ms·

Not so long ago, we’d say “That’s an NP-complete problem” with the implication that it was hopeless to expect an efficient solution. Now (to exaggerate a little

Not so long ago, we’d say “That’s an NP-complete problem” with the implication that it was hopeless to expect an efficient solution. Now (to exaggerate a little) it’s more like a sign that there probably is an efficient solution using some powerful solver. LKH is a lovely piece of work. I used it a couple of years ago to find a counterexample to an unimportant but fairly long-standing conjecture in combinatorics[0], and the list of scientific applications[1] is impressively diverse. The best SMT solvers are also hugely impressive. Z3 has an excellent interactive tutorial and online solver.[2] [0] https://arxiv.org/abs/1408.5108 https://arxiv.org/abs/1408.5108 [1] http://webhotel4.ruc.dk/~keld/research/LKH/ScientificApplications.html http://webhotel4.ruc.dk/~keld/research/LKH/ScientificApplica... [2] http://rise4fun.com/z3/tutorial http://rise4fun.com/z3/tutorial

preygel 10y ago
Absolutely! Not to mention the often impressive performance of "general" MIP solvers. It is only a shame that the best ones there are commercial (Gurobi followed by Cplex). That said, Cbc is lovely in a wide range of cases, and is open-source.
botw 10y ago
I always thought "NP-complete/NP-hard" metaphor only meaningful in theoretical work. In practice, it does not make much sense in guiding what/how the real world problem is to be solved.
- robinhouston 10y ago
  I don't know. I find it useful in practice. Apart from anything else it means there's (probably) no point looking for an exact polynomial-time algorithm, which can save a lot of wasted effort. But it also gives useful clues about what sort of algorithmic approaches might be useful, and allows you to relate your problem to a huge amount of existing research. It's really basic taxonomy: what sort of problem are we dealing with? If you don't know that, how could you even begin to design a reasonable algorithm for it?
  - botw 10y ago
    Maybe you are heavily on huge algorithmic work. In practice, most algorithms are polynomial-time, and we are looking for under-polynomial-time alternative - log(n). For exponential-time, we are just looking for an approximate alternative.
Retr0spectrum 10y ago
Z3 (and other constraint solvers) are very impressive. The most interesting application I've seen is in binary exploitation and reverse-engineering through symbolic execution. Angr is a very popular framework which allows for symbolic execution of binaries using Z3 as a backend. It's made a whole class of common CTF challenges almost trivial: https://docs.angr.io/docs/examples.html https://docs.angr.io/docs/examples.html

preygel 10y ago

Absolutely! Not to mention the often impressive performance of "general" MIP solvers. It is only a shame that the best ones there are commercial (Gurobi followed by Cplex). That said, Cbc is lovely in a wide range of cases, and is open-source.

botw 10y ago

I always thought "NP-complete/NP-hard" metaphor only meaningful in theoretical work. In practice, it does not make much sense in guiding what/how the real world problem is to be solved.

robinhouston 10y ago
I don't know. I find it useful in practice. Apart from anything else it means there's (probably) no point looking for an exact polynomial-time algorithm, which can save a lot of wasted effort. But it also gives useful clues about what sort of algorithmic approaches might be useful, and allows you to relate your problem to a huge amount of existing research. It's really basic taxonomy: what sort of problem are we dealing with? If you don't know that, how could you even begin to design a reasonable algorithm for it?
- botw 10y ago
  Maybe you are heavily on huge algorithmic work. In practice, most algorithms are polynomial-time, and we are looking for under-polynomial-time alternative - log(n). For exponential-time, we are just looking for an approximate alternative.

Retr0spectrum 10y ago

Z3 (and other constraint solvers) are very impressive. The most interesting application I've seen is in binary exploitation and reverse-engineering through symbolic execution. Angr is a very popular framework which allows for symbolic execution of binaries using Z3 as a backend. It's made a whole class of common CTF challenges almost trivial: https://docs.angr.io/docs/examples.html https://docs.angr.io/docs/examples.html