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 th

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.