The International SAT Competition Web Page

http://www.satcompetition.org/

by kelseyfrog • 3 years ago

42 16 3 years ago

aarestad• 3 years ago

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• 3 years 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• 3 years 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

fovc3• 3 years 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• 3 years ago

https://xkcd.com/559/

eru2• 3 years 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-so... and https://sahandsaba.com/understanding-sat-by-implementing-a-s...

karpierz• 3 years ago

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

Jtsummers2• 3 years 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-v...

svat• 3 years 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

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.

nuand• 3 years ago

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

bravura• 3 years ago

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.

belter• 3 years ago

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

The International SAT Competition Web Page

Related Stories