Download PDFOpen PDF in browserHash-based preprocessing and inprocessing techniques in SAT solversEasyChair Preprint 593916 pages•Date: June 27, 2021AbstractModern 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
|