Hash-based preprocessing and inprocessing techniques in SAT solvers

EasyChair Preprint 5939

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

@booklet{EasyChair:5939,
  author    = {Henrik Cao},
  title     = {Hash-based preprocessing and inprocessing techniques in SAT solvers},
  howpublished = {EasyChair Preprint 5939},
  year      = {EasyChair, 2021}}