Automated SAT problem feature extraction using convolutional autoencoders
dc.contributor.author | Dalla, Marco | |
dc.contributor.author | Visentin, Andrea | |
dc.contributor.author | O'Sullivan, Barry | |
dc.contributor.funder | Science Foundation Ireland | en |
dc.date.accessioned | 2021-11-19T11:49:28Z | |
dc.date.available | 2021-11-19T11:49:28Z | |
dc.date.issued | 2021-11-01 | |
dc.date.updated | 2021-11-19T11:36:23Z | |
dc.description.abstract | The Boolean Satisfiability Problem (SAT) is the first known NP-complete problem and has a very broad literature focusing on it. It has been applied successfully to various realworld 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 in 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.sponsorship | Science Foundation Ireland (under Grant number 18/CRT/6223) | en |
dc.description.status | Peer reviewed | en |
dc.description.version | Accepted Version | en |
dc.format.mimetype | application/pdf | en |
dc.identifier.citation | Dalla, M., Visentin, A. and O'Sullivan, B. (2021) 'Automated SAT Problem Feature Extraction using Convolutional Autoencoders', ICTAI 2021: IEEE International Conference on Tools with Artificial Intelligence Virtual event, 01-03 November, pp. 232-239. doi: 10.1109/ICTAI52525.2021.00039 | en |
dc.identifier.doi | 10.1109/ICTAI52525.2021.00039 | |
dc.identifier.eissn | 2375-0197 | |
dc.identifier.endpage | 239 | en |
dc.identifier.isbn | 978-1-6654-0898-1 | |
dc.identifier.startpage | 232 | en |
dc.identifier.uri | https://hdl.handle.net/10468/12238 | |
dc.language.iso | en | en |
dc.publisher | IEEE | en |
dc.relation.project | info:eu-repo/grantAgreement/SFI/SFI Research Centres/12/RC/2289/IE/INSIGHT - Irelands Big Data and Analytics Research Centre/ | en |
dc.relation.uri | https://ieeexplore.ieee.org/document/9643220 | |
dc.rights | For the purpose of Open Access, the authors have applied a CC BY public copyright licence to this Author Accepted Manuscript; Copyright published version: © 2021 IEEE; | en |
dc.rights.uri | https://creativecommons.org/licenses/by/4.0/ | en |
dc.subject | Boolean Satisfiability Problem (SAT) | en |
dc.subject | N-P complete problem | en |
dc.subject | SAT problem | en |
dc.subject | Deep learning | en |
dc.subject | Autoencoders | en |
dc.title | Automated SAT problem feature extraction using convolutional autoencoders | en |
dc.type | Conference item | en |
Files
Original bundle
1 - 1 of 1
Loading...
- Name:
- Marco_-Andrea-_Barry-_IEEE_ICTAI-2021_paper_433.pdf
- Size:
- 225.85 KB
- Format:
- Adobe Portable Document Format
- Description:
- Accepted version
License bundle
1 - 1 of 1
Loading...
- Name:
- license.txt
- Size:
- 2.71 KB
- Format:
- Item-specific license agreed upon to submission
- Description: