← Back to context

Comment by lossolo

10 years ago

Indeed, NP-hard (edited it now). Can you expand on "we know a lot about what to do about them" ? Thanks.

7 comments

lossolo

Reply
Darmani  10 years ago

So first, NP-hard isn't much of a barrier. We often like to call it "NP-easy." Or, going a step further:

"PSPACE-complete is great news. It's the new poly-time." -- Moshe Vardi

SAT solvers are very fast. It's worst-case exponential, sure, but it's hard to find that worst-case. I just heard at lunch yesterday that MaxSAT is now also easily handling problems with millions of variables. I think I'd be scared if I found out what the record was for normal SAT.

So, how do you actually do synthesis? I could talk for quite a while about it.....but here's a pretty good intro-article: https://homes.cs.washington.edu/~bornholt/post/synthesis-for...

  • tgflynn  10 years ago

    It's worst-case exponential, sure, but it's hard to find that worst-case.

    It's not that hard. Just generate a boolean circuit for the multiplication of 2 64 bit prime numbers and convert the circuit to a 3-SAT formula. I doubt any current SAT solver can solve that problem. If you could do it for 1024 bit primes a lot of cryptography would be toast.

    EDIT: To be a bit more clear I mean that the circuit takes two n-bit numbers, multiplies them then compares the result to some known product of 2 primes. So by solving this circuit you factor the known integer.

    EDIT2: Doesn't solving MaxSAT exactly imply that you can also solve SAT ? If there's a SAT solver that can handle million variable instances "easily" that's something I'd be really interested in hearing more about.