Every few years or so I get interested in implementing a SAT solver. In 2021 I reached something of a peak: the full implementation can be found in github. Writing this summary post now 3 years later, I see the README is pretty good (and as far as I see comparing it to my memories, accurate) as well as the pdf writeup.

The Project

I wanted to learn more about SAT solving, and implement the solver. It’s such a central problem to computer science, I am glad to have a deeper understanding of it. I studied related problems in grad school for computational complexity; that the practical algorithms to solve it seem to disconnected from that structure is itself very interesting.

The code is in C++, and was an attempt to admit myriad options for which optimization algorithms to use, to facilitate experimentation and learning. Maintaining a SAT solver with such a plugins setup (without incurring ludicrous overhead) was itself an interesting challenge. I was able to explore most of the algorithms I wanted to.

For more details please read the README and paper.

The Takeaways

One thing: I’m interested in doing things correctly. For many of the algorithms in SAT solving, I found it remarkably difficult to verify that I was doing things correctly. Of course the algorithms weren’t trivial, but they weren’t mind-boggling either. Instead the challenge in verification was, ironically, finding a certificate of correctness. Things like two-watched-literal-scheme involved an intermediate structure that has certain invariants that can be validated at runtime, but even then it’s sophisticated enough where it’s not obvious it’s correct. Moreover, when the intended result is that “on some inputs, things get faster”, there’s always that specter of “if it doesn’t get faster, is it the input, or the code?”. This is even-more-exacerbated by many of the improvements being based on hardware changes, better cache usage etc.

I generally came to call these sort of things “qualitative features”. It is changes in execution that seem coNP to validate, har har.