Effective preprocessing in #SAT
Qin Guo, Juan Sang, HE Yong-mei · Proceedings of SPIE, the International Society for Optical Engineering/Proceedings of SPIE · 2011
Preprocessing #SAT instances can reduce their size considerably and decrease the solving time. In this paper we investigate the use of the hyper-binary resolution and equality reduction to preprocess the #SAT instances. And a preprocessing algorithm Preprocess MC is presented, which combines the unit propagation, the hyper-binary resolution, and the equality reduction together. The experiment shows that these excellent technologies not only reduce the size of the #SAT formula, but also improve the ability of the model counters to solve #SAT problems.