Definability for model counting

We define and evaluate a new preprocessing technique for propositional model counting. This technique leverages definability, i.e., the ability to determine that some gates are implied by the input formula Sigma. Such gates can be exploited to simplify Sigma without modifying its number of models. Unlike previous techniques based on gate detection and replacement, gates do not need to be made explicit in our approach. Our preprocessing technique thus consists of two phases: computing a bipartition < l, O > of the variables of Sigma where the variables from O are defined in E in terms of I, then eliminating some variables of O in Sigma. Our experiments show the computational benefits which can be achieved by taking advantage of our preprocessing technique for model counting. (C) 2020 Elsevier B.V. All rights reserved.