Preprocessing in Model Counting through Clause and Variable Elimination
Preprocessing model counting instances can reduce their size considerably and decrease the solving time. In this paper we present a preprocessing algorithm Preprocess, which combines many advanced techniques, such as the unit propagation, and the hyper-binary resolution. In particular, it also combines (1) clause elimination by subsumption, and (2) variable elimination by equivalence reasoning. It has proved that these excellent technologies not only reduce the size of the model counting formulae, but also improve the ability of the model counters to solve model counting problems.
Q. Guo et al., "Preprocessing in Model Counting through Clause and Variable Elimination", Advanced Materials Research, Vols. 255-260, pp. 2033-2036, 2011