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.

Any category    Compiler   

2014 Jean-Marie Lagniez, Pierre Marquis, Preprocessing for Propositional Model Counting in 28th AAAI Conference on Artificial Intelligence (AAAI'14), pp. 2688-2694, 2014.