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 language||English (US)|
|Number of pages||12|
|Journal||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|State||Published - Dec 1 2004|
All Science Journal Classification (ASJC) codes
- Theoretical Computer Science
- Computer Science(all)