4 ms·

It's not just GPU. There are not even good multicore SAT solvers. State of the art SAT algorithms are serial and they don't parallelize.

bmc7505 3y ago
I was thinking there might be some theoretical barrier to parallelization, e.g., maybe naturally-arising SAT instances have poor empirical scaling constants [1], so sequential solvers with good branch heuristics are pretty close to optimal. There are some portfolio solvers (e.g., [2]) that have shown modest, but not dramatic speedups. Or maybe we just haven't tried hard enough. [1]: https://en.wikipedia.org/wiki/NC_(complexity) https://en.wikipedia.org/wiki/NC_(complexity) [2]: https://baldur.iti.kit.edu/hordesat/files/horde.pdf https://baldur.iti.kit.edu/hordesat/files/horde.pdf
js8 3y ago
You could reduce to 2XSAT and presolve the linear portion. That would paralelize. I think people are not doing it because they are not aware of the reduction.
- adrianN 3y ago
  You'd think that the handful of people who devote a significant fraction of their time to writing SAT solver would be aware of such simple tricks and there might be other reasons why your idea isn't being applied.
  - js8 3y ago
    I would think so too, but I couldn't find this particular trick anywhere. Anyway, I believe it's similar to LP - we still use simplex method in practice, despite the fact that LP has a polynomial algorithm. What likely happens in SAT is even though there actually is (as I believe) a nice polynomial algorithm on the order of O(n^4) or so (which involves repeated solving of linear systems), the CDCL still wins in practical problems simply because in most cases, the upfront cost of solving the equations is higher than trying to find a first solution. However, not all hope is lost. You could actually presolve a more general problem, and then just rely on propagation to deal with a more specific instance. For instance, for integer factorization, you could presolve a general system for integers of certain bit size, and then if you wanted to factorize a specific integer, you would just plugin constants into the presolved instance. That would eliminate most of the upfront cost and bring it on par with CDCL. Unfortunately, DIMACS is not all that good format to represent SAT, because it is not composable like this - it doesn't allow for representation of presolved instances. But composability might be a win for a different types of algorithms, which do presolving.
    - adrianN 3y ago
      If you know a O(n^4) algorithm for SAT, I'm sure a couple of people would be interested in your paper.
      - js8 3y ago
        I don't really know the exact algorithm yet, but I have a strong feeling it is possible based on what I see. There are like 3 major steps in the strategy, first one is 2XSAT reduction, second is a proof of refutation completeness (in particular, a form of deduction theorem) of a certain logic that models 2XSAT class, and the last one is polynomial-sized representation of all true statements in that logic (which uses n sets of linear equations, and from that follows the complexity of O(n^4)). The 2XSAT reduction is 100% correct (I have been using it to solve small integer factoring problems), the deduction theorem proof still has a small flaw which I think is fixable, and the third part is an ongoing research which is trucking along. I will get there eventually, but if more people would be looking at this approach, then we (humanity) could arrive there faster, that's all.
        bmc7505 3y ago
        Just gotta keep on trucking. Either way, I would be interested in seeing how the 2XSAT reduction works. Don't get discouraged!
thesz 3y ago
ManySAT: http://www.cril.univ-artois.fr/~jabbour/manysat.htm http://www.cril.univ-artois.fr/~jabbour/manysat.htm It shares short conflict clauses between parallel solvers and achieves superlinear speedup in some cases, e.g., 4 parallel solvers solve faster than one forth of the single solver soolution time. Short conflict clauses are rare so there is little communication between solvers required. CryptoMiniSAT: https://github.com/msoos/cryptominisat https://github.com/msoos/cryptominisat Author's goal to have solver that is good in computing range from single CPU up to cluster. Judging from CryptoMiniSAT successes, he has mostly reached the goal.

bmc7505 3y ago

I was thinking there might be some theoretical barrier to parallelization, e.g., maybe naturally-arising SAT instances have poor empirical scaling constants [1], so sequential solvers with good branch heuristics are pretty close to optimal. There are some portfolio solvers (e.g., [2]) that have shown modest, but not dramatic speedups. Or maybe we just haven't tried hard enough. [1]: https://en.wikipedia.org/wiki/NC_(complexity) https://en.wikipedia.org/wiki/NC_(complexity) [2]: https://baldur.iti.kit.edu/hordesat/files/horde.pdf https://baldur.iti.kit.edu/hordesat/files/horde.pdf

js8 3y ago

You could reduce to 2XSAT and presolve the linear portion. That would paralelize. I think people are not doing it because they are not aware of the reduction.

adrianN 3y ago
You'd think that the handful of people who devote a significant fraction of their time to writing SAT solver would be aware of such simple tricks and there might be other reasons why your idea isn't being applied.
- js8 3y ago
  I would think so too, but I couldn't find this particular trick anywhere. Anyway, I believe it's similar to LP - we still use simplex method in practice, despite the fact that LP has a polynomial algorithm. What likely happens in SAT is even though there actually is (as I believe) a nice polynomial algorithm on the order of O(n^4) or so (which involves repeated solving of linear systems), the CDCL still wins in practical problems simply because in most cases, the upfront cost of solving the equations is higher than trying to find a first solution. However, not all hope is lost. You could actually presolve a more general problem, and then just rely on propagation to deal with a more specific instance. For instance, for integer factorization, you could presolve a general system for integers of certain bit size, and then if you wanted to factorize a specific integer, you would just plugin constants into the presolved instance. That would eliminate most of the upfront cost and bring it on par with CDCL. Unfortunately, DIMACS is not all that good format to represent SAT, because it is not composable like this - it doesn't allow for representation of presolved instances. But composability might be a win for a different types of algorithms, which do presolving.
  - adrianN 3y ago
    If you know a O(n^4) algorithm for SAT, I'm sure a couple of people would be interested in your paper.
    - js8 3y ago
      I don't really know the exact algorithm yet, but I have a strong feeling it is possible based on what I see. There are like 3 major steps in the strategy, first one is 2XSAT reduction, second is a proof of refutation completeness (in particular, a form of deduction theorem) of a certain logic that models 2XSAT class, and the last one is polynomial-sized representation of all true statements in that logic (which uses n sets of linear equations, and from that follows the complexity of O(n^4)). The 2XSAT reduction is 100% correct (I have been using it to solve small integer factoring problems), the deduction theorem proof still has a small flaw which I think is fixable, and the third part is an ongoing research which is trucking along. I will get there eventually, but if more people would be looking at this approach, then we (humanity) could arrive there faster, that's all.
      - bmc7505 3y ago
        Just gotta keep on trucking. Either way, I would be interested in seeing how the 2XSAT reduction works. Don't get discouraged!

thesz 3y ago

ManySAT: http://www.cril.univ-artois.fr/~jabbour/manysat.htm http://www.cril.univ-artois.fr/~jabbour/manysat.htm It shares short conflict clauses between parallel solvers and achieves superlinear speedup in some cases, e.g., 4 parallel solvers solve faster than one forth of the single solver soolution time. Short conflict clauses are rare so there is little communication between solvers required. CryptoMiniSAT: https://github.com/msoos/cryptominisat https://github.com/msoos/cryptominisat Author's goal to have solver that is good in computing range from single CPU up to cluster. Judging from CryptoMiniSAT successes, he has mostly reached the goal.