4 ms·

Any suggestions for a good parallel open source SMT solver? It seems to me like contests are full of documentation-less entries that are setup to just run the

by nullc 2y ago

Any suggestions for a good parallel open source SMT solver? It seems to me like contests are full of documentation-less entries that are setup to just run the contests and may or may not be generally usable.

philzook 2y ago
https://github.com/domschrei/mallob https://github.com/domschrei/mallob I've seen talks by AWS where they claim that distributed SAT solving is very effective. Do you need it to be parallel or just fast? My impression is that at the single machine level, it's hard to beat kissat and the CPU or GPU parallelism is not that useful. https://github.com/arminbiere/kissat https://github.com/arminbiere/kissat
almostgotcaught 2y ago
SAT/SMT isn't parallelizable. If it were it would be in P and you'd have P=NP.
- 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.

by nullc 2y ago

philzook 2y ago

https://github.com/domschrei/mallob https://github.com/domschrei/mallob I've seen talks by AWS where they claim that distributed SAT solving is very effective. Do you need it to be parallel or just fast? My impression is that at the single machine level, it's hard to beat kissat and the CPU or GPU parallelism is not that useful. https://github.com/arminbiere/kissat https://github.com/arminbiere/kissat

almostgotcaught 2y ago

SAT/SMT isn't parallelizable. If it were it would be in P and you'd have P=NP.

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.