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.