Preprocessing for Propositional Model Counting

This web page contains:

the runtime code of our preprocessor pmc under Linux OS (preproc linux) or Mac OS (preproc mac)
a list of the benchmarks considered in our experiments (list of benchmarks used)
the benchmarks themselves (set of benchmarks)
a table synthesizing the empirical results (full table)

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