mate_soos

Before crying pilot error, we must all read Sydney Dekker's A Field Giude to Understading "Human Error" (and fully appreciate why he uses those quotes). Don't immediately assign blame to the sharp end. Take a look at the blunt one first. Most likely not a pilot error. Assigning blame is a very human need, but assigning it to the most visible and accessible part is almost always wrong.

If you to treat your employees as children, you will end up with a culture of excuses. If you give and take responsiblity for both your own work and the work of helping others do their work, you will realize that excuses won't be needed. People will inherently know they are either messing up or have messed up and will volountarily ask for help from others, who will help.

Not trusting and respecting in your employees will corner them to behave like children and you will eternally (be unhappy to) be their parent. Treat people with trust and respect and expect the same. It will make for a much more happy and a much better performing team and ultimately, company.

I am a bit saddened that Vegard Nossum's work, which they used for encoding SHA-1 to SAT, is only mentioned as a footnote. The github code is at

https://github.com/vegard/sha1-sat

and his Master Thesis, whose quality is approaching a PhD thesis is here:

https://www.duo.uio.no/bitstream/handle/10852/34912/thesis-o...

Note that they also only mention MiniSat as a footnote, which is pretty bad. The relevant paper is at

http://minisat.se/downloads/MiniSat.pdf

All of these are great reads. Highly recommended.

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/

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.

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 :)