Self-subsuming resolution | Wonderings of a SAT geek

# Self-subsuming resolution

August 4, 2010 SAT resolution, self-subsuming resolution, simplification, subsumption msoos

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.