3 ms·

That's patently false. For example, you can fix some variables on different instances, and run the solve with those variables fixed. This doesn't result in re

by nullc 2y ago

That's patently false. For example, you can fix some variables on different instances, and run the solve with those variables fixed. This doesn't result in really good work distribution, but it's a toy example.

almostgotcaught 2y ago
> That's patently false. Then you should file a patent? Or at least email Clay Institute about it because I believe (I'm not sure) there's a substantial prize associated with proving P=NP. > For example, you can fix some variables on different instances You can also parallelize stock picking by just picking stocks at random across multiple portfolios. Do you think I should patent this approach as a winning strategy?
- NooneAtAll3 2y ago
  first of all, it's not P=NP - it would be NC=NP. If you nitpick, then at least do it right and secondly, when "normal bloody people" talk about parallelizing, we don't mean exponential speedup - we mean using 4 cores in hopes of getting 3x time shrinking and cube'n'conquer does exactly that - and have been the standard tool in SAT solving for forever
  - almostgotcaught 2y ago
    NC is a subset is P. > mean using 4 cores in hopes of getting 3x time shrinking I've already been over this: reducing 2^N by a factor of 3 is useless.
    - NooneAtAll3 2y ago
      > I've already been over this: reducing 2^N by a factor of 3 is useless. and here you're again showing your absence of practice and you being too much into theory it's not useless if it transforms day computation into work-shift one because actual people aren't working on theoretical infinite problems - people need solving specific examples they are stuck at you sound like you'll enjoy working with galactic algorithms - too bad inter-universal beings aren't hiring right now
- nullc 2y ago
  It may well be that for some worst case instances of SAT/SMT that there is no parallel algorithm to solve them faster than a sequential algorithm unless P==NP. But most people who are not complexity theorists (or perhaps cryptographers) are not generally interested in worst case instances, but are instead interested in solving practical problems which are often not (or even-- are practically never) worst case instances. My own experience w/ real SMT problems is that I can usually home-brew a fair amount of parallelism by fixing some variables and then solving the derived problems w/ Z3 on each core. But the result often has fairly poor load distribution (e.g. some threads finish long before others), so it could obviously be done better by software the changes the variable its parallel on and how it distributes those variables adaptively as it goes.
  - almostgotcaught 2y ago
    > But the result often has fairly poor load distribution (e.g. some threads finish long before others), so it could obviously be done better by software the changes the variable its parallel on and how it distributes those variables adaptively as it goes. It's astonishing to me that you're staring my point straight in the face and still not getting it. Let me restate in terms of portfolios: If I distribute my stock picks across many portfolios, without an oracle to tell me how to distribute them, some of the portfolios will perform poorly and some will perform well, but on average they will perform as if I just had a single portfolio.
    - nullc 2y ago
      I do wonder how we're talking past each other. Usually when I use an SMT solver I'm interested in finding a satisfying solution. Breaking up the problem on some variable the solver would search across multiple processors can improve the wall-time until finding one. I doubt I'm following your metaphors/allusions, but the parallel may be that you're only hoping for any portfolio to have excess performance, and not the sum total.
      - deleted 2y ago
        [deleted]

by nullc 2y ago

almostgotcaught 2y ago

> That's patently false. Then you should file a patent? Or at least email Clay Institute about it because I believe (I'm not sure) there's a substantial prize associated with proving P=NP. > For example, you can fix some variables on different instances You can also parallelize stock picking by just picking stocks at random across multiple portfolios. Do you think I should patent this approach as a winning strategy?

NooneAtAll3 2y ago
first of all, it's not P=NP - it would be NC=NP. If you nitpick, then at least do it right and secondly, when "normal bloody people" talk about parallelizing, we don't mean exponential speedup - we mean using 4 cores in hopes of getting 3x time shrinking and cube'n'conquer does exactly that - and have been the standard tool in SAT solving for forever
- almostgotcaught 2y ago
  NC is a subset is P. > mean using 4 cores in hopes of getting 3x time shrinking I've already been over this: reducing 2^N by a factor of 3 is useless.
  - NooneAtAll3 2y ago
    > I've already been over this: reducing 2^N by a factor of 3 is useless. and here you're again showing your absence of practice and you being too much into theory it's not useless if it transforms day computation into work-shift one because actual people aren't working on theoretical infinite problems - people need solving specific examples they are stuck at you sound like you'll enjoy working with galactic algorithms - too bad inter-universal beings aren't hiring right now
nullc 2y ago
It may well be that for some worst case instances of SAT/SMT that there is no parallel algorithm to solve them faster than a sequential algorithm unless P==NP. But most people who are not complexity theorists (or perhaps cryptographers) are not generally interested in worst case instances, but are instead interested in solving practical problems which are often not (or even-- are practically never) worst case instances. My own experience w/ real SMT problems is that I can usually home-brew a fair amount of parallelism by fixing some variables and then solving the derived problems w/ Z3 on each core. But the result often has fairly poor load distribution (e.g. some threads finish long before others), so it could obviously be done better by software the changes the variable its parallel on and how it distributes those variables adaptively as it goes.
- almostgotcaught 2y ago
  > But the result often has fairly poor load distribution (e.g. some threads finish long before others), so it could obviously be done better by software the changes the variable its parallel on and how it distributes those variables adaptively as it goes. It's astonishing to me that you're staring my point straight in the face and still not getting it. Let me restate in terms of portfolios: If I distribute my stock picks across many portfolios, without an oracle to tell me how to distribute them, some of the portfolios will perform poorly and some will perform well, but on average they will perform as if I just had a single portfolio.
  - nullc 2y ago
    I do wonder how we're talking past each other. Usually when I use an SMT solver I'm interested in finding a satisfying solution. Breaking up the problem on some variable the solver would search across multiple processors can improve the wall-time until finding one. I doubt I'm following your metaphors/allusions, but the parallel may be that you're only hoping for any portfolio to have excess performance, and not the sum total.
    - deleted 2y ago
      [deleted]