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.