B+E est un préprocesseur qui associe à une formule CNF d’entrée une formule CNF de sortie qui admet le même nombre de modèles. B+E suit les relations de définissabilité entre les variables (gates) et les utilise pour réduire l’instance en éliminant les variables qui ont été identifiées comme des sorties de certaines gates.



GPL    Toute catégorie    Compilateurs   


2020 Jean-Marie Lagniez, Emmanuel Lonca, Pierre Marquis, Definability for model counting in Artificial Intelligence, vol. 281, pp. 103229, 2020.
2016 Jean-Marie Lagniez, Emmanuel Lonca, Pierre Marquis, Improving Model Counting by Leveraging Definability in 25th International Joint Conference on Artificial Intelligence (IJCAI'16), pp. 751-757, 2016.