Treffer: SIGmA:GPU accelerated simplification of SAT formulas
Title:
SIGmA:GPU accelerated simplification of SAT formulas
Authors:
Contributors:
Ahrendt, Wolfgang, Tapia Tarifa, Silvia Lizeth
Source:
Osama, M & Wijs, A 2019, SIGmA : GPU accelerated simplification of SAT formulas. in W Ahrendt & S L Tapia Tarifa (eds), Integrated Formal Methods - 15th International Conference, IFM 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11918 LNCS, Springer, Cham, pp. 514-522, 15th International Conference on Integrated Formal Methods, IFM 2019, Bergen, Norway, 2/12/19. https://doi.org/10.1007/978-3-030-34968-4_29
Publisher Information:
Springer
Publication Year:
2019
Subject Terms:
Document Type:
Fachzeitschrift
article in journal/newspaper
Language:
English
ISBN:
978-3-030-34967-7
3-030-34967-5
3-030-34967-5
Relation:
info:eu-repo/semantics/altIdentifier/isbn/9783030349677; urn:ISBN:9783030349677
DOI:
10.1007/978-3-030-34968-4_29
Availability:
Rights:
info:eu-repo/semantics/closedAccess
Accession Number:
edsbas.3B5F7F4E
Database:
BASE
Weitere Informationen
We present SIGmA (SAT sImplification on GPU Architectures), a preprocessor to accelerate SAT solving that runs on NVIDIA GPUs. We discuss the tool, focussing on its full functionality and how it can be used in combination with state-of-the-art SAT solvers. SIGmA performs various types of simplification, such as variable elimination, subsumption elimination, blocked clause elimination and hidden redundancy elimination. We study the effectiveness of our tool when applied prior to SAT solving. Overall, for our large benchmark set of problems, SIGmA enables MiniSat and Lingeling to solve many problems in less time compared to applying the SatElite preprocessor.