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.


Auteurs :
Pierre Marquis
Jean-Marie Lagniez
Emmanuel Lonca

GPL    Toute catégorie    Compilateurs   

    • Aller sur la page web du logiciel

    Code source

    Articles de revues internationales

    2020 Contraintes Jean-Marie Lagniez, Emmanuel Lonca, Pierre Marquis, Definability for model counting in Artificial Intelligence, vol. 281, pp. 103229, 2020.

    Articles de conférences internationales

    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.