Download PDFOpen PDF in browser

Hash-based preprocessing and inprocessing techniques in SAT solvers

EasyChair Preprint no. 5939

16 pagesDate: June 27, 2021

Abstract

Modern satisfiability solvers are interwoven with important simplification techniques as preprocessors and inprocessors. Implementations of these techniques are hampered by expensive memory accesses which result in a large number of cache misses. In this paper, I explore the application of hash functions in encoding clause structures and bitwise operations for detecting relations between clauses. My evaluation showed a significant increase in performance for subsumption and blocked clause elimination on the Main track benchmark of the 2020 SAT competition.

Keyphrases: blocked clause elimination, bounded variable elimination, CDCL, clause signature, hash based preprocessing, hash function, inprocessing, Preprocessing, SAT, SAT solver

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@Booklet{EasyChair:5939,
  author = {Henrik Cao},
  title = {Hash-based preprocessing and inprocessing techniques in SAT solvers},
  howpublished = {EasyChair Preprint no. 5939},

  year = {EasyChair, 2021}}
Download PDFOpen PDF in browser