
Proceedings Paper
Effective preprocessing in #SATFormat | Member Price | Non-Member Price |
---|---|---|
$17.00 | $21.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
Published in SPIE Proceedings Vol. 8350:
Fourth International Conference on Machine Vision (ICMV 2011): Computer Vision and Image Analysis; Pattern Recognition and Basic Technologies
Safaa S. Mahmoud; Zhu Zeng; Yuting Li, Editor(s)
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)
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
Safaa S. Mahmoud; Zhu Zeng; Yuting Li, Editor(s)
© SPIE. Terms of Use
