Preprocessing in Model Counting through Clause and Variable Elimination

Abstract:

Article Preview

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.

Info:

Periodical:

Advanced Materials Research (Volumes 255-260)

Edited by:

Jingying Zhao

Pages:

2033-2036

DOI:

10.4028/www.scientific.net/AMR.255-260.2033

Citation:

Q. Guo et al., "Preprocessing in Model Counting through Clause and Variable Elimination", Advanced Materials Research, Vols. 255-260, pp. 2033-2036, 2011

Online since:

May 2011

Export:

Price:

$35.00

In order to see related information, you need to Login.

In order to see related information, you need to Login.