4 ms·

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

by lossolo 10y ago

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.
deleted 10y ago
[deleted]
hcs 10y ago
Relatedly, even though Boolean Satisfiability [1] is NP-complete, there are SAT solvers that can solve huge practical instances fast enough to be useful. 1: https://en.wikipedia.org/wiki/Boolean_satisfiability_problem https://en.wikipedia.org/wiki/Boolean_satisfiability_problem

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

by lossolo 10y ago

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

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.

deleted 10y ago

[deleted]

hcs 10y ago

Relatedly, even though Boolean Satisfiability [1] is NP-complete, there are SAT solvers that can solve huge practical instances fast enough to be useful. 1: https://en.wikipedia.org/wiki/Boolean_satisfiability_problem https://en.wikipedia.org/wiki/Boolean_satisfiability_problem