SAT Solving with GPU Accelerated Inprocessing

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

5 Citations (Scopus)


Since 2013, the leading SAT solvers in the SAT competition all use inprocessing, which unlike preprocessing, interleaves search with simplifications. However, applying inprocessing frequently can still be a bottle neck, i.e., for hard or large formulas. In this work, we introduce the first attempt to parallelize inprocessing on GPU architectures. As memory is a scarce resource in GPUs, we present new space-efficient data structures and devise a data-parallel garbage collector. It runs in parallel on the GPU to reduce memory consumption and improves memory access locality. Our new parallel variable elimination algorithm is twice as fast as previous work. In experiments our new solver PARAFROST solves many benchmarks faster on the GPU than its sequential counterparts.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021
EditorsJan Friso Groote, Kim Guldstrand Larsen
Number of pages19
ISBN (Print)9783030720155
Publication statusPublished - 2021

Publication series

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


  • Eager Redundancy Elimination
  • GPU
  • Parallel Garbage Collection
  • Parallel SAT Inprocessing
  • Satisfiability
  • Variable Elimination


Dive into the research topics of 'SAT Solving with GPU Accelerated Inprocessing'. Together they form a unique fingerprint.

Cite this