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.<p>Also if anyone knows about how can they be applied in a compiler (typesystem, optimization, …), feedback is also welcomed.
Minisat is designed to elucidate; consider reading the paper and implementation - it's actually a very fast solver.<p>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.