A Machine Learning Approach to Model Counting

Model counting (#SAT) is the problem of computing the number of satisfying assignments for a given Boolean formula. It has a significant theoretical and practical interest. Tackling it can be challenging since the number of potential solution grows exponentially with the number of variables. Due to the inherent complexity of the problem, approaches to approximate model counting have been developed as a practical alternative. These methods extract the number of solutions within user-specified tolerance and confidence levels and in a fraction of the time required by exact model counters. However, even these methods require extensive computations, restricting their applicability to relatively small instances. In this paper, we propose a new approximate machine learning model counter that overcome this limitation. Predicting the number of solutions can be seen as a regression problem. We deploy an array of machine learning techniques trained to infer the approximate number of solutions based on statistical features extracted from a SAT propositional formula. Extensive numerical experiments performed on synthetic crafted and benchmark datasets show that learning approaches can provide a good approximation of the number of solutions with a much lower computational time and resource cost than the state-of-the-art approximate and exact model counters, making it possible to approximate the model count of instances previously out of reach. We then investigated the structural factors that lead to a high model count using AI explainability approaches.