8 ms·

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 b

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?

dietr1ch 3y ago
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.
- inasio 3y ago
  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
fovc 3y ago
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)
- pwdisswordfishc 3y ago
  https://xkcd.com/559/ https://xkcd.com/559/
  - fovc 3y ago
    I guess “pun” because I proposed an exponential worst-case but usually actually fast algorithm based on backtracking, which is what SAT is.
- eru 3y ago
  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-solver/index.html https://www.gibiansky.com/blog/verification/writing-a-sat-so... and https://sahandsaba.com/understanding-sat-by-implementing-a-simple-sat-solver-in-python.html https://sahandsaba.com/understanding-sat-by-implementing-a-s...
  - fovc 3y ago
    > 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.)
    - eru 3y ago
      You can find many textbooks online. With varying degrees of legality.
karpierz 3y ago
I'd recommend starting here: http://minisat.se/ http://minisat.se/
Jtsummers 3y ago
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-volume-4b-combinatorial-9780201038064 https://www.informit.com/store/art-of-computer-programming-v...
- svat 3y ago
  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 https://cs.stanford.edu/~knuth/fasc6a.ps.gz 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.
  - Jtsummers 3y ago
    I was looking for that and didn't find it on his page. Thanks.
nuand 3y ago
https://sat-smt.codes/ https://sat-smt.codes/ is the best introductory to expert, and reference work I've ever read on SAT/SMT solvers
bravura 3y ago
I really loved this work on SAT: http://www.cs.cornell.edu/selman/papers/pdf/97.aaai.invariants.pdf 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.
belter 3y ago
I think you are supposed to start from here: https://ebooks.iospress.nl/volume/handbook-of-satisfiability-second-edition https://ebooks.iospress.nl/volume/handbook-of-satisfiability...

dietr1ch 3y ago

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.

inasio 3y ago
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

fovc 3y ago

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)

pwdisswordfishc 3y ago
https://xkcd.com/559/ https://xkcd.com/559/
- fovc 3y ago
  I guess “pun” because I proposed an exponential worst-case but usually actually fast algorithm based on backtracking, which is what SAT is.
eru 3y ago
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-solver/index.html https://www.gibiansky.com/blog/verification/writing-a-sat-so... and https://sahandsaba.com/understanding-sat-by-implementing-a-simple-sat-solver-in-python.html https://sahandsaba.com/understanding-sat-by-implementing-a-s...
- fovc 3y ago
  > 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.)
  - eru 3y ago
    You can find many textbooks online. With varying degrees of legality.

karpierz 3y ago

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

Jtsummers 3y ago

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-volume-4b-combinatorial-9780201038064 https://www.informit.com/store/art-of-computer-programming-v...

svat 3y ago
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 https://cs.stanford.edu/~knuth/fasc6a.ps.gz 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.
- Jtsummers 3y ago
  I was looking for that and didn't find it on his page. Thanks.

nuand 3y ago

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

bravura 3y ago

I really loved this work on SAT: http://www.cs.cornell.edu/selman/papers/pdf/97.aaai.invariants.pdf 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.

belter 3y ago

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