@inproceedings{HeuleJB:LPAR2010,
 author = {Marijn Heule and Matti J\"arvisalo and Armin Biere},
 title  = {Clause Elimination Procedures for {CNF} Formulas},
 editor = {Christian Ferm\"uller and Andrei Voronkov},
 booktitle = {Proceedings of the 17th International Conference on 
              Logic for Programming, Artificial Intelligence and Reasoning 
              (LPAR-17)},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 volume = {6397},
 pages  = {357--371},
 year   = {2010},
}

Abstract:

We develop and analyze clause elimination procedures, a specific family 
of simplification techniques for conjunctive normal form (CNF) formulas. 
Extending known procedures such as tautology, subsumption, and blocked 
clause elimination, we introduce novel elimination procedures based on 
hidden and asymmetric variants of these techniques. We analyze the 
resulting nine (including five new) clause elimination procedures from 
various perspectives: size reduction, BCP-preservance, confluence, and 
logical equivalence. For the variants not preserving logical equivalence, 
we show how to reconstruct solutions to original CNFs from satisfying 
assignments to simplified CNFs. We also identify a clause elimination 
procedure that does a transitive reduction of the binary implication 
graph underlying any CNF formula purely on the CNF level.