SAT feature analysis for machine learning classification tasks

Simple item page
dc.contributor.authorDalla, Marcoen
dc.contributor.authorProvan-Bessell, Benjaminen
dc.contributor.authorVisentin, Andreaen
dc.contributor.authorO'Sullivan, Barryen
dc.contributor.funderScience Foundation Irelanden
dc.contributor.funderEuropean Regional Development Funden
dc.date.accessioned2023-11-03T14:12:23Z
dc.date.available2023-11-03T14:12:23Z
dc.date.issued2023-07-02en
dc.description.abstractThe 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.en
dc.description.statusPeer revieweden
dc.description.versionAccepted Versionen
dc.format.mimetypeapplication/pdfen
dc.identifier.citationDalla, 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.27292en
dc.identifier.doihttps://doi.org/10.1609/socs.v16i1.27292en
dc.identifier.endpage142en
dc.identifier.isbn978-1-57735-882-4en
dc.identifier.issn2832-9163en
dc.identifier.issn2832-9171en
dc.identifier.startpage138en
dc.identifier.urihttps://hdl.handle.net/10468/15190
dc.language.isoenen
dc.publisherThe AAAI Pressen
dc.relation.ispartofProceedings of the International Symposium on Combinatorial Searchen
dc.relation.ispartofSixteenth International Symposium on Combinatorial Searchen
dc.relation.projectinfo:eu-repo/grantAgreement/SFI/SFI Research Centres Programme::Phase 1/16/RC/3918/IE/Confirm Centre for Smart Manufacturing/en
dc.relation.projectinfo:eu-repo/grantAgreement/SFI/SFI Research Centres/12/RC/2289/IE/INSIGHT - Irelands Big Data and Analytics Research Centre/en
dc.relation.projectinfo:eu-repo/grantAgreement/SFI/SFI Research Centres Programme::Phase 2/12/RC/2289-P2s/IE/INSIGHT Phase 2/en
dc.relation.projectinfo:eu-repo/grantAgreement/SFI/SFI Centres for Research Training Programme::Data and ICT Skills for the Future/18/CRT/6223/IE/SFI Centre for Research Training in Artificial Intelligence/en
dc.rights© 2023, Association for the Advancement of Artificial Intelligence (www.aaai.org)en
dc.subjectMachine and deep learning in searchen
dc.subjectSearch in Boolean satisfiabilityen
dc.subjectPortfolios of search algorithmsen
dc.subjectTimeen
dc.subjectMemoryen
dc.subjectSolution quality trade-offsen
dc.subjectCombinatorial Searchen
dc.subjectSAT CNF instancesen
dc.subjectArtificial intelligenceen
dc.subjectSAT/UNSATen
dc.subjectSATfeatPyen
dc.subjectProblem category classificationen
dc.subjectMachine learningen
dc.subjectAIen
dc.titleSAT feature analysis for machine learning classification tasksen
dc.typeConference itemen
oaire.citation.issue1en
oaire.citation.volume16en
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
SOCS2023_SATFeatPy_AV.pdf
Size:
453.6 KB
Format:
Adobe Portable Document Format
Description:
Accepted version
Download
License bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
license.txt
Size:
2.71 KB
Format:
Item-specific license agreed upon to submission
Description:
Download
Collections
Computer Science - Conference Items
Insight Centre for Data Analytics - Conference Items