B+E is a preprocessor that associates with an input CNF formula an output CNF formula which admits the same number of models. B+E tracks definability relations between variables (aka gates) and use them to reduce the instance by eliminating variables which have been identified as outputs of some gates.


Authors :
Pierre Marquis
Jean-Marie Lagniez
Emmanuel Lonca

GPL    Any category    Compiler   

    • Go to the software webpage

    Source code

    International journals

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

    International conferences

    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.