Download PDFOpen PDF in browserHash-based preprocessing and inprocessing techniques in SAT solversEasyChair Preprint no. 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: blocked clause elimination, bounded variable elimination, CDCL, clause signature, hash based preprocessing, hash function, inprocessing, Preprocessing, SAT, SAT solver
|