The International SAT Competition Web Page
satcompetition.org
satcompetition.org
Now, implementing that is surely full of tricks too, which you may also find interesting, but is probably not discussed too much.
1. Pick a paper in the field ~at random.
1b. If it’s basic enough for you, you’re done
2. Read the first few paragraphs and find the most basic statement that is cited
3. Find the cited paper
4. Go back to step 1b
Occasionally you’ll hit a book as the citation, in which case you must backtrack to take a different branch of the tree and try again.
In theory this is worst-case exponential, but in practice most searches end quickly
(Excuse the pun)
Btw, people often cite the earliest articles, but not necessarily the simplest.
Often there are papers like '[topic] simplified' etc, and they can be quite useful.
In our case, an alternative approach is to just do a web search for 'how to write a simple sat solver' and that yields eg https://www.gibiansky.com/blog/verification/writing-a-sat-so... and https://sahandsaba.com/understanding-sat-by-implementing-a-s...
Because I usually don’t own those books and don’t have a university library
> Often there are papers like '[topic] simplified' etc, and they can be quite useful.
Yes! This is adding heuristics on top of the basic algorithm, of which there are many useful ones. (Figure out who the field luminaries are, what the best journals/conferences were, etc.)
https://www.informit.com/store/art-of-computer-programming-v...
In typical Knuth style, it is a very clear and solid explanation of the whole area, assuming no additional background than the rest of the book (high-school/undergraduate math), written in a lively style with concrete examples and humour. It also has the typical Knuth problems: everything is passed through Knuth's own notation and ideas (which are often clearer than mainstream, but nevertheless are different); it's all very densely written (every word matters, even in what looks like casual/breezy sentences): not skimmable, you have to read everything.
http://www.cs.cornell.edu/selman/papers/pdf/97.aaai.invarian...
Local search heuristics typically involve a noise-parameter, which controls the tradeoff between exploration and exploitation. The paper found a statistical measure that was invariant in many heuristics they tried, allowing them quickly to ascertain the optimal noise level for new heuristics. This then allowed them to design better heuristics.
I always found this work quite interesting. Sadly, it's not indexed by ChatGPT because I wanted to interrogate it about recent progress in this specific direction.