Self-subsuming resolution in SAT uses the resolution operator to carry out its magic. Resolution can be used on two clauses if they share a variable, but the sign of the variable is inverted, e.g.v1 V v2-v1 V v3 V v4
(where v1..v4 are binary variables and “V” means binary OR) can be resolved on v1, producing the clause:v2 V v3 V v4
In SAT this is used to simplify problems as follows. Let’s assume we have many clauses, among which there are these three:a V c (1)a V -c V d V f (2)a V -c V g (3)
In this case, if we use the resolution operator on (1) and (2), we get:a V d V f (4)
The interesting thing about (4) is that it is a strict subset of (2). In other words, we could simply replace (2) with (4), thus shortening clause (2). If we use the resolution operator on (1) and (3) we get:a V g (5)
whose literals form a strict subset of those of (3), so we can replace (3) with (5), again shortening a clause. We shortened 2 clauses, each with one literal. For completeness, this technique can be applied in a recursive manner on all possible clause-pairs.
Until now, CryptoMiniSat was doing self-subsuming resolution in such a way that the clauses being manipulated were kept inside the propagation queue. The problem was, that the propagation queue enforces a very strict position of literals in the clause. So, when e.g. removing literal “a” from clause (3), CryptoMiniSat had to completely remove the clause, and then to completely re-add it, since the position of “a” changed (it got removed). The additional overhead for this was simply too much: in certain cases, self-subsuming resolution took 130 seconds to complete, 115 of which was taken by this detach-reattach overhead.
The solution to this problem was to completely remove all clauses from the propagation queue, then do self-subsuming resolution, and finally re-add the clauses. Interestingly, complete removal of all clauses is very fast (essentially, a constant-time operation, even though removing clauses one-by-one is very costly), and completely re-adding them is also very fast (linear in the number of clauses). The first impressions from this technique are very positive, and I decided to release CryptoMiniSat 2.6.0 with this technique included.
NOTE: Thanks to N. Sörensson for pointing me out that self-subsuming resolution could be done better. I am not sure this is what he meant, but fingers are crossed.
Actually, I finally had to a add two more things to this to get it up to the efficiency (in terms of overall solving time) of the original solver:
1) I had to clean the clauses once in a while during subsumption from variables that have already been assigned
2) I had to keep binary clauses inside the watchlists, which is free: no detach-reattach overhead is needed, since these clauses are inside the watchlists “natively”, i.e. without any pointers to the clauses causing them (this is more-or-less the case with GLUCOSE, it is I think the case with the new MiniSat, and it is the case with lingeling).
Unfortunately, I couldn’t detail these experiences, since I struggled with this for about 2 weeks to get it right(!), even though the original (all detach, then all reattach) idea is quite simple. Even now, I think I need to do (1) a bit more to get to the same overall solving speed as with the original no-detach method.