SAT feature analysis for machine learning classification tasks

Dalla, Marco; Provan-Bessell, Benjamin; Visentin, Andrea; O'Sullivan, Barry

SAT feature analysis for machine learning classification tasks

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

Publisher

The AAAI Press

Published Version

https://doi.org/10.1609/socs.v16i1.27292

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.

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