I have lately been describing two techniques to speed up SAT solving: on-the-fly self-subsuming resolution, and an interesting way to apply asymmetric branching. It turns out, the first was already used in PrecoSat (by Armin Biere) under the name “strong minimization”, and the second was already published as Vivification by Piette, Hamadi and Sais. As far as I could tell, both optimisations bring tangible benefits to SAT solving. I have tried solving the problem instances of the 2009 SAT competition with and without both optimisations, and it turns out that using both is the fastest.

Of course I am at fault for not knowing that these techniques have been published before. Maybe both have been published in respected journals/conferences, but I don’t seem to have the capacity to read every journal and conference article. I think we can safely assume that this is true for most researchers. So are we forever destined to reinvent the wheel? Probably the only techniques that don’t need to be reinvented are those that have been demonstratively shown to work well. Such a technique is for example glue-clauses, or variable elimination (VE). Glucose, the solver based on glue-clauses had won the 2009 SAT competition, and VE in the SatELite preprocessor blew away the 2005 SAT competition. Similarly, xor clauses might end up in mainline SAT solvers due to the win of CryptoMiniSat (even though I think that win was due to far more than just that).

This leads us to a somewhat dim conclusion, however: useful, but small techniques might get lost forever (if they are not reinvented). This is sad, because lots of small techniques bring about lots of improvements in the end, especially if they work together. For example, both techniques mentioned above lead to smaller clauses, which in turn lead to more binary and tertiary clauses. These binary and tertiary clauses lead in turn to increased solving speed due to modern solvers which keep both of them natively in the watchlists. So, as the technology changes, the smallish benefits that some techniques gave might increase due to the technical advancements that have been made since.