I did a bit of googling to see if I could find a decent civilian introduction to "how to write a SAT solver" but everything I found were papers assume quite a bit of previous knowledge. Is there a good source where one could learn a bit about how to write a basic SAT solver and how to improve on it?

The general purpose algorithm that’s not necessarily the fastest but has an upper bound worst-case runtime:

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)

I guess “pun” because I proposed an exponential worst-case but usually actually fast algorithm based on backtracking, which is what SAT is.

Why do you backtrack when you hit a book?

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

> Why do you backtrack when you hit a book?

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

You can find many textbooks online. With varying degrees of legality.

Well, the simple approach is to use backtracking. From there you can dive into back jumping, constraint learning and DPLL.

Now, implementing that is surely full of tricks too, which you may also find interesting, but is probably not discussed too much.

The simplest is probably WALKSAT-like heuristics, essentially local search: flip a random variable, evaluate, if you see an improvement accept the flip, otherwise try again. This can be surprisingly efficient on some SAT problems

I'd recommend starting here: http://minisat.se/

I like Knuth's writing in general so possibly worth considering TAOCP Volume 4B. (NB: I have not yet obtained and worked through Volumes 4A and 4B, at my current rate of study I probably won't unless I live as long as he has)

https://www.informit.com/store/art-of-computer-programming-v...

In fact, just the part on Satisfiability was previously published (2015, before Volume 4B published 2023) as "Volume 4, Fascicle 6: Satisfiability", and the even-earlier draft (pre-fascicle) is available online at https://cs.stanford.edu/~knuth/fasc6a.ps.gz

I was looking for that and didn't find it on his page. Thanks.

https://sat-smt.codes/ is the best introductory to expert, and reference work I've ever read on SAT/SMT solvers

I really loved this work on SAT:

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.

I think you are supposed to start from here: https://ebooks.iospress.nl/volume/handbook-of-satisfiability...