pmc est un préprocesseur associant à une formule CNF d’entrée une formule CNF de sortie qui est soit logiquement équivalente à l’entrée, soit n’a que le même nombre de modèles que l’entrée (en fonction des préprocesseurs élémentaires qui sont utilisés). Ces prétraitements comprennent la réduction des occurrences, la vivification, l’identification du “backbone”, ainsi que l’identification et le remplacement des portes d’équivalence, AND et XOR.



Toute catégorie    Compilateurs   


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