Share Email Print
cover

Proceedings Paper

Effective preprocessing in #SAT
Author(s): Qin Guo; Juan Sang; Yong-mei He
Format Member Price Non-Member Price
PDF $14.40 $18.00

Paper Abstract

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.

Paper Details

Date Published: 13 January 2012
PDF: 5 pages
Proc. SPIE 8350, Fourth International Conference on Machine Vision (ICMV 2011): Computer Vision and Image Analysis; Pattern Recognition and Basic Technologies, 835022 (13 January 2012); doi: 10.1117/12.921379
Show Author Affiliations
Qin Guo, Jilin Univ. of Finance and Economics (China)
Juan Sang, Jilin Univ. of Finance and Economics (China)
Yong-mei He, Jilin Univ. of Finance and Economics (China)


Published in SPIE Proceedings Vol. 8350:
Fourth International Conference on Machine Vision (ICMV 2011): Computer Vision and Image Analysis; Pattern Recognition and Basic Technologies

© SPIE. Terms of Use
Back to Top