Spent a lot of today in an industry talk and talking with my colleague Nate about SAT solving. With my recent partial read of the Narbonic archives on my brain, a comment from Nate made me realize—those who build SAT solvers are the mad scientists of CS…
For those who don't know: basically 3-CNF SAT is a sort of puzzle problem, albeit one with a lot of practical applications. You are given a formula like
(A or B or not C) and (A or C or D)
with an arbitrary number of atoms (capitalized names) and clauses (parenthesized expressions). To solve the problem, find an assignment of the values true and false to the atoms that makes the whole formula evaluate to true.
In our example case, this is easy: A=true, B=false, C=false, D=false is such an assignment. As the instances get larger, it turns out that there would be important consequences if one could give a method that always finds such an assignment (when it exists) quickly. It would also be satisfying to prove that no such method exists. Unfortunately, to date no one has done either: 3-CNF SAT is the canonical example of what is known as the NP-complete problems. Because there are cool things that you can do if you can solve 3-CNF SAT instances (trust me), people still try to build solvers that work well at least on small or simple instances.
The point I'm making (after way too much explanation) is that the way SAT solvers are built seems to be mostly in the mad science style. Somebody has a wacky idea for how to speed up solving, "we must use oysters!" Much work then goes into building oyster-based solvers, racing them against previous solvers, finding out what kinds of problems oyster-based solvers can solve that other solvers cannot, and picking magic tuning constants that constitute slight performance improvements. Perhaps four dozen people in the world even care, and most of those have their own schemes.
It's a lot of fun, but being a SAT otaku is also a weird experience. I'm getting back into it now—but how far? (B)