Using machine learning classifiers in SAT branching

Simple item page
dc.contributor.authorBergin, Ruth Helenen
dc.contributor.authorDalla, Marcoen
dc.contributor.authorVisentin, Andreaen
dc.contributor.authorO'Sullivan, Barryen
dc.contributor.authorProvan, Gregoryen
dc.contributor.funderScience Foundation Irelanden
dc.contributor.funderEuropean Regional Development Funden
dc.date.accessioned2023-11-03T14:33:41Z
dc.date.available2023-11-03T14:33:41Z
dc.date.issued2023-07-02en
dc.description.abstractThe Boolean Satisfiability Problem (SAT) can be framed as a binary classification task. Recently, numerous machine and deep learning techniques have been successfully deployed to predict whether a CNF has a solution. However, these approaches do not provide a variables assignment when the instance is satisfiable and have not been used as part of SAT solvers. In this work, we investigate the possibility of using a machine-learning SAT/UNSAT classifier to assign a truth value to a variable. A heuristic solver can be created by iteratively assigning one variable to the value that leads to higher predicted satisfiability. We test our approach with and without probing features and compare it to a heuristic assignment based on the variable's purity. We consider as objective the maximisation of the number of literals fixed before making the CNF unsatisfiable. The preliminary results show that this iterative procedure can consistently fix variables without compromising the formula's satisfiability, finding a complete assignment in almost all test instances.en
dc.description.statusPeer revieweden
dc.description.versionAccepted Versionen
dc.format.mimetypeapplication/pdfen
dc.identifier.citationBergin, R.H., Dalla, M., Visentin, A., O’Sullivan, B. and Provan, G. (2023) ‘Using machine learning classifiers in SAT branching’, Sixteenth International Symposium on Combinatorial Search, Proceedings of the International Symposium on Combinatorial Search, 16(1), pp. 169–170, https://doi.org/10.1609/socs.v16i1.27298en
dc.identifier.doihttps://doi.org/10.1609/socs.v16i1.27298en
dc.identifier.endpage170en
dc.identifier.isbn978-1-57735-882-4en
dc.identifier.issn2832-9163en
dc.identifier.issn2832-9171en
dc.identifier.issued1en
dc.identifier.startpage169en
dc.identifier.urihttps://hdl.handle.net/10468/15191
dc.identifier.volume16en
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 2/12/RC/2289-P2s/IE/INSIGHT Phase 2/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 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 ArtificialIntelligence (www.aaai.org)en
dc.subjectSearch in Boolean satisfiabilityen
dc.subjectMachine and deep learning in searchen
dc.subjectRandom vs systematic search strategy selectionen
dc.subjectTimeen
dc.subjectMemoryen
dc.subjectSolution quality trade-offsen
dc.subjectCombinatorial Searchen
dc.subjectArtificial intelligenceen
dc.subjectMachine learningen
dc.subjectSearch strategy selectionen
dc.subjectBoolean satisfiability problem (SAT)en
dc.titleUsing machine learning classifiers in SAT branchingen
dc.typeConference itemen
oaire.citation.issue1en
oaire.citation.volume16en
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
SOCS2023___ML_for_SAT_Branching___AV.pdf
Size:
123.25 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