CNF Rule hierarchy discovery
Efficient CNF Simplification based on Binary Implication Graphs, Marijn Heule, Matti Jarvisalo, and Armin Biere, 2011
  
  "This paper develops techniques for efficiently detecting and removing redundancies from CNF (conjunctive normal form) formulas based on the underlying binary clause structure (i.e., the binary implication graph) of the formulas. 
  
  In addition to considering known simplification techniques (hidden tautology elim- ination (HTE), hyper binary resolution (HBR), failed literal elimination over binary clauses, equivalent literal substitution, and transitive reduction  of the binary implication graph), we introduce the novel technique of hidden literal elimination (HLE) that removes so-called hidden literals from clauses without affecting the set of satisfying assignments."


I recommend Section 2.1 of the paper which reviews known simplification techniques.