Cache performance of SAT solvers: A case study for efficient implementation of algorithms

Lintao Zhang, Sharad Malik

Research output: Contribution to journalArticle

10 Scopus citations

Abstract

We experimentally evaluate the cache performance of different SAT solvers as a case study for the efficient implementation of SAT algorithms. We evaluate several different Boolean Constraint Propagation (BCP) mechanisms and show their respective run time and cache performances on selected benchmark instances. From the experiments we conclude that a cache friendly data structure is a key element in the efficient implementation of SAT solvers. We also show empirical cache miss rates of several modern SAT solvers based on the Davis-Logemann- Loveland (DLL) algorithm with learning and non-chronological backtracking. We conclude that the recently developed SAT solvers are much more cache friendly in data structures and algorithm implementations compared with their predecessors.

Original languageEnglish (US)
Pages (from-to)287-298
Number of pages12
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2919
StatePublished - Dec 1 2004

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Cache performance of SAT solvers: A case study for efficient implementation of algorithms'. Together they form a unique fingerprint.

  • Cite this