GPU's are not friends with pointer chasing, which is the basis of contemporary CDCL solvers, because internal lazily-updateable structures are multi-linked list

GPU's are not friends with pointer chasing, which is the basis of contemporary CDCL solvers, because internal lazily-updateable structures are multi-linked lists. They are not friends with bottlenecks like clause queues used in contemporary stochastic SAT solvers. They can be good at something like survey and/or belief propagation [1]. [1] https://simons.berkeley.edu/talks/belief-survey-propagation https://simons.berkeley.edu/talks/belief-survey-propagation The problem is that survey/belief propagatin is effective in the area of random CNF problems and it is not a complete solution technique. It may compute a solution but it cannot provide you with the evidence that there is no soolution.