Ask HN: Beginner pointers on SAT solvers?
I just got started on writing a SAT solver (https://github.com/rjmacready/sat-solver) (this is not working ATM) and while I’ve been finding some resources, I feel like I’m missing something … does anyone have some beginner pointers on SAT solver implementation? I was looking for something like pseudocode, algorithm visualization (like this http://www.cs.usfca.edu/~galles/visualization/Algorithms.html, for instance), anything.
Also if anyone knows about how can they be applied in a compiler (typesystem, optimization, …), feedback is also welcomed.
Comments
Minisat is designed to elucidate; consider reading the paper and implementation - it's actually a very fast solver.
As to compilers: one interesting idea is the "superoptimizer". In its basic form, try all byte sequences and use a solver to filter out the ones that do what you want when executed; then pick the fastest. Regehr has an interesting blog post on this topic.
Minisat is definitely on my read list; I'll probably need to read it 2/3 times to fully appreciate it's content. Thanks for the "superoptimizer" pointer, I'll explore that.