## The pmc preprocessor

### Preprocessing for Propositional Model Counting

pmc is a preprocessor associating with an input CNF formula an output CNF formula which is either logically equivalent to the input or has only the same number of models as the input (depending on the elementary preprocessings which are used). Such preprocessings include occurrence reduction, vivification, backbone identification, as well as equivalence, AND and XOR gate identification and replacement.

#### Ressources for the pmc preprocessor (V 1.1)

- 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)

J.-M. Lagniez, P. Marquis. "Preprocessing for Propositional Model Counting". Proceedings of AAAI'14, pages 2688-2694. (pdf)

#### 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:

p cnf 123 4567

1 -2 3 0

....

p cnf 123 4567

1 -2 3 0

....

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.