Download PDFOpen PDF in browser

Hash-based preprocessing and inprocessing techniques in SAT solvers

EasyChair Preprint 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: CDCL, Preprocessing, SAT, SAT solver, blocked clause elimination, bounded variable elimination, clause signature, hash based preprocessing, hash function, inprocessing

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 5939},
  year      = {EasyChair, 2021}}
Download PDFOpen PDF in browser