Hacker News new | past | comments | ask | show | jobs | submit login

The "2 watched literal" algorithm used in sat solvers (here is a random blog post I found by googling http://haz-tech.blogspot.com/2010/08/whos-watching-watch-lit... ).

The algorithm has many lovely features. It is very efficient -- it is used in basically every SAT solver with minimal modifications. It's not entirely trivial it works, particularly the backtracking part. It is a good example of how there are algorithms which are extremely hard to do functionally (the whole algorithm is about moving pointers around).

It's also a good example of practical Vs theoretical efficiency. In the worst case it is no more efficient than the algorithm it replaced, in practice it is hundreds of times more efficient. The "not moving back" feels like it should save at most half the time, it on fact speeds things up by often 10 times (this is because watches are often moved around until they reach some "boring" variables, where they lay undisturbed).




Awesome, thanks for mentioning this! I completely forgot about 2-literal watching and I hadn't ever thought about the idea that it'd be difficult to implement functionally. It's absolutely clever. And one other intuition I would like to add to it is that, from the way I see it at least, it is a cheap "detector" for when 3-SAT degenerates into 2-SAT, which finally becomes polynomial-time solvable -- which is exactly the kind of thing you want to have a detector for!


this is a neat way to avoid moving those pointers around: https://www.cs.kent.ac.uk/pubs/2010/2970/content.pdf


While this is very cute I'd be interested to know what kind of code it turns into -- I imagine it will either boil down to the same, or will be much slower (but I am happy to be impressed)




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: