SATfeatPy -- A Python-based Feature Extraction System for Satisfiability

TL;DR

SATfeatPy is a comprehensive Python library that extracts structural and statistical features from SAT instances, enabling improved machine learning-based SAT classification and analysis.

Contribution

It provides an up-to-date, easy-to-use implementation of key SAT feature extraction techniques, addressing reproducibility and comparison issues in the field.

Findings

High accuracy in SAT/UNSAT classification

Effective problem category prediction

Insights from ablation study on feature importance

Abstract

Feature extraction is a fundamental task in the application of machine learning methods to SAT solving. It is used in algorithm selection and configuration for solver portfolios and satisfiability classification. Many approaches have been proposed to extract meaningful attributes from CNF instances. Most of them lack a working/updated implementation, and the limited descriptions lack clarity affecting the reproducibility. Furthermore, the literature misses a comparison among the features. This paper introduces SATfeatPy, a library that offers feature extraction techniques for SAT problems in the CNF form. This package offers the implementation of all the structural and statistical features from there major papers in the field. The library is provided in an up-to-date, easy-to-use Python package alongside a detailed feature description. We show the high accuracy of SAT/UNSAT and problem category classification, using five sets of features generated using our library from a dataset of 3000 SAT and UNSAT instances, over ten different classes of problems. Finally, we compare the usefulness of the features and importance for predicting a SAT instance's original structure in an ablation study.