The paper presents our work on cache analysis of SAT-solving. The aim is to study how resources are utilized by a SAT-solver and to use this knowledge to improve the resource usage in SAT-solving. The analysis is performed mainly on our CDCL-based SAT-solver and additionally on MiniSAT and PrecoSAT. The measurement is conducted using sample-based profiling on some industrial benchmark from the SAT-competition 2009. During the measurement the following hardware events are traced: total cycles, stall cycles, L2 cache hits and L2 cache misses. From the measurement results, our runtime and implementation analysis unveil that several improvements on resource usage can be done, i.e. on data structures and memory access. These improvements bring about 60% speedup of runtime performance for our solver.
Cache analysis in presence of pointer-based data structures
