SAT feature analysis for machine learning classification tasks

Loading...
Thumbnail Image
Files
SOCS2023_SATFeatPy_AV.pdf(453.6 KB)
Accepted version
Date
2023-07-02
Authors
Dalla, Marco
Provan-Bessell, Benjamin
Visentin, Andrea
O'Sullivan, Barry
Journal Title
Journal ISSN
Volume Title
Publisher
The AAAI Press
Research Projects
Organizational Units
Journal Issue
Abstract
The extraction of meaningful features from CNF instances is crucial to applying machine learning to SAT solving, enabling algorithm selection and configuration for solver portfolios and satisfiability classification. While many approaches have been proposed for feature extraction, their relevance to these tasks is unclear. Their applicability and comparison of the information extracted and the computational effort needed are complicated by the lack of working or updated implementations, negatively affecting reproducibility. In this paper, we analyse the performance of five sets of features presented in the literature on SAT/UNSAT and problem category classification over a dataset of 3000 instances across ten problem classes distributed equally between SAT and UNSAT. To increase reproducibility and encourage research in this area, we released a Python library containing an updated and clear implementation of structural, graph-based, statistical and probing features presented in the literature for SAT CNF instances; and we define a clear pipeline to compare feature sets in a given learning task robustly. We analysed which of the computed features are relevant for the specific task and the tradeoff they provide between accuracy and computational effort. The results of the analysis provide insights into which features mostly affect an instance's satisfiability and which can be used to identify the problem's type. These insights can be used to develop more effective solver portfolios and satisfiability classification algorithms.
Description
Keywords
Machine and deep learning in search , Search in Boolean satisfiability , Portfolios of search algorithms , Time , Memory , Solution quality trade-offs , Combinatorial Search , SAT CNF instances , Artificial intelligence , SAT/UNSAT , SATfeatPy , Problem category classification , Machine learning , AI
Citation
Dalla, M., Provan-Bessell, B., Visentin, A. and O’Sullivan, B. (2023) ‘SAT feature analysis for machine learning classification tasks’, Sixteenth International Symposium on Combinatorial Search, Proceedings of the International Symposium on Combinatorial Search, 16(1), pp. 138–142, https://doi.org/10.1609/socs.v16i1.27292
Link to publisher’s version
Copyright
© 2023, Association for the Advancement of Artificial Intelligence (www.aaai.org)