Comment by 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...

4 comments

Darmani

Reply
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.

  • mortehu  10 years ago

    The satisfiability problem doesn't require that you provide the solution, only that you determine whether or not a solution exists. So you'd end up with a primality check, which is known to be in P:

    https://en.wikipedia.org/wiki/AKS_primality_test

    • tgflynn  10 years ago

      It's not a primality test. A primality test determines whether or not a single given integer is prime.

      The circuit I described checks that the product of two arbitrary input integers is a specific known integer.

      By solving the decision problem for each bit independently you can determine all bits of the 2 input integers and hence factor the known target.

      1 reply →