Submitter: Armin Biere
Description: Devised by Armin Biere, it is based on Q-resolution (to eliminate existential variables) and Shannon expansion (to eliminate universal variables), plus a number of features, such as equivalence reasoning, subsumption checking, pure literal detection, unit propagation, and also a scheduler for the elimination step. [ A. Biere. Resolve and Expand. In Seventh Intl. Conference on Theory and Applications of Satisfiability Testing (SAT'04), volume 3542 of LNCS, 2005.]