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

11–19 of 19 posts

Re: Parallelization of SAT Algorithms on GPUs [pdf]

#11

Post by dlo »

mate_soos wrote: post #8
mafribe wrote: post #7

Earlier quoted context omitted.

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…

Thanks for the recommendations. I love SAT solvers and have been looking for a way to get into them.

Re: Parallelization of SAT Algorithms on GPUs [pdf]

#12

Post by mate_soos »

mtve wrote: post #9
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!

Sorry, wanted to say CoMiniSatPS, here:

http://cs.nyu.edu/~chanseok/cominisatps/index.html

One of its variants won the Main track of the SAT Competition of 2016, see

http://baldur.iti.kit.edu/sat-competition-2016/index.php?cat...

For all the solvers' source codes, see

http://baldur.iti.kit.edu/sat-competition-2016/solvers/

Re: Parallelization of SAT Algorithms on GPUs [pdf]

#14

Post by deepnet »

wmu wrote: post #5
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.

https://fenix.tecnico.ulisboa.pt/downloadFile/395146463244/r...

from May 2014 [pdf]

Re: Parallelization of SAT Algorithms on GPUs [pdf]

#15

Post by dang »

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…

> I don't understand how it got this high at ycombinator

Oh that's easy: because most of us know nothing about SAT solvers other than (maybe) what they are and that they're cool. We need people like you to teach us, so I'm glad you showed up! (A great example of https://meta.wikimedia.org/wiki/Cunningham's_Law.)

Re: Parallelization of SAT Algorithms on GPUs [pdf]

#16

Post by pron »

SAT solvers and neural networks are probably the most curious software technologies around. Both attempt to solve NP-complete problems (learning and SAT). Both are still largely based on 1960s algorithms (backpropagation for NNs and DPLL for SAT) made surprisingly useful in practice by advances in hardware and heuristics accumulated over the years. Both are mysterious from a theoretical point of view, with little progress in our theoretical understanding of why they work well in practice and how we can come up with better algorithms.

This article by Moshe Vardi[1] and this one by Dick Lipton[2] are a nice introduction to the mystery of SAT solvers.

[1]: http://cacm.acm.org/magazines/2014/3/172516-boolean-satisfia...

[2]: https://rjlipton.wordpress.com/2009/07/13/sat-solvers-is-sat...

Re: Parallelization of SAT Algorithms on GPUs [pdf]

#17

Post by p1esk »

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.…

the top sequential algorithms still beat parallel solvers

Wow, that's interesting! Are there any other examples where a sequential algorithm beats a parallel one?

Re: Parallelization of SAT Algorithms on GPUs [pdf]

#18

Post by tlb »

p1esk wrote: post #17
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.…

the top sequential algorithms still beat parallel solvers Wow, that's interesting! Are there any other examples where a sequential algorithm beats a parallel one?

It is an open question whether there exist algorithms that cannot be parallelized. Some that are most likely to be inherently sequential are listed here: https://en.wikipedia.org/wiki/P-complete#P-complete_problems

Re: Parallelization of SAT Algorithms on GPUs [pdf]

#19

Post by pettou »

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…

Please, do you have any recommendations for books about SAT solving for beginners?
Post reply on HN