A machine learning approach to model counting

Loading...
Thumbnail Image
Date
2024
Authors
Dalla, Marco
Visentin, Andrea
O'Sullivan, Barry
Journal Title
Journal ISSN
Volume Title
Publisher
Institute of Electrical and Electronics Engineers (IEEE)
Published Version
Research Projects
Organizational Units
Journal Issue
Abstract
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.
Description
Keywords
Model counting , Machine learning , SAT problem , Feature analysis
Citation
Dalla, M., Visentin, A., and O'Sullivan, B. (2024) 'A Machine Learning Approach to Model Counting' , IEEE International Conference on Tools with Artificial Intelligence (ICTAI), Herndon, Virginia, USA, October 28–30, October 2024.
Link to publisher’s version
Copyright
© 2024, IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.