Engineering an Efficient Preprocessor for Model Counting

Given a formula F, the problem of model counting is to compute the number of solutions (also known as models) of F. Over the past decade, model counting has emerged as key building block of quantitative reasoning in design automation and artificial intelligence. Given the wide-ranging applications, scalability remains the major challenge. Motivated by the observation that the formula simplification can dramatically impact the performance of the state-of-the-art exact model counters, we design a new state-of-the-art preprocessor, Arjun2, that relies on tight integration of techniques. The design of Arjun2 is motivated from our observation that it is often beneficial to employ preprocessing techniques whose overhead may be prohibitive for the task of SAT solving but not for model counting: accordingly, we rely on a specifically tailored SAT solver design for redundancy detection, sampling-boosted backbone detection, as well as storing of redundancy information for the purposes of improving propagation within top-down model counters. Our detailed empirical evaluation demonstrates that Arjun2 achieves significant performance improvements over prior model counting preprocessors in terms of instance-size reductions achieved as well as the runtime improvements of the downstream model counters.