Automated SAT Problem Feature Extraction using Convolutional Autoencoders

Simple item page
dc.contributor.authorDalla, Marco
dc.contributor.authorVisentin, Andrea
dc.contributor.authorO'Sullivan, Barry
dc.contributor.funderScience Foundation Irelanden
dc.contributor.funderEuropean Regional Development Funden
dc.date.accessioned2022-09-08T14:06:47Z
dc.date.available2022-09-08T14:06:47Z
dc.date.issued2022-08-01
dc.description.abstractThe Boolean Satisfiability Problem (SAT) was the first known NP-complete problem and has a very broad literature focusing on it. It has been applied successfully to various real-world problems, such as scheduling, planning and cryptography. SAT problem feature extraction plays an essential role in this field. SAT solvers are complex, fine-tuned systems that exploit problem structure. The ability to represent/encode a large SAT problem using a compact set of features has broad practical use in instance classification, algorithm portfolios, and solver configuration. The performance of these techniques relies on the ability of feature extraction to convey helpful information. Researchers often craft these features “by hand” to capture particular structures of the problem. Instead, in this paper, we extract features using semi-supervised deep learning. We train a convolutional autoencoder (AE) to compress the SAT problem into a limited latent space and reconstruct it minimizing the reconstruction error. The latent space projection should preserve much of the structural features of the problem. We compare our approach to a set of features commonly used for algorithm selection. Firstly, we train classifiers on the projection to predict if the problems are satisfiable or not. If the compression conveys valuable information, a classifier should be able to take correct decisions. In the second experiment, we check if the classifiers can identify the original problem that was encoded as SAT. The empirical analysis shows that the autoencoder is able to represent problem features in a limited latent space efficiently, as well as convey more information than current feature extraction methods.en
dc.description.sponsorshipScience Foundation Ireland (Grant 16/RC/3918, 12/RC/2289-P2, and 18/CRT/6223 which are co-funded under the European Regional Development Fund)en
dc.description.statusPeer revieweden
dc.description.versionAccepted Versionen
dc.format.mimetypeapplication/pdfen
dc.identifier.citationDalla, M., Visentin, A. and O'Sullivan, B. (2022) 'Automated SAT Problem Feature Extraction using Convolutional Autoencoders', FLOC 2022: Federated Logic Conference, dpcp22 Doctoral Program Papers, July 31- 12 August, Haifa, Israel.en
dc.identifier.endpage9en
dc.identifier.startpage1en
dc.identifier.urihttps://hdl.handle.net/10468/13554
dc.language.isoenen
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.urihttps://easychair.org/smart-program/FLoC2022/paper2269.html
dc.rights© Marco Dalla, Andrea Visentin, and Barry O’Sullivan; licensed under Creative Commons License CC-BY 4.0en
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/en
dc.subjectBoolean satisfiabilityen
dc.subjectDeep learningen
dc.subjectConvolutional autoencodersen
dc.subjectFeature extractionen
dc.subjectSatisfiability predictionen
dc.subjectCNF encodingen
dc.titleAutomated SAT Problem Feature Extraction using Convolutional Autoencodersen
dc.typeConference itemen
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Automated_SAT_Problem_Marco_Dalla.pdf
Size:
503.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