Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Parallelization of SAT Algorithms on GPUs [pdf]

algos.inesc-id.pt

Post reply on HN
Print view View original

1–10 of 19 posts

Re: Parallelization of SAT Algorithms on GPUs [pdf]

#3

Post by raverbashing »

petters wrote: post #2

This is a proposed work for a Master's thesis. It seems to be from 2013, so I wonder whether it was successful? If I had to guess, I would think implementing a SAT solver on a GPU is quite hard. Many branches etc.

It would be interesting to apply probabilistic algorithms for SAT solving in GPUs

Re: Parallelization of SAT Algorithms on GPUs [pdf]

#4

Post by mate_soos »

This approach is unworkable, it has been demonstrated many times. I have not only been developing a SAT solver for >7 years (with >9000 commits) but also have participated in the SAT competition in all these years. I used to get a proposal like this a lot (thankfully, they dried up). None of them made it work. I used to work on programming GPGPUs in a professional setting, (rainbow table generators&lookup systems), so I'm not unfamiliar with their advantages and restrictions.

This approach is unworkable because: * propagation needs modification of the watchlist (or it needs to have all literals of all clauses attached, which is incredibly slow and also unworkable) * propagation is actually only about 50-60% of what a solver is doing: conflict resolution, clause database management and inprocessing takes a lot of time * propagation is hard to parallelize as you need to update a global data structure of propagated literals and then act on that * etc

This proposal will not work (and I sure it did not, if it was ever tried) and I don't understand how it got this high at ycombinator. If you want to look at good SAT solvers, look at lingeling, COPMinisat, MiniSat, or CryptoMiniSat. You may learn a lot from them. Easy starting is MiniSat. Good luck :)

Re: Parallelization of SAT Algorithms on GPUs [pdf]

#5

Post by wmu »

petters wrote: post #2

This is a proposed work for a Master's thesis. It seems to be from 2013, so I wonder whether it was successful? If I had to guess, I would think implementing a SAT solver on a GPU is quite hard. Many branches etc.

Look at http://algos.inesc-id.pt/~pff/projects/parsat/?Publications

It seems Mr Costa has graduated, but the link to his thesis points to an empty pdf.

Re: Parallelization of SAT Algorithms on GPUs [pdf]

#6

Post by mafribe »

There is quite a bit of work on parallelising SAT solving, as it's one of the most important algorithmic problems, both in theory and in practise, but (as far as I'm aware) the top sequential algorithms still beat parallel solvers. The most successful approach at this point seems to be Cube-and-Conquer [1], but I don't think this is considered a good approach in itself. There is a huge amount of scope for new ideas. I doubt that anything naive will work, as SAT solving is a rather competitive research field.

The annual SAT competition http://www.satcompetition.org has a track for parallel solving.

See [2, 3, 4] for an overview of the field.

[1] M. J. H. Heule, O. Kullmann, S. Wieringa, A. Biere, Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads.

[2] S. Hölldobler, N. Manthey, V. H. Nguyen, J. Stecklina, P. Steinke, A Short Overview on Modern Parallel SAT-Solvers.

[3] S. Wieringa, K. Heljanko, Asynchronous Multi-Core Incremental SAT Solving.

[4] Y. Hamadi, C. M. Wintersteiger, Seven Challenges in Parallel SAT Solving.

Re: Parallelization of SAT Algorithms on GPUs [pdf]

#7

Post by mafribe »

mate_soos wrote: post #4

This approach is unworkable, it has been demonstrated many times. I have not only been developing a SAT solver for >7 years (with >9000 commits) but also have participated in the SAT competition in all these years. I used to get a proposal like this a lot (thankfully, they dried up). None of them made it work. I used to work on programming GPGPUs in a professional setting, (rainbow table generators&lookup systems), s…

   If you want to look at good SAT 
   solvers, look ... CryptoMiniSat.
Any personal relationship with CryptoMiniSat? ;)

Re: Parallelization of SAT Algorithms on GPUs [pdf]

#8

Post by mate_soos »

mafribe wrote: post #7
mate_soos wrote: post #4

This approach is unworkable, it has been demonstrated many times. I have not only been developing a SAT solver for >7 years (with >9000 commits) but also have participated in the SAT competition in all these years. I used to get a proposal like this a lot (thankfully, they dried up). None of them made it work. I used to work on programming GPGPUs in a professional setting, (rainbow table generators&lookup systems), s…

If you want to look at good SAT solvers, look ... CryptoMiniSat. Any personal relationship with CryptoMiniSat? ;)

Considering that CryptoMiniSat got 3rd place (after 1st and 2nd both being lingeling) in Parallel SAT solving the last competition, I think it was fair to include it. Sure, it's mine, but I also put it at the end :) Other solvers that are good to look at: glucose and riss. Note that a lot of solvers are variations of MiniSat. riss, ligeling, PrecoSat and CryptoMiniSat are the only ones that substantially differ from MiniSat.

Re: Parallelization of SAT Algorithms on GPUs [pdf]

#9

Post by mtve »

mate_soos wrote: post #4

This approach is unworkable, it has been demonstrated many times. I have not only been developing a SAT solver for >7 years (with >9000 commits) but also have participated in the SAT competition in all these years. I used to get a proposal like this a lot (thankfully, they dried up). None of them made it work. I used to work on programming GPGPUs in a professional setting, (rainbow table generators&lookup systems), s…

Google does not know "COPMinisat", would you please clarify?

PicoSAT is also small and easy to embed, however in CryptoMiniSat we trust, thank you very much!

Re: Parallelization of SAT Algorithms on GPUs [pdf]

#10

Post by panic »

mafribe wrote: post #6

There is quite a bit of work on parallelising SAT solving, as it's one of the most important algorithmic problems, both in theory and in practise, but (as far as I'm aware) the top sequential algorithms still beat parallel solvers. The most successful approach at this point seems to be Cube-and-Conquer [1], but I don't think this is considered a good approach in itself. There is a huge amount of scope for new ideas.…

Here's a non-paywalled link to [2] if anyone else is looking for it: http://www.ki.inf.tu-dresden.de/~norbert/webdata/publication...
Post reply on HN