SIGmA: GPU accelerated simplification of SAT formulas

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationIntegrated Formal Methods - 15th International Conference, IFM 2019, Proceedings
EditorsWolfgang Ahrendt, Silvia Lizeth Tapia Tarifa
Place of PublicationCham
PublisherSpringer
Pages514-522
Number of pages9
ISBN (Print)9783030349677
DOIs
Publication statusPublished - 1 Jan 2019
Event15th International Conference on Integrated Formal Methods, IFM 2019 - Bergen, Norway
Duration: 2 Dec 20196 Dec 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11918 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference15th International Conference on Integrated Formal Methods, IFM 2019
CountryNorway
CityBergen
Period2/12/196/12/19

Keywords

  • Boolean satisfiability
  • Multi-GPU computing
  • Parallel SAT preprocessing
  • SAT decomposition

Fingerprint

Dive into the research topics of 'SIGmA: GPU accelerated simplification of SAT formulas'. Together they form a unique fingerprint.

Cite this