While writing the description of CryptoMiniSat for the 2010 SAT Race, I have realised how powerful the blocked clause elimination (BCE) technique by Matti Jarvisalo and Armin Biere is. For xor clauses, which represent a simple XOR like
v1 + v2 + v3 = true
there is a technique called dependent variable removal by Heule and Maaren. This technique removes an xor clause if one of its variables appears only in one place: in that xor clause. The idea is that since that variable only appears there, the XOR can always be satisfied. For example, if variable v1 is dependent (i.e. it only appears in this XOR), and
v2 = true, v3 = true
then this xor-clause can simply be satisfied by giving v1 = true:
true + true + true = true
So, variable v1 can be removed from the problem along with the xor clause, and the value of variable v1 needs only to be calculated after the solving has finished.
The great thing about blocked clause elimination, is that it can achieve this automatically, without the use of xor-clauses! Let us convert our xor-clause into regular clauses:
v1 v2 v3 (1)v1 -v2 -v3 (2)-v1 v2 -v3 (3)-v1 -v2 v3 (4)
Now, let us try to block these clauses on variable v1. Resolving (1) with (3) gives tautology since the result of the resolution,
v2 v3 v2 -v3
has both a literal and its negation (v3 and -v3) in it. The same is true for resolving (1) and (4), this time with v2 and -v2. The same happens to (2)&(3) and (2)&(4), too, eventually removing all clauses.
So, can blocked clause elimination replace dependent variable removal? I am not sure. Dependent variable removal can be used in conjunction with other methods that treat xor caluses, that can lead to potentially very long XOR chains. These long XOR chains are not well handled through regular clauses, and so they are not created by solvers that don’t handle xor clauses natively — creating them is avoided through heuristic cut-offs. Thus, dependent variable removal can potentially remove more of these XOR-s than blocked clause elimination. But blocked clause elimination can remove clauses that dependent variable elimination cannot. So, I believe there is point in using both.