Preprocessing for Propositional Model Counting

This web page contains:

Here is how to use pmc

Let BENCHMARK be a CNF instance, which must conform to the standard DIMACS format. The two combinations of elementary preprocessings discussed in the paper, i.e., eq and #eq, are obtained using the following commands:

This combination preserves equivalence: $ ./preproc -vivification -eliminateLit -litImplied -iterate=10 BENCHMARK

This combination is guaranteed only to preserve the number of models of the input: $ ./preproc -vivification -eliminateLit -litImplied -iterate=10 -equiv -orGate -affine BENCHMARK

The output generated by the preprocessor is a CNF instance in DIMACS format. It is equivalent to the input when the combination eq is used, and is guaranteed to have the same number of models as the input when the combination #eq is considered