← Back to context

Comment by Darmani

10 years ago

Hi, I'm a researcher in program synthesis.

I think you meant to say "NP-hard" . And indeed, there are many program synthesis problems which are NP-hard, 2EXP-complete, or undecidable. But there are also many program synthesis algorithms which are polynomial time. If you use Windows, there might even be one running on your computer.

We've been studying this problem for close to 50 years. I think you see the basic problems, but we know a lot about what to do about them.

11 comments

Darmani

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

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

      3 replies →