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.



GPL    Any category    Compiler   


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.