$ ./pmc -vivification -eliminateLit -litImplied -iterate=10
BENCHMARK
p cnf 123 4567
1 -2 3 0
....
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)
For more details, see the paper:
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:
This combination preserves equivalence (the result is printed on
the standard output):
This combination is guaranteed only to preserve the number
of models of the input (the result is printed on the standard output):
$ ./pmc -vivification -eliminateLit -litImplied -iterate=10
-equiv -orGate -affine BENCHMARK
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.