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.
Hash-based preprocessing and inprocessing techniques in SAT solvers