3 ms·

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

by Darmani 10y 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-architects.html https://homes.cs.washington.edu/~bornholt/post/synthesis-for...

tgflynn 10y 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 10y 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 https://en.wikipedia.org/wiki/AKS_primality_test
  - tgflynn 10y 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.
    - mortehu 10y ago
      Neat. I wasn't aware of the trick of peeling off a bit at a time.

by Darmani 10y ago

tgflynn 10y 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 10y 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 https://en.wikipedia.org/wiki/AKS_primality_test
- tgflynn 10y 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.
  - mortehu 10y ago
    Neat. I wasn't aware of the trick of peeling off a bit at a time.